[m-dev.] Re: diff: Fix problem with quantifiers and double negation

[Fergus Henderson]

On 23-Jun-1998, Lee Naish <lee at cs.mu.OZ.AU> wrote:
> 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 ...

Sorry, I made a mistake there -- I meant

	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.

For those of us who still haven't had the first coffee of the day ;-),
could you please elaborate, e.g. by giving a counter-example?

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

Yes, we currently do just a few transformations -- the expansion of
`<=>', `=>' and `<=' and the elimination of double negation --
before doing quantification analysis.

The main reason for this was to avoid the need to have seperate HLDS goal
types for `<=>' and `=>'.

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

Yep.  As I mentioned in our earlier discussions on rules for implicit
quantification of assertions, the current rules regarding implicit
quantification of `<=>' do the wrong thing, precisely because it
gets expanded before quantification analysis.

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