Search code examples
prologsuccessor-arithmeticslogical-purity

Pure Prolog Peano Number Apartness

Lets assume there is pure_2 Prolog with dif/2 and pure_1 Prolog without dif/2. Can we realize Peano apartness for values, i.e. Peano numbers, without using dif/2? Thus lets assume we have Peano apartness like this in pure_2 Prolog:

/* pure_2 Prolog */
neq(X, Y) :- dif(X, Y).

Can we replace neq(X,Y) by a more pure definition, namely from pure_1 Prolog that doesn't use dif/2? So that we have a terminating neq/2 predicate that can decide inequality for Peano numbers? So what would be its definition?

/* pure_1 Prolog */
neq(X, Y) :- ??
Solution

  • Using less from this comment:

    less(0, s(_)).
less(s(X), s(Y)) :- less(X, Y).

neq(X, Y) :- less(X, Y); less(Y, X).