prolog 一元数 - 评估表达式

Question

我正在尝试了解 Prolog，但我遇到了以下情况。我用以下方式定义了自然数（一元）：

n(0).
n(s(X)) :- nat(X).

这意味着0是0，s(0)是1，s(s(0))是2等等......

然后我定义谓词添加：

add(0, Y, Y) :- nat(Y).
add(s(X), Y, s(Z)) :-
   add(X, Y, Z).

将两个一元数和结果存储添加到 Z。

现在我有以下谓词“测试”来证明我的问题：

test(s(0),0).

然后在解释中输入：

add(s(0),0,R). %result: R = s(0), which is correct

那我试试：

test(add(s(0),0,R), 0).

所以第一个参数应该导致 R = s(0)，第二个参数是零，所以整个表达式应该被评估为 true，但 prolog 说 false。我想这与这一点有关，即“测试”谓词中的 add(s(0),0,R) 不会评估我的想法。谁能向我解释一下，或者最终提供一些描述这种行为的链接？谢谢你的帮助！ 干杯。

Answer 1

不，prolog 不会像您想象的那样工作。 当你问

?- test(add(s(0),0,R), 0).

prolog 试图找到一个匹配的子句。但是，您的数据库中没有匹配的子句，因为s(0) 与add(s(0),0,R) 不匹配。两个结构只有在具有相同函子时才能匹配。

s(0) 具有函子 s，而 add(s(0),0,R) 具有函子 add。