[m-dev.] Re: Assocative predicates

[Fergus Henderson]

On 20-Apr-1998, Lee Naish <lee at cs.mu.OZ.AU> wrote:
> Implicit universal quantification of free vars over the
> whole formula is
> 
> 1) consistent with the rule used for other logical formulas (ie, clauses)

But inconsistent with the rule used for clause _bodies_,
which is the only other place where Mercury allows arbitrary logical
formulas.

> 2) consistent with the rule we have used in assertion languages for
> declarative debugging

The current such assertion languages are not at all widely used,
so I don't think we should give this argument much weight.

> (it makes sense that the assertion language used
> for optimisation should be a subset of that used for debugging)

Agreed.  But IMHO the historical precedent here is not strong enough to
be important; thus if you think that implicit universal quanfication
is best for debugging assertion languages, then you need to explain why.

> 3) more concise for the immediate application

The difference is pretty marginal either way.

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

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

So we're comparing `some [ABs] ... <=> some [BCs] ...'
with               `all [As, Bs, Cs, ABCs] (... <=> ...)'.
It's pretty marginal.

> (and I suspect more generally)

This may be right.  It's hard to know.

For commutativity, you want universal quantification:

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

> 4) more natural - this is partly because traditionally we tend to treat
> open formulas as their universally closed versions,

As a long-time Mercury programmer (;-), I disagree.

In Mercury, the only other place where arbitrary formulas are allowed
is in clause bodies, and in clause bodies variables are implicitly
existentially quantified.  As a Mercury programmer I find it unnatural
to have to explicitly exisentially quantify variables -- normally this
is never necessary.

Another example of this is that current in Mercury

	p(f(X))

is always equivalent to
	
	(V = f(X), p(V))

where V is some fresh variable, presuming this is syntactically correct.
(The only time it is not syntactically correct is in clause heads,
where you have to put the V = f(X) in the body rather than in the head.)

If assertions are implicitly universally quantified, then the above
statement would not be true in assertions -- instead you'd have to
replace `p(f(X))' with `some [V] (V = f(X), p(V))'.
                        ^^^^^^^^

> 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 don't agree with this.  The Mercury compiler in fact keeps track of the
*non*-existentially-quantified variables ("non-locals") for each subgoal.
So it is those ones which require special treatment by the compiler.
The same is true of the programmer's brain, at least for me.

> 5) less error prone for the immediate application

I'm not convinced about this.

Also this must be weighed up against the consideration of the cost of
the errors.  A universally quantified assertion is stronger than an
existentially quantified assertion.  Thus if the default quantification
is existential, and you forget an explicit (universal) quantifier, then
you've made a weaker assertion than you meant to, which is probably
better than what would happen in the converse case: it might make your
program run slower, but it wouldn't cause the program to report wrong
results.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.