[m-dev.] Re: Assocative predicates

[Zoltan Somogyi]

I wrote:
>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.

Lee wrote:
> I disagree.  Implicit universal quantification of free vars over the
> whole formula is
> ...
> 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)

As long as the assertion is just a formula, there is significant scope for
quantification errors. If the assertion had two compulsory parts, a formula
and a set which specifies which variables are non-local, programmers will be
forced think about the issue explicitly, and thus they will make far
fewer mistakes.

Lee wrote:
> 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)

Yes, but the difference is very minor, and there is a trivial translation.

Lee wrote:
> 3) more concise for the immediate application (and I suspect more
> generally)

Yes, but I would argue that this is at the expense of being more likely
to lead to errors, which is not a good trade.

Lee wrote:
> 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)

I disagree, but this is not a question that can be settled by argument.

Zoltan.