prolog - 序言-无限法则

Question

我有下一条规则

% Signature: natural_number(N)/1
% Purpose: N is a natural number.
natural_number(0).
natural_number(s(X)) :-
   natural_number(X).

ackermann(0, N, s(N)). % rule 1
ackermann(s(M),0,Result):-
   ackermann(M,s(0),Result). % rule 2
ackermann(s(M),s(N),Result):-
   ackermann(M,Result1,Result),
   ackermann(s(M),N,Result1). % rule 3

查询是: ackermann (M,N,s(s(0)))。

现在，据我了解，在第三次计算中，我们得到了无限搜索(失败分支)。我检查了一下，然后得到了一个有限的搜索(失败分支)。

我将解释:首先，我们得到M = 0，N = s(0)的替换(规则1-成功!)。在第二个中，我们得到了M = s(0)，N = 0的替换(规则2-成功!)。但是现在呢？我尝试匹配M = s(s(0))N = 0，但是得到了 有限搜索-失败分支。为什么编译器不写我“失败”。

谢谢你。

Answer 1

很难确切地理解汤姆在这里要问什么。可能期望谓词 natural_number/1 某种程度上影响 ackermann/3 的执行。它不会。后者谓词纯粹是递归的，不会产生依赖 natural_number/1 的子目标。

当为 ackermann/3 定义了所示的三个子句时，目标是:
?- ackermann(M,N,s(s(0))).
使SWI-Prolog查找(回溯)Tom报告的两个解决方案，然后进行无限递归(导致“Out of Stack”错误)。我们可以确定，此无限递归涉及为 ackermann/3 给出的第三子句(根据汤姆在代码中的注释，规则3)，因为在缺少该子句的情况下，我们只会得到两个公认的解决方案，然后是显式失败:

M = 0,
N = s(0) ;
M = s(0),
N = 0 ;
false.

在我看来，Tom要求解释为什么将提交的查询更改为设置 M = s(s(0))和 N = 0的查询，从而产生有限搜索(找到一个解决方案，然后在回溯时失败)，这与上一个查询产生的无限递归一致。我的怀疑是，对于Prolog引擎尝试回溯(针对原始查询)有误解，因此我将对此进行深入研究。希望汤姆能解决这个问题，但让我们看看是否可以解决。诚然，我的处理方式比较罗word，但Prolog执行机制(子目标的统一和解决)值得研究。

[ 已添加:谓词与著名的 Ackermann function有着明显的联系，后者是完全可计算的，但不是原始递归的。该函数以快速增长而著称，因此我们在声明无限递归时要小心，因为也可以进行很大但有限的递归。但是，第三个子句将其两个递归调用的顺序与我执行的顺序相反，并且这种逆转似乎在我们逐步遍历下面的代码时发现的无限递归中起着至关重要的作用。

提交最高目标 ackermann(M,N,s(s(0)))后，SWI-Prolog会尝试为 ackermann/3 定义的子句(事实或规则)，直到找到其“头”与给定查询一致的子句。 Prolog引擎作为第一个子句看起来并不遥远，这是事实:
ackermann(0, N, s(N)).
将统一，将 M = 0和 N = s(0)绑定(bind)在一起，这已被描述为首次成功。

如果要求回溯，例如通过用户输入分号，Prolog引擎将检查是否存在满足该第一条款的替代方法。那没有。然后，Prolog引擎将继续按照给定顺序尝试 ackermann/3 的以下子句。

同样，搜索也不必走得太远，因为第二子句的头部也与查询统一。在这种情况下，我们有一条规则:
ackermann(s(M),0,Result) :- ackermann(M,s(0),Result).
统一查询和此规则的开头会产生 绑定(bind)，即绑定(bind)，即查询中使用的变量。就上述规则中使用的变量而言，M = s(0)和N = 0。请注意，统一通过术语作为调用参数的出现来匹配术语，并且不会将跨越查询/规则边界重用的变量名称视为表示身份。

因为此子句是一条规则(具有主体和头部)，所以统一只是尝试成功的第一步。现在，Prolog引擎尝试出现在此规则主体中的一个子目标:
M = 0
请注意，此子目标来自于用统一值Result = s(s(0))和ackermann(0,s(0),s(s(0))).替换规则中使用的“本地”变量。 Prolog引擎现在正在递归调用谓词 ackermann/3 ，以查看是否可以满足此子目标。

作为 ackermann/3的第一个子句(事实)，可以以明显的方式进行统一(实际上，该子句中使用的变量的方式与以前基本相同)。因此(在此递归调用成功之后)，我们在外部调用(顶级查询)中获得了第二个成功的解决方案。

如果用户要求Prolog引擎再次回溯，它将再次检查是否可以以其他方式满足当前子句( ackermann/3 的第二个子句)。不能，因此搜索继续到谓词 ackermann/3 的第三个(也是最后一个)子句:

ackermann(s(M),s(N),Result) :-
    ackermann(M,Result1,Result),
    ackermann(s(M),N,Result1).

我将要解释的是，这种尝试确实会产生无限递归。当我们用此子句的开头统一顶级查询时，我们得到的参数绑定(bind)可以通过将查询中的术语与标题中的术语对齐来清楚地理解:

   query     head
     M       s(M)
     N       s(N)
   s(s(0))  Result

请记住，在查询中与规则中的变量具有相同名称的变量不会限制统一，因此可以将这三个术语统一。查询M = 0将是head Result = s(s(0))，这是一个复合词，涉及仿函数M应用于应用于出现在头部的某些未知变量s(M)。查询s也是一样。到目前为止，唯一的“地面”术语是出现在规则标题(和正文)中的M变量，该变量已与查询中的N绑定(bind)。

现在，第三个子句是一条规则，因此Prolog引擎必须继续尝试满足该规则主体中出现的子目标。如果将头部统一中的值替换为主体，则要满足的第一个子目标是:
Result
我要指出的是，在这里我使用了子句的“局部”变量，除了用统一绑定(bind)的值代替了s(s(0))之外。现在注意，除了用变量名ackermann(M,Result1,s(s(0))).和替换原始顶级查询的Result之外，我们在此子目标中的要求与原始查询相同。当然，这可能是我们可能要进入无限递归的重要线索。

但是，还需要进行更多讨论，以了解为什么我们没有得到进一步的解决方案的报告!这是因为第一个子目标的第一个成功(如先前所述)将需要N和Result1，然后Prolog引擎必须继续尝试该子句的第二个子目标:
M = 0
不幸的是，这个新的子目标没有与 ackermann/3 的第一个子句(事实)统一。它确实与第二个子句的开头统一，如下所示:

   subgoal     head
     s(0)      s(M)
      N         0
     s(0)     Result

但这会导致一个子目标(来自第二个子句的主体):
Result1 = s(0)
这与第一或第二子句的标题不统一。它还与第三个子句的开头(要求第一个参数的格式为ackermann(s(0),N,s(0)).)不统一。因此，我们在搜索树中遇到了故障。 Prolog引擎现在回溯以查看是否可以以其他方式满足第三条子句主体的第一个子目标。众所周知，它可以是(因为此子目标与原始查询基本相同)。

现在，第二个解决方案的ackermann(0,s(0),s(0)).和s(_)导致了第三条子句主体的第二个子目标的实现:
M = s(0)
虽然这与谓词的第一个子句(事实)不统一，但与第二个子句的开头统一:

   subgoal     head
   s(s(0))     s(M)
      N         0
      0       Result

但是为了成功，Prolog引擎还必须满足第二个子句的主体，该子句现在为:
Result1 = 0
我们可以很容易地看到，这不能与 ackermann/3 的第一或第二子句的标题统一。可以与第三子句的标题统一:

  sub-subgoal  head(3rd clause)
    s(s(0))       s(M)
      s(0)        s(N)
       0         Result

现在应该熟悉的是，Prolog引擎会检查第三子句主体的第一个子目标是否可以满足，这相当于该子子目标:
ackermann(s(s(0)),N,0).
这无法与第一个子句(事实)统一，但与第二个子句的开头结合ackermann(s(s(0)),s(0),0).，ackermann(s(0),Result1,0).和M = 0统一，并(通过熟悉的逻辑)生成sub-sub-sub-subgoal:
Result1 = 0
由于这不能与三个子句的任何一个都统一，因此失败了。此时，Prolog引擎使用第三子句回溯到尝试满足上述子子目标。统一是这样的:

  sub-sub-subgoal  head(3rd clause)
       s(0)             s(M)
      Result1           s(N)
         0             Result

然后Prolog引擎的任务是满足从第三子句的正文的第一部分派(dispatch)生的子子目标:
Result = 0
但这不会与这三个条款中的任何一个统一。对以上子子目标的解决方案的搜索失败。 Prolog引擎一直回溯到它最初试图满足原始顶级查询所调用的第三子句的第二子目标的位置，因为现在这已经失败了。换句话说，它试图用第三个子句的第一个子目标的前两个解决方案来满足它，您会记得，除了变量名与原始查询的更改之外，该本质上是相同的:
ackermann(0,0,0).
上面我们看到的是，此子目标的解决方案与 ackermann/3 的第一和第二子句中的原始查询重复，不允许第三子句的正文的第二子目标成功。因此，Prolog引擎尝试查找满足第三条款的解决方案。但是很显然，现在这将进入无限递归，因为该第三子句将在其头部统一，但是该第三子句的主体将重复我们刚刚进行的搜索。因此，Prolog引擎现在不断进入第三子句的主体。