问题描述
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中的 S(选择规则)a>,一个可以追溯到 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))).
甚至有时会出现不稳定性和真实性:
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 中 diff 和 freeze 的实现
Mats Carlsson - 1986 年 12 月 18 日
http://www.softwarepreservation.com/projects/prolog/sics/doc/Carlsson-SICS-TR-86-12.pdf/view
这篇关于Peano算术中的“less/2"关系的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持!