Assocative predicates

[Harald Sondergaard]

Fergus Henderson <fjh at cs.mu.OZ.AU> writes:

>If you're using explicit existential quantification, then the
>natural thing is to push the quantifiers down into the formula:

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

Care is necessary here.  

    some [X,Y] (p(X) <=> q(Y))

is not logically equivalent to

    (some [X] p(X)) <=> (some [Y] q(Y))

I think that you do indeed want the formula as you gave it, but it is
not right to think of it as a result of "pushing the quantifier in".
Unfortunately there are no nice rules of passage over biimplication.

>In contrast, if you're using explicit universal quantification,
>then you'll just use a single quantifier at the top-level:

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

But then it has to be understood that the intended meaning is the
formula you gave above.  It seems nicer to simply use that formula.

>For commutativity, you want universal quantification:

>	all [As, Bs] p(As, Bs) <=> p(Bs, As)

Unless you use the rule you suggested earlier, that LHS-specific
and RHS-specific variables are existentially quantified (inside the
biimplication) and all other variables are universally quantified 
(outside the biimplication).  I think that this kind of implicit
quantification would always work for you -- I certainly can't think
of a counter-example.

Harald