Seeking a pure Prolog implementation of (\=)/2

Question

Negation as failure is usually considered impure. The Prolog interpreter needed for negation as failure must realize SLDNF which is an extension of SLD.

The predicate (\=)/2 is for example used in the library(reif). It can be bootstrapped via negation as failure as follows, but is often a built-in:

X \= Y :- \+ X = Y.

Would it be possible to implement (\=)/2 as a pure predicate? Using only pure Prolog, i.e. only first order horn clauses?

Answer 1

Would it be possible to implement (=)/2 as a pure predicate? Using only pure Prolog, i.e. only first order horn clauses?

You can't implement (\=)/2 in pure Prolog.

Proof:

In logic, conjunction is commutative, and pure Prolog queries, if they terminate, must be logical.

However, with (\=)/2, the order of the terms matters, so it is not logical:

?- X \= Y, X=0, Y=1.
false.

?- X=0, Y=1, X \= Y.
X = 0,
Y = 1.