[m-dev.] Re: Assocative predicates

[Fergus Henderson]

I had a talk with Zoltan and Peter Ross about this, and I came up with
another idea.  Basically, we can get the "right" quantification
for assertions involving "<=>" just by a very small tweak to the
current rules for implicit quantification -- one which is quite
natural and which could be seen as just a "bug" in the original
specification.

The current rules for implicit quantification (see
`info -f mercury lang syntax impl') say this:

 | An occurrence of a variable is "in a negated context" if it is in a
 | negation, in a universal quantification, in the condition of an
 | if-then-else, in an inequality, or in a lambda expression.

Currently expansion of `<=>', `=>', and `<=' into `not' and `,'
occurs before implicit quantification (well, the reference manual
is not completely explicit about this, but I think that was my intent,
and that's certainly what the compiler does).  This works OK for
`=>' and `<=', where it just means that both sides of an
implication are considered to be "negated contexts" inside
which variables are locally existentially quantified.
However, for `<=>', when you expand to `<=' and `=>', the
goal gets duplicated, which then causes the implicit
quantification rules to do the wrong thing.  
What we'd like is for implicit quantification to occur *before*
expansion of bi-implications, with both sides of a bi-implication
to be considered to be negated contexts, and for variables
which occur on either side to thus be implicitly existentially
quantified around their closest enclosing scope.

Thus, I propose we change the language reference manual as follows:

1.  In the definition of "negated context", we should insert
    "... or on either side of an implicitation or bi-implication".

2.  We should add some explicit wording to say that the syntactic expansion
    of `<=>', `=>', and `<=' occurs *after* implicit quantification.

Comments?

-- 
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.