如何解决Pure Prolog Peano Number 公寓
让我们假设有带 dif/2 的 pure_2 Prolog 和不带 dif/2 的 pure_1 Prolog。我们能不能意识到 值的 Peano 分离度,即 Peano 数字,不使用 dif/2?因此,让我们假设我们在 pure_2 Prolog 中有这样的 Peano 分离:
/* pure_2 Prolog */
neq(X,Y) :- dif(X,Y).
我们能否用更纯的定义替换 neq(X,Y),即来自不使用 dif/2 的 pure_1 Prolog?所以我们有一个终止的 neq/2 谓词可以决定皮亚诺数的不等式?那么它的定义是什么?
/* pure_1 Prolog */
neq(X,Y) :- ??
解决方法
使用 this comment 中的 less
:
less(0,s(_)).
less(s(X),s(Y)) :- less(X,Y).
neq(X,Y) :- less(X,Y); less(Y,X).
,
我想到了其他一些东西,它源自 Peano Axioms 中的两个,这也是 Robinson 算术的一部分。第一个公理已经是一个讨论分离的 Horn 子句:
∀x(0 ≠ S(x))
∀x∀y(S(x) = S(y) ⇒ x = y)
对第二个公理应用对位给出。
公理现在是一个讨论分离的 Horn 子句:
∀x∀y(x ≠ y ⇒ S(x) ≠ S(y))
现在我们可以编写一些 Prolog 代码了。
添加一些对称性,我们得到:
neq(0,s(_)).
neq(s(_),0).
neq(s(X),s(Y)) :- neq(X,Y).
以下是一些示例查询。谓词是否留下选择
点取决于 Prolog 系统。我得到:
SWI-Prolog 8.3.15(一些选择点):
?- neq(s(s(0)),s(s(0))).
false.
?- neq(s(s(0)),s(0)).
true ;
false.
Jekejeke Prolog 1.4.6(无选择点):
?- neq(s(s(0)),s(s(0))).
No
?- neq(s(s(0)),s(0)).
Yes
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。