Pure Prolog Peano Number Apartness

Question

假设存在带dif/2的pure_2 Prolog和不带dif/2的pure_1 Prolog。我们能意识到吗值的Peano伙伴关系，即Peano数，而不使用dif/2？因此，假设我们在pure_2 Prolog:中有这样的Peano伙伴关系

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

我们可以用一个更纯粹的定义来代替neq(X，Y(吗？也就是说，从不使用dif/2的pure_1Prolog中？所以我们有一个终止的neq/2谓词，它可以决定Peano数的不等式？那么它的定义是什么呢？

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

Answer 1

使用此注释中的less：

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

Answer 2

我有其他想法，它源自两个Peano公理，也是Robinson算术的一部分。第一条公理已经是关于伙伴关系的Horn子句：

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

将对位法应用于第二公理给出
公理现在是一个Horn子句，谈论伙伴关系：

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

现在我们有了编写Prolog代码的一切
添加一些对称性：

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

以下是一些查询示例。谓词是否留下选择
点取决于Prolog系统。我得到：

SWI Prolog 8.3.15(一些选择点(：

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

Jekejeke Prolog 1.4.6(无选择点(：

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

Answer 3

只是从用户502187的答案中删除了不需要的选择点：

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

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