[m-dev.] Re: Assocative predicates
Fergus Henderson
fjh at cs.mu.OZ.AU
Thu Apr 23 13:53:19 AEST 1998
On 23-Apr-1998, Andrew Bromage <bromage at cs.mu.OZ.AU> wrote:
> 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.
This is all true, except that `:-' is not exactly reverse implication,
due to our use of the completion semantics.
If there's only one clause for a given predicate, then `:-' means `<=>'.
If there's more than one clause, it's a little more complicated, but
to give an example,
p(Args1) :- Clause1.
p(Args2) :- Clause2.
means
all [Args] p(Args) <=> (
some [FV<Args1,Clause1>] Args = Args1, Clause1
;
some [FV<Args2,Clause2>] Args = Args2, Clause2
).
where `FV<X>' denotes the set of unquantified variables in X.
> 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)))).
Well, maybe you want to assert determinism-like properties without
giving a mode definition:
:- pragma assert(all [Y, Z] some [X] p(X, Y, Z).
This assertion would be implied by the mode declaration
:- mode p(out, in, in) is det.
but it may sometimes be useful to give the assertion explicitly,
for example if the code for p/3 is not actually mode-correct in that mode.
> What would be interesting is to work out if single implication assertions
> are useful.
Well, depends on what sort of things you're using assertions for, I guess,
but I can imagine that assertions such as
:- assertion(X > 0 => f(X) > 0).
might help if you're using assertions to help with proofs of
termination, or proofs that an algorithm doesn't divide by zero, etc.
--
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.
More information about the developers
mailing list