Is this a valid semantic for not*?

Help!
1

Is this a sound semantic for negation?

  1. The negation of p(X) is freeze(X,not(p(X)).
  2. The negation of p(X,Y) is freeze(X,freeze(Y,not(p(X))).
  3. etc.

The delayed-negation-by-failure…

Is this valid?

2

The “freeze” needs to be determined by the predicate; getting it right is not trivial. You probably should use when/2, which allows more complex conditions.

Consider something simpler than negation: “different” which is defined as dif(X,Y) :- \+ X=Y. If you have atomic arguments (e.g., dif(1,X),X=2, something like this would work:

dif(X, Y) :- when((nonvar(X), nonvar(Y)), dif_(X, Y). % freeze(X, freeze(Y, dif_(X,Y)))
dif_X, Y) :- ( unifiable(X, Y, _) -> fail; true ).

but if you want to handle something like dif(p(X,b), p(a,C)), then you need to look inside the arguments (nonvar/1 isn’t sufficient and ground/1 is too much). The full code for dif/2 is here: swipl-devel/dif.pl at 0186f1fe0382abd0d35373a4cda0ad045282f23e · SWI-Prolog/swipl-devel · GitHub

Lee Naish wrote some papers in the 1980s about negation and control that you might find useful (some of this is paywalled; but you might find enough in the manuals for MU-Prolog and NU-Prolog).

2 Likes
3

That’s definitely useful to know.

To be clear, my definition would be fine only for atomic terms and not trees (if I threw errors for tree arguments as a compromise, for instance), it would not be a fully general not*.

4

Your proposal is still too “strong”.
For example:

p(1,_).
p(2,_).

then not_p(X,Y):-freeze(X,not(p(X,Y)) would suffice whereas your not_p(X,Y):-freeze(X,freeze(Y,not(p(X,Y)))) would unnecessarily delay when called with not_p(3,_).