[m-dev.] Re: Assocative predicates

[Fergus Henderson]

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.