recursion - Prolog peano 数字差/减法
问题描述
我正在尝试计算“Peano numbers”(Recursive definition of natural numbers represented as s(0), s(s(0)) etc.
)的差异,但我有点被一个问题困住了。
减法的定义如下:
s(X) - 0 = s(X)
s(X) - s(s(X)) = 0
s(X) - s(X) = 0
s(s(X)) - s(X) = s(0)
0 - s(X) = 0
这是我当前的代码:
nat(0).
nat(s(X)) :- nat(X).
% sub/3
% Subtracts right operand from left operand and returns difference
sub(0, _, 0).
sub(X, 0, X).
sub(s(X), s(Y), X) :-
sub(X,Y,X).
我背后的思考过程:
因为我真的不需要递归地增加差异,所以我可以使用X
递归后剩下的最后一个作为结果。
出于某种原因,以下问题有效:
?- sub(s(0), s(0), X)。
X = 0 ;
但是这个没有:
?- sub(s(s(0)), s(s(0)), X)。
错误的。
谁能指出我的错误或提出更好的方法来实现子程序?
这可能是初学者的错误,因为我真的没有做太多。对不起,如果是这样的话。
//编辑 这就是我解决它的方法
sub(X, 0, X).
sub(0, _, 0).
% not sure why I didn't test this before, thought I did.
sub(s(X), s(Y), Diff) :-
sub(X,Y,Diff).
解决方案
sub(s(X), s(Y), X) :- sub(X,Y,X).
说
You can prove that s(X)-s(Y) = X
if you can prove that X-Y = X
这有点奇怪。那里应该有第三个变量,Z
。
Prolog 试图证明(使真实)
sub(s(s(0)), s(s(0)), X).
如果可以的话
sub(s(0),s(0),s(0)).
因为规则的右侧是通过定位X=s(0)
和Y=s(0)
模式匹配 LHS 来设置的。
试图sub(s(0),s(0),s(0))
再次证明这一点意味着使用规则(没有其他适用),定位X=0
, Y=0
, X=s(0)
. 但X
不能同时是0
和s(0)
。僵局!false
.
推荐阅读
- native-web-component - 如何为插槽中的所有插槽表重复外部 DOM?
- javascript - 如何显示将 express.js 开发服务器公开给网络中其他机器的 IP 地址?
- azure - 用于启动 Azure 虚拟机的可执行文件
- python - 依赖于 dlib 的 python 可执行文件不起作用
- php - 我想在 php 中计算上传文件中的重复单词我怎么能得到它
- react-native - 在取消链接所有软件包后,在 react-native 升级时,它会再次手动链接以下模块
- json - 如何序列化和无法序列化的对象?
- swift5 - 进程 kill() 返回意外错误 1 Xcode 11.2 - iOS 13.2 - Swift 5
- laravel - 在 Laravel 的视图中使用 2 个控制器函数
- android - 我正在为使用 ConstraintLayout 和 Barrier 的 Android 布局而苦苦挣扎