harald at cs.mu.OZ.AU
Mon Apr 20 19:18:03 AEST 1998
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.
More information about the developers