[m-dev.] Re: Assocative predicates

[Fergus Henderson]

On 19-Apr-1998, Zoltan Somogyi <zs at cs.mu.OZ.AU> wrote:
> 
> [Fergus wrote:]
> > One question we need to answer is what should the default
> > quantification be for goals inside `pragma assert'?
> > Should variables be implicitly existentially quantified
> > or should they be implicitly universally quantified?
> 
> I think the right thing to do is to state the set of variables with respect to
> which observational equivalent is required, which in this case would be
> As, Bs, Cs and ABCs, but not ABs or BCs.

This would correspond to stating the set of variables which are universally
quantified, and having the remainder be implicitly existentially quantified.
The obvious syntax for this would be the one I was using previously:

	:- pragma assert(all [As, Bs, Cs, ABCs] 
		(append(As, Bs, ABs), append(ABs, Cs, ABCs)) <=>
		(append(Bs, Cs, BCs), append(As, BCs, ABCs))).

Note that in this example, the set of variables which are universally
quantified happens to be exactly the set of variables shared between
the LHS and the RHS of the equivalence.  I think this may be true
in general.  (Counter-examples, anyone?)
Thus, perhaps it would be worth making this the default.
To do this, we'd be giving the top-level `<=>' some special semantics,
so we ought to use a different syntax for it.  For example, we could use

	:- pragma assert_equivalent(
		(append(As, Bs, ABs), append(ABs, Cs, ABCs)),
		(append(Bs, Cs, BCs), append(As, BCs, ABCs))
	).

or

	:- pragma assert(
		(append(As, Bs, ABs), append(ABs, Cs, ABCs))
		is_equivalent_to
		(append(Bs, Cs, BCs), append(As, BCs, ABCs))
	).

or something like that.  This would mean that in the common case
the programmer wouldn't need to write any explicit quantification.

-- 
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.