Peano算术中的`less/2`关系 [英] `less/2` relation in Peano arithmetic

问题描述

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`关系的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！