Assocative predicates

[Lee Naish]

Zoltan Somogyi <zs at cs.mu.OZ.AU> writes:


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

I disagree.  Implicit universal quantification of free vars over the
whole formula is

1) consistent with the rule used for other logical formulas (ie, clauses)

2) consistent with the rule we have used in assertion languages for
declarative debugging (it makes sense that the assertion language used
for optimisation should be a subset of that used for debugging)

3) more concise for the immediate application (and I suspect more
generally)

4) more natural - this is partly because traditionally we tend to treat
open formulas as their universally closed versions, but also because the
existentially quantified variables which have to be dealt with more
carefully (by the compiler and also by the programmer's brain)

5) less error prone for the immediate application (see previous postings
which have two different kinds of errors, both because people have been
sloppy with their thinking about ABs and BCs)

	lee