当您调用目标add(succ(succ(succ(0))), succ(succ(0)), R)
并且 Prolog 尝试使用 head 执行子句时add(succ(X),Y,succ(Z))
,就会发生统一。统一是 Prolog 的核心概念之一,理解它很重要。统一也是操作员执行的=
操作。执行子句头部时发生的情况与执行以下等效查询时发生的情况完全相同:
?- add(succ(succ(succ(0))), succ(succ(0)), R) = add(succ(X),Y,succ(Z)).
重要的是要理解统一不仅仅是“拆包”或“构建”术语,而是两者同时进行。
它可以从术语中“提取”信息:
?- X = f(a), Y = f(Z), X = Y.
X = Y, Y = f(a),
Z = a.
在这里,我们发现这a
是 中f
函子的参数X
。
它可以“构造”术语:
?- X = f(Y), Y = g(h).
X = f(g(h)),
Y = g(h).
在这里,我们将术语“插入”g(h)
到Y
.X
它也可以同时对多个术语进行:
?- X = f(a, B), Y = f(A, b), X = Y.
X = Y, Y = f(a, b),
B = b,
A = a.
这里统一“解开”了这两个f
术语,然后在每个术语中“填充”了一个洞。
现在,有了这些知识,你的例子中的统一有什么作用?
?- add(succ(succ(succ(0))), succ(succ(0)), R) = add(succ(X),Y,succ(Z)).
R = succ(Z),
X = Y, Y = succ(succ(0)).
特别是,当succ(succ(succ(0)))
与 统一时succ(X)
, this 将绑定X
到succ(succ(0))
。不受整个术语的约束,X
而仅与“内部”部分有关。这就是从论点中删除一级的原因。succ(succ(succ(0)))
succ