[m-dev.] Re: Assocative predicates

[Zoltan Somogyi]

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

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. What we would be requiring is that
the formulae on the two sides of the equivalent have the same set of solutions
when projected onto this set of variables. The compiler would need to check
when it applies the equivalence that any variables in the actual code that
correspond to variables not in this set do not occur outside the matched
code. For example, if the compiler wants to apply the equivalence to
optimize the code fragment

p(...) :-
	...
	append(X,Y,U),
	append(U,Z,All),
	...

it would need to verify that U occurs nowhere else in p.

Zoltan.