[mercury-users] DCG expansion and logical connectives

[Fergus Henderson]

On 24-Nov-1999, Ralph Becket <rbeck at microsoft.com> wrote:
> :- pred ground(atom_type(S), varctxt(S), varctxt(S)).
> :- mode ground(in, mdi, muo) is semidet.
> 
> ground(functor(_Name, _Arity, Args)) -->
>         ( all [Arg]
>                 { list__member(Arg, Args) }
>           =>
>                 ground(Arg)
>         ).
...
> atom.m:488: In clause for predicate `atom:ground/4':
> atom.m:488:   warning: variable `Arg' has overlapping scopes.

I think that is simply due to the relative precedences
of `=>' and `all' not being what you expect.  You need
to write

    ground(functor(_Name, _Arity, Args)) -->
         all [Arg] (
                 { list__member(Arg, Args) }
           =>
                 ground(Arg)
         ).

if you want the universal quantification to scope
over the implication.

The current precedence for `all' and `some' is the same as that used in
NU-prolog.  It seems to cause confusion quite frequently, so I think it
might well be a good idea to change their precedence.  But obviously
that might cause some problems for backwards compatibility.
And it's hard to know whether changing the precedence would
eliminate the confusion or simply lead to confusion for
different examples.

> atom.m:491: In clause for predicate `atom:ground/4':
> atom.m:491:   error: undefined predicate `=>/4'.
> 
> I'm not sure about the first one yet, but the second error has me worried.
> As far as I'm concerned, `,' and ';' etc. are syntax for conjunction and
> disjunction and `=>' is syntax for implication.  Indeed, the reference
> manual states that
> 
> Goal1 => Goal2 
>    An implication. This is an abbreviation for `not (Goal1, not Goal2)'.

Yes, but that is in the "Goals" section of the syntax chapter,
not in the "DCG-goals" section.  It is preceded by the words
"A goal is a term of one of the following forms:".
The definition of `=>' in terms of negation and conjunction
applies only to the use of `=>' in goals, not in DCG-goals.

> So my question is, is this a bug of omission from the DCG transformation
> (I'd say yes) or is there a good reason to eschew implication in DCG
> clauses?

Well, it was a deliberate decision, rather than an accident, so in that
sense it is not a bug.  Our decision was partly based on being
conservative -- it would be possible to give a semantics for
implications in DCGs, but we were not certain that it would be
a good idea, so we took the conservative course of not allowing them.
But in part it was based on a belief that allowing `=>' in DCG goals
would not improve program readability.

The rationale is that in DCGs, the sequence is important, and
implications are concepts from logic which do not necessarily imply any
particular sequence.  For `=>', it might be reasonably obvious that the
sequence is left-to-right, but what about `<=' and (even worse) `<=>'?
For them the sequence would not be clear.  Even if we did allow it, the
use of implication in DCGs would be rare, I think, and so many Mercury
programmers would not be familiar with it.  If the reader has to look
up the language reference manual in order to understand such a
construct, then that construct can hardly be said to improve
readability.  So it's probably going to be clearer to just write such
code using `,' and `not' so that the sequencing is clear.

The rationale that I have explained above does not apply to your
particular case, because in your particular case, one of the goals
in the implication uses { ... }, meaning that it does not access
the DCG arguments, and so the sequencing is irrelevant.
Also for your particular example where the DCG arguments are
this `varcnxt(S)' type, it may be that the operations
on this type are all commutative, so sequencing is not
important.  But in the general case sequencing might well be
important.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------