纯Prolog Peano数的不相等性

Question

假设存在具有 dif/2 的 pure_2 Prolog 和没有 dif/2 的 pure_1 Prolog。我们能否在不使用 dif/2 的情况下实现数值的 Peano apartness，即 Peano 数字？因此，假设我们在 pure_2 Prolog 中具有以下 Peano apartness：

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

我们能否用更纯粹的定义来替换neq（X，Y）？也就是来自pure_1 Prolog的定义，它不使用dif/2吗？这样我们就可以拥有一个终止的neq/2谓词，它可以决定Peano数字的不等关系。那么它的定义会是什么？

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

- user502187

Answer 1

从这个评论中使用less:

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

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

- MWB

---

好的，（;）/2 再来。为了保持纯洁，它应该是两个从句... - user502187

?- neq(X,Y), X = s(0), Y = 0. 会不必要地循环。 - false

@false 非常有趣。谢谢。我会尝试修复less/2。 - MWB

Answer 2

我心目中想到的内容源自于两个皮亚诺公理中的一个，也是罗宾逊算术的一部分。第一个公理已经是一个谔谔角式，讨论了不同之处：

   ∀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

- user502187

---

你的Prolog程序基本上与被接受答案中的程序相同，除了一些微不足道的转换。 - gusbro

@gusbro：Trivial 在这里指的是属于 trivium。虽然它具有相同的终止性质，但在存在性终止方面优越。 ？- neq(X,Y)，X = s(0)，Y = 0. 找到了一个解，而另一个答案则会一直循环下去。 - false

@false: 你说得对，这个程序在你的示例中不会循环，与被接受的答案不同。我所说的“平凡变换”是指“简单变换”; 现在我看到它的行为并不完全相同。 - gusbro

由于@false和gusbro所讨论的原因，这应该成为被采纳的解决方案。 - Jason Hemann

Answer 3

从user502187的答案中删除不需要的选择点（在swi-prolog中）：

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

- brebs