Pure Prolog Peano Number Apartness

Question

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) :- ??

MWB · Accepted Answer · 2020-12-23T16:48:23.480

3

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

edited Dec 23 '20 at 16:48

answered Dec 23 '20 at 16:46

MWB

11,740
6
46
91

Oki Doki, (;)/2 again. For being pure it would be two clauses... – Dec 23 '20 at 16:47
1

`?- neq(X,Y), X = s(0), Y = 0.` unnecessarily loops. – false Dec 24 '20 at 08:51
@false Very interesting. Thanks. I'll try to fix `less/2`. – MWB Dec 24 '20 at 13:19

score 3 · Answer 2 · answered Dec 23 '20 at 16:58

3

I had something else in mind, which is derived from two of the Peano Axioms, which is also part of Robinson Arithmetic. The first axiom is already a Horn clause talking about apartness:

   ∀x(0 ≠ S(x)) 

   ∀x∀y(S(x) = S(y) ⇒ x = y)

Applying contraposition to the second axiom gives.
The axiom is now a Horn clause talking about apartness:

   ∀x∀y(x ≠ y ⇒ S(x) ≠ S(y))

Now we have everything to write some Prolog code.
Adding some symmetry we get:

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

Here are some example queries. Whether the predicate leaves a choice
point depends on the Prolog system. I get:

SWI-Prolog 8.3.15 (some choice point):

?- neq(s(s(0)), s(s(0))).
false.

?- neq(s(s(0)), s(0)).
true ;
false.

Jekejeke Prolog 1.4.6 (no choice point):

?- neq(s(s(0)), s(s(0))).
No

?- neq(s(s(0)), s(0)).
Yes

answered Dec 23 '20 at 16:58

Your prolog program is basically the same as the one from the accepted answer, sans trivial transformation. – gusbro Dec 24 '20 at 00:37
2

@gusbro: Trivial means here belonging to the [trivium](https://en.wikipedia.org/wiki/Trivium). While it has the same termination property, it is superior w.r.t existential termination. `?- neq(X,Y), X = s(0), Y = 0.` finds a solution whereas the other answer just loops away. – false Dec 24 '20 at 08:49
@false: You are right, this program does not loop in your example as with the accepted answer. And I meant "trivial transformation" as in "simple transformation"; now I see it does not behave exactly the same. – gusbro Dec 27 '20 at 21:57
For the reasons @false and gusbro discuss, this should instead be the accepted solution. – Jason Hemann Apr 30 '22 at 21:47

score 1 · Answer 3 · answered Dec 28 '22 at 12:01

Just removing the unwanted choicepoint (in swi-prolog) from user502187's answer:

neq(0, s(_)).
neq(s(N), M) :-
    % Switch args, to use first-arg indexing
    neq_(M, s(N)).

neq_(0, s(_)).
neq_(s(N), s(M)) :-
    % Switch args back, to fix choicepoint
    neq(M, N).

Results in swi-prolog:

?- neq(s(s(0)), s(0)).
true.

?- neq(s(0), s(s(0))).
true.

?- neq(N, M).
N = 0,
M = s(_) ;
N = s(_),
M = 0 ;
N = s(s(_)),
M = s(0) ;
N = s(0),
M = s(s(_)) ;
N = s(s(0)),
M = s(s(s(_))) ;
N = s(s(s(_))),
M = s(s(0)) ;

Pure Prolog Peano Number Apartness

3 Answers3

Linked