prolog - Peano算术中的`less/2`关系

Question

Peano算术中的这个小于谓词

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

循环时

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

有没有更好的写作方式less/2（仅使用 Horn 子句）？

Answer 1

您可以使用when/2. 使它不再是一个无限枚举的谓词，并且仍然保持 100% 的纯正。修改了SLD-Resolution中的when/2S（选择规则），这个想法可以追溯到 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/2intoless/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 的指令，这样你就不需要重写，只需要声明。一种这样的系统是 SICStus Prolog。在 SICStus Prolog 中，感谢block/1 指令，

你只会写：

:- 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