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))).

甚至有时会出现不稳定性和真实性:

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