diff: Fix problem with quantifiers and double negation

[Lee Naish]

Fergus Henderson <fjh at cs.mu.OZ.AU> writes:

>Thus, I think the ideal thing from this perspective would be to push
>negations inwards as far as possible, so long as this will not reduce
>mode-correctness.  So we would apply the following transformations:
>	
>	1.	`~(~P)' ===> P.

>	2.	`~(P ; Q ; ...)' ===> `(~P, ~Q, ...)'.

>	3.	`~(if P then Q else R)' ===> `if P then ~Q else ~R'.

>	4.	`~(P, Q, ...)' ===> `~NotP ; ~NotQ ; ...' iff
>			`~P' ===> `NotP', and `~Q' ===> `NotQ', and ...

>the scopes of variables.  This causes some problems, as I will explain

Very true.  Its very tempting to assume that predicate logic behaves the
same way as propositional logic when it comes to transforming negation
and other constructs.  Unfortunately it is not.  Please don't implement
3 and 4 above - they are wrong.

>According to the language reference manual, implicit quantification
>comes before elimination of double negation.  I think this is the
>right thing from the point of view of language design, especially
>if we change elimination of double negation into something more complicated,

Indeed.  Nearly all transformations are sensitive to quantification and
the quantification should be clarified before the transformations are
performed/though about etc.  I guess from the following:

>    (2) require a fairly significant change to the current implementation,

that quantification is dealt with after some transformation.  I think it
may have been wiser to clarify the quantification first, thus allowing
all sorts of things (such as the current discussion) to be done "right"
in later stages.

	lee