prolog - 为什么这个奇怪的痕迹

Question

这是prolog代码(我跟着它).

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.

我知道prolog会运行这些"树",但是我很难弄清楚为什么变量的增量只在它退出时才会完成 - 这个机制的解释是什么？

非常感谢!

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产生IFF既真a且b是真实的.在Prolog中,b只有在知道它a是真的时才会被评估(否则评估没有意义b,因为已知结果为假).

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