6

我有下一个规则

% 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,但它有一个有限搜索 - 失败分支。为什么编译器不写我“失败”。

谢谢你。

4

2 回答 2

8

很难理解汤姆在这里问的是什么。也许有人期望谓词natural_number/1以某种方式影响ackermann/3的执行。它不会。后一个谓词是纯递归的,并且不产生依赖于natural_number/1的子目标。

当为ackermann/3定义显示的三个子句时,目标:

?- ackermann(M,N,s(s(0))).

导致 SWI-Prolog 找到(回溯)Tom 报告的两个解决方案,然后进入无限递归(导致“Out of Stack”错误)。我们可以肯定,这种无限递归涉及为ackermann/3给出的第三个子句(根据 Tom 在代码中的注释的规则 3),因为在没有它的情况下,我们只能得到两个公认的解决方案,然后是显式失败:

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

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

[补充:谓词与著名的Ackermann 函数 有明显的联系,该函数是完全可计算的,但不是原始递归的。这个函数以快速增长而闻名,所以我们在声明无限递归时需要小心,因为一个非常大但有限的递归也是可能的。然而,第三个子句将其两个递归调用的顺序与我所做的相反,并且这种反转似乎在我们在逐步执行下面的代码时发现的无限递归中发挥了关键作用。]

ackermann(M,N,s(s(0)))当提交顶级目标时,SWI-Prolog 会尝试为ackermann/3定义的子句(事实或规则),直到找到其“头部”与给定查询相结合的子句。Prolog 引擎没有远看作为第一个子句,这个事实:

ackermann(0, N, s(N)).

将统一、绑定M = 0N = s(0)已经描述为第一次成功。

如果请求回溯,例如通过用户键入分号,Prolog 引擎会检查是否有替代方法来满足第一个子句。那没有。然后 Prolog 引擎继续按照给定的顺序尝试ackermann/3的以下子句。

同样,搜索不必走得太远,因为第二个子句的头部也与查询相结合。在这种情况下,我们有一个规则:

ackermann(s(M),0,Result) :- ackermann(M,s(0),Result).

根据查询中使用的变量M = s(0),统一查询和这条规则的头部会产生绑定。就上述规则中使用的变量而言,和。请注意,统一通过它们作为调用参数的外观来匹配术语,并且不考虑跨查询/规则边界重用的变量名称表示身份。N = 0M = 0Result = s(s(0))

因为这个子句是一个规则(有主体也有头),统一只是尝试成功的第一步。Prolog 引擎现在尝试出现在该规则正文中的一个子目标:

ackermann(0,s(0),s(s(0))).

请注意,此子目标来自将规则中使用的“局部”变量替换为统一值M = 0Result = 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).

我将要解释这种尝试确实会产生无限递归。当我们将顶级查询与该子句的头部统一起来时,我们会得到参数的绑定,通过将查询中的术语与头部中的术语对齐,我们可能可以清楚地理解这些参数:

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

请记住,查询中与规则中的变量具有相同名称的变量不限制统一,因此可以统一这三个术语。查询M将是 head s(M),这是一个复合术语,涉及s应用于头部中出现的一些未知变量的函子M。查询同样的事情N。到目前为止,唯一的“基础”术语是Result出现在规则头部(和主体)中的变量,该规则已与s(s(0))查询绑定。

现在第三个子句是一条规则,因此 Prolog 引擎必须继续尝试满足出现在该规则主体中的子目标。如果您将头部统一中的值替换到正文中,则要满足的第一个子目标是:

ackermann(M,Result1,s(s(0))).

让我指出,我在这里使用了子句的“局部”变量,除了我用Result它在统一中绑定的值替换。现在请注意,除了用N变量 name 替换原始顶级查询之外Result1我们只是在询问与此子目标中原始查询相同的事情。当然,这是我们可能即将进入无限递归的重要线索。

但是,需要进行更多讨论才能了解为什么我们没有报告任何进一步的解决方案!这是因为第一个子目标的第一个成功(如前所述)将需要M = 0and Result1 = s(0),然后 Prolog 引擎必须继续尝试子句的第二个子目标:

ackermann(s(0),N,s(0)).

不幸的是,这个新的子目标与ackermann/3的第一个子句(事实)不一致。它确实与第二子句的头部统一,如下:

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

但这会导致一个子目标(来自第二个子句的主体):

ackermann(0,s(0),s(0)).

这与第一个或第二个子句的头部都不统一。它也不与第三个子句的头部统一(它要求第一个参数具有形式s(_))。所以我们在搜索树中遇到了一个失败点。Prolog 引擎现在回溯以查看是否可以以替代方式满足第三子句主体的第一个子目标。正如我们所知,它可以(因为这个子目标与原始查询基本相同)。

现在M = s(0)Result1 = 0第二个解决方案导致第三个子句主体的第二个子目标:

ackermann(s(s(0)),N,0).

虽然这不与谓词的第一个子句(事实)统一,但它确实与第二个子句的头部统一:

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

但是为了成功,Prolog 引擎还必须满足第二个子句的主体,现在是:

ackermann(s(s(0)),s(0),0).

我们可以很容易地看到这不能与ackermann/3的第一个或第二个子句的头部统一。可以与第三小句的头部统一:

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

正如现在应该熟悉的那样,Prolog 引擎检查是否可以满足第三个子句主体的第一个子目标,这相当于这个子子子目标:

ackermann(s(0),Result1,0).

这无法与第一个子句(事实)统一,但确实与第二个子句绑定的头部统一M = 0Result1 = 0并且Result = 0(通过熟悉的逻辑)产生子子子子目标:

ackermann(0,0,0).

由于这不能与三个子句的任何一个头部统一,因此失败了。此时,Prolog 引擎回溯到尝试使用第三个子句来满足上述子子目标。统一是这样的:

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

然后Prolog引擎的任务是满足从第三个子句主体的第一部分派生的这个子子子子目标:

ackermann(0,Result1,0).

但这不会与三个子句中的任何一个子句的头部统一。对上述子子目标的解决方案的搜索以失败告终。Prolog 引擎一直回溯到它第一次尝试满足原始顶级查询调用的第三个子句的第二个子目标的位置,因为现在已经失败了。换句话说,它试图用第三个子句的第一个子目标的前两个解决方案来满足它,你会记得它本质上是相同的,除了变量名称与原始查询的更改:

ackermann(M,Result1,s(s(0))).

我们在上面看到的是这个子目标的解决方案,从ackermann/3的第一个和第二个子句复制原始查询,不允许第三个子句主体的第二个子目标成功。因此,Prolog 引擎试图找到满足第三个子句的解决方案。但很明显,这现在进入了无限递归,因为第三个子句将在其头部统一,但第三个子句的主体将重复我们刚刚进行的相同搜索。因此,Prolog 引擎现在无休止地进入第三个子句的主体。

于 2011-06-26T00:55:23.380 回答
5

让我重新表述您的问题:查询ackermann(M,N,s(s(0))).找到两个解决方案,然后循环。理想情况下,它将在这两个解决方案之后终止,因为没有其他解决方案N并且M其值为s(s(0)).

那么为什么查询不会普遍终止呢?理解这一点可能非常复杂,最好的建议是不要试图理解精确的执行机制。有一个非常简单的原因:Prolog 的执行机制非常复杂,如果您尝试通过单步执行代码来理解它,那么无论如何您很容易误解它。

相反,您可以尝试以下方法:false在程序中的任何位置插入目标。如果生成的程序没有终止,那么原始程序也不会终止。

在你的情况下:

阿克曼(0,N,s(N)):-ackermann(s(M),0,Result):- false ,
    ackermann(M,s(0),Result)。
阿克曼(s(M),s(N),结果):-
   ackermann(M,Result1,Result), false ,
    ackermann(s(M),N,Result1)

我们现在可以删除第一个和第二个子句。而在第三个子句中,我们可以去掉 false 之后的目标。所以如果下面的片段没有终止,那么原始程序也不会终止。

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

该程序现在仅在第一个参数已知时终止。但在我们的案例中,它是免费的......

也就是说:通过考虑程序的一小部分(称为),我们已经能够推断出整个程序的属性。有关详细信息,请参阅本文和网站上的其他文件。

不幸的是,这种推理只适用于不终止的情况。对于终止,事情更复杂。最好的方法是尝试使用cTI 之类的工具来推断终止条件并尝试证明它们的最优性。我已经进入你的程序了,试试修改if看看效果!

如果我们这样做:这个小片段还告诉我们第二个参数不会影响终止1。这意味着,类似的查询ackermann(s(s(0)),s(s(0)),R).也不会终止。交换目标以查看差异...


1 准确地说,与 不统一的术语s(_)会影响终止。想想0。但是任何s(0), s(s(0)), ... 都不会影响终止。

于 2011-06-24T19:18:22.547 回答