[m-dev.] Re: Assocative predicates

[Fergus Henderson]

On 17-Apr-1998, Lee Naish <lee at cs.mu.OZ.AU> wrote:
> Fergus Henderson <fjh at cs.mu.OZ.AU> writes:
> >On 16-Apr-1998, Peter Schachte <pets at cs.mu.OZ.AU> wrote:
> >How about just `pragma assert(Goal)'?
> 
> >	:- pragma assert(all [A,B,C] (A+B)+C=A+(B+C)).
> 
> >	:- pragma assert(all [A,B,C,D,E,F,G,H] (
> >		foo(A, B, C, D, E), foo(D, E, F, G, H) <=> 
> >		foo(A, B, F, D, E), foo(D, E, C, G, H))).
> 
> I think there is some confusion here.

Yes, you're right.

> You want to express something
> like
> 	some [ABs] (append(As, Bs, ABs), append(ABs, Cs, ABCs)) <=>
> 	some [BCs] (append(As, BCs, ABCs), append(Bs, Cs, BCs))
> 
> The existential quantification of the linking variable is very important

Agreed.

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?

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