Assocative predicates

[Lee Naish]

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.  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
(for transformation purposes you need to know there are no other
occurrences of that variable, ie, the scope of the quantification can
be reduced to just those two calls).

>This syntax seems to be nice, at least from the user's perspective.
>It may require more effort for the compiler to figure out which
>assertions specify associativity...

True.  It may also be useful to know the relative efficiency of the two
formulas.  There are cases where you can cleverly apply associativity
and accumulator techniques and get a nice tail-recursive program which
is O(N^2) where the original simple code is O(N) (eg, flattening lists).

Also, its nice to generalise the notion of associativity to the case
where the types of the inputs are different: *->**->* or *->**->** in
Miranda notation (basically you want to know how to convert between
foldl and foldr - identity elements come in here also).

	lee