prolog - Pure Prolog Peano Number 公寓

Question

让我们假设有带有 dif/2 的 pure_2 Prolog 和没有 dif/2 的 pure_1 Prolog。我们能否在不使用 dif/2 的情况下实现 Peano 值的独立性，即 Peano 数？因此，让我们假设我们在 pure_2 Prolog 中有这样的 Peano 独立性：

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

我们可以用更纯粹的定义替换 neq(X,Y)，即来自不使用 dif/2 的 pure_1 Prolog 吗？所以我们有一个终止的 neq/2 谓词可以决定 Peano 数的不等式？那么它的定义是什么？

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

score 3 · Accepted Answer

less从此评论中使用：

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

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

score 2 · Accepted Answer

我想到了其他一些东西，它来自两个Peano Axioms，这也是 Robinson Arithmetic 的一部分。第一个公理已经是一个关于分离性的霍恩子句：

   ∀x(0 ≠ S(x)) 

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

将对立应用于第二个公理给出。
该公理现在是一个关于分离性的霍恩子句：

   ∀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

2 回答 2