在 Prolog 中有列表追加实现 -
append([],X,X).
append([H|T1],X,[H|T2]) :-
append(T1,X,T2).
哪个放弃 -
append([a,b,c],[d,e,f],X).
输出 -
X = [a,b,c,d,e,f].
我想知道它是如何工作的，我试图跟踪函数调用，但我不明白 T2 是列表的尾部，它可以作为 X 的尾部在 append([a,b,c],[d,e,f],X) 调用还没有定义。
你能为我清除这个递归吗？
【问题讨论】：
归结为 Unification 在 Prolog 中的工作方式。基本上：
所以你打电话给：append([a, b, c], [d, e, f], Y) 这是你的第一个目标。请注意，为了便于查看，我将变量名从 X 更改为 Y。
这得和一个事实或一个规则统一起来：让我们看看它是否会和 append([], X, X) 统一起来？
(1) append([a, b, c], [d, e, f], Y)
(2) append([], X, X)
(1) 和 (2) 都具有相同的仿函数（附加），所以这很好，而且它们都有 3 个参数，所以也很好。但要统一每个相应的论点必须统一。因此，(1) 中的第一个列表 [a, b, c] 将尝试与 (2) 中的空列表统一，但它们不能，因为 (1) 中的列表不是空列表。所以统一失败了。
然后我们可以尝试用 append([H|T1],X,[H|T2]) 统一。
(1) append([a, b, c], [d, e, f], Y)
(2) append([H|T1],X,[H|T2])
这一次，(1) 中的列表 [a, b, c] 将尝试与 (2) 中的列表 [H|T1] 统一。为了使这成为可能，变量 H 可以与原子 a (H -> a) 绑定，并且列表 T1 可以与 (1) 中列表的尾部绑定，T1 -> [b, c]。所以第一个论点有效，所以我们拥有的是：
(1) append([a, b, c], [d, e, f], Y)
(2)' append([a, b, c],X,[a|T2])
第二个参数也将统一，因为 X 是一个变量并且可以绑定到任何东西。 X -> [d, e, f] 所以我们有：
(1) append([a, b, c], [d, e, f], Y)
(2)'' append([a, b, c],[d, e, f],[a|T2])
最后最后一个参数统一因为 Y -> [a|T2]。因此，既然它与规则的头部统一，我们需要制定规则的主体：我们现在以append([b, c], [d, e, f], T2) 作为目标。
再次从第一个事实开始，我们寻找这个目标将绑定到的子句。通过上面相同的解释，它不会与第一个子句统一，但会与第二个子句通过绑定统一：H -> b, T1 -> [c], X -> [d, e, f] 和 T2 -> [ b|T2']。
我们的目标是：append([c], [d, e, f], T2')。同样，它不与第一个子句统一，而是通过绑定与第二个子句统一：H -> c, T1 -> [], X -> [d, e, f], T2' -> [c|T2'' ].
现在的目标是：append([], [d, e, f], T2'')。
让我们看看当我们尝试将其与第 1 条统一时会发生什么：
(1) append([], [d, e, f], T2'')
(2) append([],X,X)
两个空列表合并，X -> [d, e, f] 并且因为 T2''->X 然后 T2'' -> [d, e, f]。现在棘手的部分是跟踪到目前为止的递归调用，然后沿着递归返回以查看最终结果。回想一下 T2' -> [c | T2''] 所以 T2' 实际上是 [c, d, e, f]。回想一下 T2 -> [b| T2'] 所以 T2 实际上是 [b, c, d, e, f]。
最后是 Y -> [a|T2] 所以 Y 是 [a, b, c, d, e, f]。由于 Y 是一个外部变量，因此现在显示原始目标已满足。
【讨论】：