[m-dev.] Re: Assocative predicates
fjh at cs.mu.OZ.AU
Wed Apr 22 21:06:53 AEST 1998
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
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.
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 18.104.22.168 | -- the last words of T. S. Garp.
More information about the developers