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

[Fergus Henderson]

On 24-Jun-1998, Andrew Bromage <bromage at cs.mu.OZ.AU> wrote:
> G'day all.
> 
> Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> 
> > >	4.	`~(P, Q, ...)' ===> `NotP ; NotQ ; ...' iff
> > >			`~P' ===> `NotP', and `~Q' ===> `NotQ', and ...
> > 
> Lee Naish replied:
> > The correctness of 4. depends very much on what rules are
> > used for implicit quantification and what restrictions are placed on
> > modes.
> 
> It doesn't look right on the face of it.  This goal:
> 
> 	\+ (
> 		produce(X :: out) is det,
> 		test(X :: in) is semidet
> 	)
> 
> does not correctly transform into:
> 
> 	(
> 		\+ (produce(X :: out) is det)
> 	;
> 		\+ (test(X :: in) is semidet)
> 	)

This transformation is not allowed by "4" above, because
it doesn't satisfy the `~P' ===> `NotP' condition, since there is no
rule for `===>' for which `\+ produce(X)' ===> `\+ produce(X)'.

The idea behind rule 4 is that it only works if the conjuncts are
themselves negated -- in that case it is safe, because the conjuncts
must have no outputs, so there can be no conjunct like `test(X)' that
depends on the outputs of one of the other conjuncts.

However, now that I think about it, there is a bug in the rule, because
rules 2 & 3 for `===>' can succeed for `~P' even if P itself is not
negated.  But the fix is not too hard.

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