logic - 序言 - 为什么这个奇怪的痕迹

Question

这是序言代码(我有点遵循)。

len([],0).
len([_|T],N) :- len(T,X), N is X+1.

这是它的跟踪(我正在运行 linux，swi)

    [trace]  ?- len([d,f,w,c],X).
   Call: (7) len([d, f, w, c], _G314) ? 
   Call: (8) len([f, w, c], _L182) ? 
   Call: (9) len([w, c], _L201) ? 
   Call: (10) len([c], _L220) ? 
   Call: (11) len([], _L239) ? 
   Exit: (11) len([], 0) ? 
^  Call: (11) _L220 is 0+1 ? 
^  Exit: (11) 1 is 0+1 ? 
   Exit: (10) len([c], 1) ? 
^  Call: (10) _L201 is 1+1 ? 
^  Exit: (10) 2 is 1+1 ? 
   Exit: (9) len([w, c], 2) ? 
^  Call: (9) _L182 is 2+1 ? 
^  Exit: (9) 3 is 2+1 ? 
   Exit: (8) len([f, w, c], 3) ? 
^  Call: (8) _G314 is 3+1 ? 
^  Exit: (8) 4 is 3+1 ? 
   Exit: (7) len([d, f, w, c], 4) ? 
X = 4.

我知道序言会沿着这些“树”运行，但我无法弄清楚为什么变量的增量仅在退出时才完成 - 对这一机制的任何解释吗？

非常感谢!

Answer 1

这样做的原因是，N is X+1 是谓词的最后一部分。

可以这样想:要计算N is X+1，我们需要知道X的值，它是通过调用len( T，X)。但是计算 X 的过程需要再次调用 len，一直到最终得到一个空列表的情况。

此时列表长度已知，即 0。因此该值被“返回”。只有这样0+1才能计算并“返回”。然后是1+1。等等

换个方式思考，观察对于任意两个谓词 a 和 b，a, b当且仅当 a 和 b 都为 true 时，才会产生 true。在 Prolog 中，仅当已知 a 为 true 时才会计算 b(否则计算 b 就没有意义，因为结果已知是假的)。

因此，所有添加都是在递归调用 len 之后完成的。