[m-dev.] Re: Assocative predicates

[Andrew Bromage]

G'day all.

Fergus Henderson wrote:

> When Harald say "It seems nicer to simply use that formula", I think that
> Harald is probably just so used to the convention of implicit universal
> quantification that he has forgotten that we are using it.
> But to someone who does more Mercury or Prolog programming than
> they do logic theory, the opposite convention of implicit existential
> quantification in goals may seem more natural.

Of course in Mercury/Prolog we _do_ use implicit universal quantification,
but it's applied to the clause as a whole, not just the goals (as you
correctly point out, Fergus).  That is:

	p(X, Y) :- some [Q] (q(X, Q), r(Q, Y)).

is the same as:

	all [Q] (p(X, Y) :- q(X, Q), r(Q, Y)).

This is precisely because :- is reverse implication.  The thing is that
most programmers tend to forget this and just pretend the implicit
quantification is a `some'.

On a related note:  Is it ever important in these assertions that a
variable be existentially quantified over the whole assertion?  That
is:

:- pragma assert(all [X] (some [Y] (p(X, Y) <=> q(X, Y)))).

What would be interesting is to work out if single implication assertions
are useful.  (Can we say "macros"?)

Cheers,
Andrew Bromage