quantification (was: Associative predicates)

Lee Naish lee at cs.mu.OZ.AU
Wed Apr 29 16:19:01 AEST 1998

Fergus Henderson <fjh at cs.mu.OZ.AU> writes:

>I think there's little doubt that in general
>it's easy to make mistakes with quantifiers.

My point is that for specifying associativity its the existential
quantifiers which people get wrong, not the universal ones.

>This is the rationale for my proposed rules based on
>universal quantification for variables which occur
>on both sides of `<=>' but for local existential quantification
>for variables that occur only on one side.

Sorry, I seem to have misunderstood your position.  I thought you were
arguing in favour of using the existential closure of an assertion as
the meaning (I was arguing that the universal closure is better).

BTW, I strongly support the suggested change to implicit quantification
rules for <=>.  It make it compatible with NU-Prolog in the case that
the implicitly quantified variables occur only once.  As a general point
about implicit quantification, there is an issue as to how much the
language designer wants to force the programmer to think about
quantification.  In NU-Prolog there was a deliberate choice to make
quantification quite prominent (in a nit-free NU-Prolog program, just
variables starting with _ are implicitly quantified).  This was an
attempt to counteract the prevailing Prolog programming culture which
was very sloppy when it came to logic.  The tradeoffs in Mercury are
different (its not Prolog, its pure, its the 1990's) and it seems
reasonable to use more implicit quantification (and there are certainly
important advantages).


More information about the developers mailing list