[m-dev.] Re: Assocative predicates
bromage at cs.mu.OZ.AU
Thu Apr 23 10:00:38 AEST 1998
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
:- 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"?)
More information about the developers