quantification (was: Associative predicates)

[Fergus Henderson]

On 27-Apr-1998, Lee Naish <lee at cs.mu.OZ.AU> wrote:
> 
> Re: quantification in assertions
> 
> There have now been three different errors concerning the existentially
> quantified variables.

I think there's little doubt that in general
it's easy to make mistakes with quantifiers.

There's two possible responses to this:

	(1) Require all quantifiers to be explicit.
	    This way, programmers will be forced to think about
	    which quantification they want, which will hopefully
	    reduce the number of times they accidentally get the
	    wrong quantification.

	(2) Design the rules so that explicit quantifiers are
	    almost never needed.  Favour a more complicated set
	    of rules that get things right in most cases, so
	    that most of the time the programmer doesn't need to
	    think about quantification.

Both of these are reasonable design choices.
Arguably (1) may lead to more reliable code,
while (2) leads to much more concise code.
However, more concise code is often more readable,
and in the long run, code that is more readable
will be more reliable, so the reliability advantage
of (1) may be outweighed by the advantages of conciseness.

Thus when designing the rules for implicit quantification of
clauses in Mercury we chose option (2).
(This design decision was additionally motivated by
the goal of Prolog syntax compatibility.)
I think we should continue to favour the same design principles
when designing rules for implicit quantification of assertions.

This is the rationale for my proposed rules based on
universal quantification for variables which occur
on both sides of `<=>' but for local existential quantification
for variables that occur only on one side.

> People seems to be getting closer to the relationship
> between assertions and clauses or collections of them.  Lets make it
> explicit: (collections of) clauses are special cases of assertions (they
> are special primarily because they have a procedural reading as well as
> the declarative reading, and to make this feasible they are restricted
> in various ways, particularly having one distinguished positive literal).
> Assertions are not a generalisation of (the logic of) goals; they
> are a generalisation of clauses.

Fine so far...

> We allow the clause:
> 
> cons(A, As, A.As).
> 
> It makes sense that we allow the assertion/specification:
> 
> :- assertion cons(A, As, A.As) <==> true.
> 
> to mean (declaratively) the same thing,

I don't think that follows directly.
Instead, you should say that the assertion

	:- assertion cons(A, As, [A|As]).

means the same thing as the above clause.
And with the rules that I have proposed, it does.

> Fortunately, Fergus has started using implicit universal quantification
> in his more recent postings (on type classes :-).

I've been using implicit universal quantification
but with both sides of `<=>' considered as negative
contexts; that is, both sides of `<=>' are treated
the same as clause bodies rather than as clause heads.

Thus `:- assertion cons(A, As, A.As) <==> true.'
does not mean the same thing as `:- assertion cons(A, As, A.As)',
because in the former the `cons' goal is treated like a clause
body (and hence the variables are locally existentially quantified),
whereas in the former it is treated like a clause head (and hence
the variables are universally quantified over the scope of
the whole clause).

By a very similar argument to the one you give above,
it would make sense if the semantics of the clause

	p :- cons(A, As, [A|As]).

were the same as the semantics of

	:- assertion p <=> cons(A, As, [A|As]).

(possibily with `<=' instead of `<=>').  This requires that the RHS of
`<=>' (or `<=') be considered a negative context for the purpose of
implicit quantification.  Symmetry strongly suggests that the
quantification rules for the LHS and RHS of `<=>' should be the same.

The different equivalences that we are trying to preserve are mutually
contradictory.  Something has to give.  If you look at a single example
like the one Lee gave, then it can argue for one particular decision,
to avoid breaking one particular equivalence, but we need to consider
the overall picture and decide which of these equivalences are more
important.

Earlier, I asked for examples for which my proposed rule did not give
the desired quantification.  Lee's example of

	:- assertion cons(A, As, [A|As]) <=> true.

is such an example.  However, I think that in practice
a programmer would be more likely to (should) instead
write it as just

	:- assertion cons(A, As, [A|As]).

and this example does have the desired quantification under my proposed
rules.  Thus I don't consider Lee's example to be a compelling one.

Cheers,
	Fergus.

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