Tom*_*Tom 6 prolog successor-arithmetics
我有下一个规则
% 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,但它有一个有限的搜索 - 失败分支.为什么编译器不会写我"失败".
谢谢.
有点难以理解汤姆在这里问的问题.也许有人期望谓词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定义的子句(事实或规则),直到找到其"head"与给定查询统一的子句.Prolog引擎作为第一个条款没有多远,这个事实:
ackermann(0, N, s(N)).
将统一,具有约束力M = 0,N = s(0)并已被描述为第一次成功.
如果要求回溯,例如通过用户输入分号,Prolog引擎会检查是否有另一种方法来满足第一个子句.那没有.然后Prolog引擎继续以给定的顺序尝试ackermann/3的以下子句.
再次搜索不必走远,因为第二个子句的头部也与查询统一.在这种情况下,我们有一个规则:
ackermann(s(M),0,Result) :- ackermann(M,s(0),Result).
统一查询和这个规则的头部产生的绑定M = s(0),N = 0在条件查询中使用的变量.就上述规则中使用的变量而言,M = 0和Result = s(s(0)).请注意,统一通过它们作为调用参数的外观来匹配术语,并且不会将在查询/规则边界中重用的变量名称视为表示身份.
因为这个条款是一个规则(有主体和头部),统一只是尝试成功的第一步.Prolog引擎现在尝试出现在此规则正文中的一个子目标:
ackermann(0,s(0),s(s(0))).
请注意,此子目标来自将规则中使用的"本地"变量替换为统一值,M = 0以及Result = 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),这是一个复合术语,涉及将functor s应用于M头部中出现的某些尚未知的变量.查询也是一样的N.到目前为止唯一的"基础"术语是变量Result出现在规则的头部(和主体)中,它已经s(s(0))从查询中绑定.
现在第三个子句是一个规则,因此Prolog引擎必须继续尝试满足出现在该规则主体中的子目标.如果将头部统一中的值替换为正文,则要满足的第一个子目标是:
ackermann(M,Result1,s(s(0))).
让我指出,我在这里使用了该子句的"局部"变量,除了我已经被Result统一中绑定的值所取代.现在请注意,除了用N变量名替换原始顶级查询之外Result1,我们只是在询问与此子目标中的原始查询相同的内容.当然,这是我们可能即将进入无限递归的一个重要线索.
然而,需要更多的讨论来了解为什么我们没有得到任何进一步的解决方案报告!这是因为第一个子目标的第一次成功(正如之前发现的那样)需要M = 0和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 = 0,Result1 = 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引擎现在无休止地进入第三个条款的主体.
让我重新解释一下你的问题:查询ackermann(M,N,s(s(0))).找到两个解决方案然后循环.理想情况下,它将这两种解决方案后终止,因为没有其他N和M其值s(s(0)).
那么为什么查询不会普遍终止？理解这一点可能非常复杂,最好的建议是不要试图理解精确的执行机制.有一个非常简单的原因:Prolog的执行机制结果是复杂的,如果你试图通过代码来理解它,你很容易误解它.
相反,您可以尝试以下操作:false在程序中的任何位置插入目标.如果生成的程序没有终止,那么原始程序也不会终止.
在你的情况下:
ackermann(0, N, s(N)) :- false.ackermann(s(M),0,Result):- false,ackermann(M,s(0),Result). ackermann(s(M),s(N),Result):- ackermann(M,Result1,Result), false,ackermann(s(M),N,Result1).
我们现在可以删除第一条和第二条规则.在第三条规则中,我们可以在错误后删除目标.因此,如果以下片段没有终止,原始程序也不会终止.
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))...不会影响终止.