[m-dev.] Re: Assocative predicates
zs at cs.mu.OZ.AU
Mon Apr 20 11:03:02 AEST 1998
>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
> 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
> 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.
> 3) more concise for the immediate application (and I suspect more
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.
> 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.
More information about the developers