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

Question

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

Plaisted [3] showed that it is possible to write formally correct PROLOG programs using first-order predicate-calculus semantics and yet derive nonsense results such as 3 < 2.

指的是当时（1980 年代）Prologs 没有使用 the occurs check。

不幸的是，the paper it cites 在付费专区后面。我仍然希望看到这样的例子。直觉上，感觉省略发生检查只是将结构的范围扩大到包括循环结构（但根据作者的说法，这种直觉一定是错误的）。

我希望这个例子不是

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

那会令人失望。

Answer 1

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

Answer 2

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

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))，s(X) 的值是“three-ish”（它包含三次出现的 s如果你不展开内部的 X)，而 X 本身就是“two-ish”。

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

?- 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 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应该是皮亚诺数。一旦它是循环的，一个就不再是皮亚诺算术。必须在其中添加一些 \+cyclic_term(X) 项。（也许以后，我现在满脑子都是）

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

How can Prolog derive nonsense results such as 3 < 2?

prolog

unification

occurs-check