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

Question

皮亚诺算术中的这个小于谓词

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% 的纯净。 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类似于表格重写。您插入一个存根并重命名子句头。但是body中的递归调用并没有被改写，而是再次调用stub

你现在获得了坚定：

?- 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 directive、

你只会写：

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

有关 1980 年代的论文，请参见示例：

WAM 中 dif 和 freeze 的实现
马茨·卡尔森 - 1986 年 12 月 18 日
http://www.softwarepreservation.com/projects/prolog/sics/doc/Carlsson-SICS-TR-86-12.pdf/view

`less/2` relation in Peano arithmetic