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

[Fergus Henderson]

On 12-Jun-1998, Zoltan Somogyi <zs at cs.mu.OZ.AU> wrote:
> 
> > +:- pred all_negated(list(hlds_goal), list(hlds_goal)).
> > +:- mode all_negated(in, out) is semidet.
> > +
> > +all_negated([], []).
> > +all_negated([not(Goal) - _ | NegatedGoals], [Goal | Goals]) :-
> > +	all_negated(NegatedGoals, Goals).
> 
> This will not catch cases where the conjunction is nested. I believe nested
> conjunctions can occur at that stage of the processing.

They can't, as it happens.  But it would be easy to handle
nested conjunctions here, and that could make the code more robust
against future changes and it could make it easier to verify the correctness
of the code, so I will make the change you suggest anyway.

> Is there any reason why we shouldn't also do the converse transformation,
> i.e. turning the negation of a disjunction in which each disjunct is a
> negated goal into the conjunction of the unnegated disjuncts? E.g.
> ~(~p or ~q) ===> p, q.

That suggestion makes quite a lot of sense.

However, I'm not sure that even that is quite enough.
We could also handle mixtures of conjunctions and disjunctions,
e.g. `(~p ; ~q) => r' expands to `~((~p ; ~q), ~r)',
which could be converted to `(p, q ; r)'.

Also we could do `~(if p then q else r)' ===> `if p then ~q else ~r'.

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

But there is one problem with your suggestion, I'm afraid.
The problem is that converting disjunctions into conjunctions affects
the scopes of variables.  This causes some problems, as I will explain
below.

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,
because the rules for implicit quantification ought to be very simple and
easy to understand -- a programmer shouldn't have to mentally perform
all the various expansions of `<=>' and `=>' and pushing negations
inwards in order to know the scope of their variables.

With the current rules, however, it actually doesn't make any different
whether you do implicit quantification first or double negation
elimination first, and the current implementation in fact actually
performs double negation elimination first.

But with the extra transformation you suggested, the order of these
two passes would be important.  If I write

	foo :-
		~(~(p(X),q(X)) ; ~(r(X),s(X))).

then according to the current rules for implicit quantification
the two Xs on the left are a different variable than the two Xs on the right.
So, if the implementation were to transform this into

	foo :-
		(p(X),q(X)) , (r(X),s(X))).

then that would be incorrect.  In order for the implementation to
correctly implement the language reference manual, it would need
to do double negation elimination *after* implicit quantification,
so that the transformed goal would end up as

	foo :-
		(p(X_1),q(X_1)) , (r(X_2),s(X_2))).

(Note that converting negated conjunctions of negations into
disjunctions does not cause the same kind of problem.)

So, given that doing the more complicated rules would

    (1) complicate the language a little, and
    (2) require a fairly significant change to the current implementation,

and given that we have not yet come across any real-world examples
that would require the more complicated rules, I think we should
leave things as is, at least unless and until someone demonstrates
a real need for it.

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.