问题描述
Peano 算术中的这个小于谓词
This less-than predicate in Peano arithmetic
less(0, s(_)).
less(s(X), s(Y)) :- less(X, Y).
循环时
?- less(X, Y), X=s(0), Y=0.
有没有更好的方法来编写 less/2(仅使用 Horn 子句)?
Is there a better way to write less/2 (using Horn clauses only)?
推荐答案
你可以使用when/2.使它不再是一个无限枚举的谓词，并且仍然保持 100% 的纯正.when/2 修改SLD-Resolution，一个可以追溯到 Alain Colmerauer 的想法.
You can use when/2. Making it not anymore an infinitely enumerating predicate and still keeping it 100% pure. The when/2 modifies the S (selection rule) in SLD-Resolution, an idea that can be traced back to 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 类似于表格重写.您插入一个存根并重命名子句头.但是主体中的递归调用没有被重写，然后再次调用存根.
The rewriting of less/2 into less/2 and less2/2 is similary like tabling rewriting. You insert a stub and rename the clause head. But the recursive call in the body is not rewritten, is then a call to the stub again.
你现在变得坚定:
?- 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:
And even failfastness and truefastness sometimes:
?- less(s(s(_)), s(0)).
false.
?- less(s(0), s(s(_))).
true.
一些 Prolog 系统甚至提供了一个类似 table/1 的指令，这样你就不需要重写，只需要声明.一种这样的系统是 SICStus Prolog.在 SICStus Prolog 中，感谢 block/1指令,
Some Prolog systems even provide a table/1 like directive, so that you don't need to do the rewriting, only make the declaration. One such system is SICStus Prolog. In SICStus Prolog, thanks to the block/1 directive,
你只会写:
:- block less(-,?), less(?,-).
less(0, s(_)).
less(s(X), s(Y)) :- less(X, Y).
对于 1980 年代的论文，例如:
For a 1980's Paper see for example:
在 WAM 中实现差异和冻结
Mats Carlsson - 1986 年 12 月 18 日
http://www.softwarepreservation.com/projects/prolog/sics/doc/Carlsson-SICS-TR-86-12.pdf/view
这篇关于Peano算术中的`less/2`关系的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！