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?

if-then-else is ISO core standard Prolog, the ISO core standard provides SLDNF and a little beyond and not only SLD. But it is not first order horn clauses. The question wants a pure Prolog implementation, and pure is specified in the question as first order horn clauses. — , Dec 18 '20 at 21:23
If it were possible to implement `\=` in pure Prolog, then we'd be able to implement list intersection in pure Prolog also (see David's answer [here](https://stackoverflow.com/questions/65351535/)). So far, no one could do the latter. If we can't even do that, this kind of makes you question the logic programming paradigm in general. — MWB, Dec 18 '20 at 23:05
fail is Horn. Just don't define it. Empty number of Horn clauses for fail. For example in ISO core Prolog you could define it as :- dynamic fail/0. And if you don't assert anything it will behave as the built-in fail. — , Dec 18 '20 at 23:20

MWB · Accepted Answer · 2020-12-19T01:23:54.760

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.

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

1 Answers1