Peano算术中的`less/2`关系答案

【问题标题】：`less/2` relation in Peano arithmeticPeano算术中的`less/2`关系
【发布时间】：2020-12-24 13:57:38
【问题描述】：

Peano 算术中的这个小于谓词

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

循环

?- less(X, Y), X=s(0), Y=0.

有没有更好的方法来编写less/2（仅使用 Horn 子句）？

【问题讨论】：

请注意@false 的评论stackoverflow.com/questions/65427391/… 是关于建立在less/2 之上的“幼稚”neq/2。这并不是指出less/2 的问题，而是说在 Prolog 中，两个目标的分离，每个目标都有无限的解决方案，不会表现得公平。
@IsabelleNewbie 你不觉得less/2 的这种行为本身就很麻烦吗？
如果您想要一个能够枚举答案的less/2，则不是。如果它可以枚举答案，那么这个查询会说“枚举所有 N, M 对，使得 N 必然循环。与neq/2 的区别很重要，因为与less/2 不同，分配X=s(0), Y=0 是一个有效的解决方案。当您要求neq/2 搜索此解决方案时，循环是不必要的。
@IsabelleNewbie 我明白你和@false 的意思了。谢谢。
@IsabelleNewbie：“两个目标的分离，每个都有无限的解决方案将不公平” 反例：( X = f(_) ; X = g(_) )。这是两个目标的分离，每个目标都有无限的解决方案。它甚至终止，从而公平地列举解决方案。需要进一步要求的是，这些无限解只能用无限多的答案来描述。否则我完全同意你的看法。

【解决方案1】：

您可以使用when/2。使它不再是一个无限枚举的谓词，并且仍然保持 100% 的纯正。 when/2 修改了 SLD-Resolution 中的 S（选择规则），这个想法可以追溯到 Alain Colmerauer。

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

将less/2 重写为less/2 和less2/2 类似于表格重写。您插入一个存根并重命名子句头。但是主体中的递归调用没有被重写，然后再次调用存根。

你现在变得坚定：

?- less(s(s(0)), s(s(s(0)))).
true.

?- less(X, Y), X = s(s(0)), Y = s(s(s(0))).
X = s(s(0)),
Y = s(s(s(0))).

有时甚至是failfastness和truefastness：

?- less(s(s(_)), s(0)).
false.

?- less(s(0), s(s(_))).
true.

一些 Prolog 系统甚至提供 table/1 like 指令，因此您无需进行重写，只需声明即可。一种这样的系统是 SICStus Prolog。在 SICStus Prolog 中，感谢block/1 directive，

你只会写：

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

对于 1980 年代的论文，例如：

在 WAM 中实现差异和冻结
Mats Carlsson - 1986 年 12 月 18 日
http://www.softwarepreservation.com/projects/prolog/sics/doc/Carlsson-SICS-TR-86-12.pdf/view

【讨论】：