prolog - Prolog 如何得出 3 < 2 之类的无意义结果？

Question

我正在阅读的一篇论文说：

Plaisted [3] 表明，可以使用一阶谓词演算语义编写形式上正确的 PROLOG 程序，并得出诸如 3 < 2 之类的无意义结果。

它指的是Prologs当时（1980年代）没有使用发生检查的事实。

不幸的是，它引用的论文位于付费墙后面。我仍然希望看到这样的例子。直觉上，似乎省略了发生检查只是将结构的范围扩大到包括圆形结构（但根据作者的说法，这种直觉一定是错误的）。

---

我希望这个例子不是

smaller(3, 2) :- X = f(X).

那将令人失望。

Answer 1

这是论文中现代语法的示例：

three_less_than_two :-
    less_than(s(X), X).

less_than(X, s(X)).

事实上，我们得到：

?- three_less_than_two.
true.

因为：

?- less_than(s(X), X).
X = s(s(X)).

具体来说，这解释了查询中 3 和 2 的选择：给定X = s(s(X))的值为“three-ish”（如果不展开 inner ，s(X)它包含三个出现的），而其本身是“two-ish”。sXX

启用发生检查让我们回到逻辑行为：

?- set_prolog_flag(occurs_check, true).
true.

?- three_less_than_two.
false.

?- less_than(s(X), X).
false.

所以这确实是沿着

arbitrary_statement :-
    arbitrary_unification_without_occurs_check.

Answer 2

我相信这是您自己看不到的论文的相关部分（没有付费墙限制我在使用 Google Scholar 时查看它，您应该尝试以这种方式访问​​）：

Answer 3

好的，给定的示例如何工作？

如果我把它写下来：

sm(s(s(s(z))),s(s(z))) :- sm(s(X),X).  % 3 < 2 :- s(X) < X
sm(X,s(X)).                            % forall X: X < s(X)

询问：

?- sm(s(s(s(z))),s(s(z)))

那是一个无限循环！

扭转局面

sm(X,s(X)).                            % forall X: X < s(X)
sm(s(s(s(z))),s(s(z))) :- sm(s(X),X).  % 3 < 2 :- s(X) < X

?- sm(s(s(s(z))),s(s(z))).
true ;
true ;
true ;
true ;
true ;
true 

深层次的问题是X应该是皮亚诺数。一旦它是循环的，它就不再是 Peano 算术了。必须在其中添加一些\+cyclic_term(X)术语。（也许以后，我的脑子现在已经满了）