谁能解释一下prolog用这个递归程序所做的步骤？

Question

我最近开始学习 prolog，但我在递归规则方面遇到了困难。我理解简单的规则，但是我发现这个例子有问题，我发现一个程序给出了列表中所有元素的总和：

addup([], 0).

addup([FirstNumber | RestOfList], Total) :-
    addup(RestOfList, TotalOfRest),   
    Total is FirstNumber + TotalOfRest.

现在如果我跟踪这个，我会得到以下信息：

[trace]  ?- addup([3, 5, 7], Total).
   Call: (7) addup([3, 5, 7], _G322)
   Call: (8) addup([5, 7], _L1)
   Call: (9) addup([7], _L2)
   Call: (10) addup([], _L3)
   Exit: (10) addup([], 0)    % I understand what it does till here
^  Call: (10) _L2 is 7+0
^  Exit: (10) 7 is 7+0
   Exit: (9) addup([7], 7)
^  Call: (9) _L1 is 5+7
^  Exit: (9) 12 is 5+7
   Exit: (8) addup([5, 7], 12)
^  Call: (8) _G322 is 3+12
^  Exit: (8) 15 is 3+12
   Exit: (7) addup([3, 5, 7], 15)
Total = 15.

我了解前几个步骤；它不断削减并制作新的 TotalOfRest，直到原始列表为空并且与第一个事实相匹配。这使得第三个 TotalOfRest（我称之为 _L3）等于 0。 但是现在呢？ prolog如何使L2等于7 + 0的步骤。我知道prolog开始回溯，但是什么与得出该结论的内容相匹配？道达尔现在是 7 吗？还是像 TotalOfRest 一样，是否存在具有不同值的三个不同 Total？ RestofList 是否仍等于 [] 且 FirstNumber 仍为 7？

所以基本上：prolog 如何从找到 L3 到最终结论？

我对此很陌生，所以如果有人能慢慢地为我解释一下，我将不胜感激！

Answer 1

请注意，您的递归调用引入了一个新变量：

addup([], 0).
addup([FirstNumber | RestOfList], Total) :-
    addup(RestOfList, TotalOfRest),   
    Total is FirstNumber + TotalOfRest.

在每个递归级别，都会创建一个新的TotalOfRest 变量。请注意，较高递归级别的TotalRest 与递归更深的级别不同。

trace 使用变量名会更方便：

[trace]  ?- addup([3, 5, 7], Total).
   Call: (7) addup([3, 5, 7], _Total)
   Call: (8) addup([5, 7], _TotalOfRest1)
   Call: (9) addup([7], _TotalOfRest2)
   Call: (10) addup([], _TotalOfRest3)
   Exit: (10) addup([], 0)
^  Call: (10) _TotalOfRest2 is 7+0
^  Exit: (10) 7 is 7+0
   Exit: (9) addup([7], 7)
^  Call: (9) _TotalOfRest1 is 5+7
^  Exit: (9) 12 is 5+7
   Exit: (8) addup([5, 7], 12)
^  Call: (8) _Total is 3+12
^  Exit: (8) 15 is 3+12
   Exit: (7) addup([3, 5, 7], 15)
Total = 15.

因此，如果执行递归调用，则会创建一个新变量_TotalOfRest1。调用递归完成，直到_TotalOfRest3。现在在那个级别_TotalOfRest3 = 0 设置为0。但是递归中还有一些命令需要解决：Total is FirstNumber + TotalOfRest.。请注意，所有这些Totals 都是局部变量（这也适用于TotalOfRest 和FirstNumber）。因此，在每个级别上都解决了这个问题。请注意，例如递归级别 2 的 Total 实际上是调用者的 _TotalOfRest2。

所以递归看起来像：

addup([3, 5, 7], Total) :-
    % FirstNumber = 3
    % RestOfList = [5, 7]
    % Total = Total
    addup([5,7], _TotalOfRest1) :-
         % FirstNumber = 5
         % RestOfList = [7]
         % Total = _TotalOfRest1
         addup([7], _TotalOfRest2) :-
             % FirstNumber = 7
             % RestOfList = []
             % Total = _TotalOfRest2
             addup([],_TotalOfRest3),
             % resolved to _TotalOfRest3 = 0
             Total is 7 + 0.
             % resolved to Total = 7
         % resolved to _TotalOfRest2 = 7
         Total is 5 + 7.
         % resolved to Total = 12
     % resolved to _TotalOfRest1 = 12
     Total is 3 + 12.
     % resolved to Total = 15
% resolved tot Total = 15

代码部分以粗体书写，您可以看到在每一层都有局部变量，这些变量被接地并传回外部范围。