Prolog继承符号表示不完整的结果和无限循环

Question

我开始学习Prolog,并首先了解了继承符号.

这就是我在Prolog中发现编写Peano公理的地方.

参见PDF的第12页:

sum(0, M, M).
sum(s(N), M, s(K)) :-
    sum(N,M,K).

prod(0,M,0).
prod(s(N), M, P) :-
    prod(N,M,K),
    sum(K,M,P).

我把乘法规则放到了Prolog中.然后我做查询:

?- prod(X,Y,s(s(s(s(s(s(0))))))).

这意味着基本上找到6的因子.

结果如下.

X = s(0),
Y = s(s(s(s(s(s(0)))))) ? ;
X = s(s(0)),
Y = s(s(s(0))) ? ;
X = s(s(s(0))),
Y = s(s(0)) ? ;
infinite loop

这个结果有两个问题:

1. 并非所有结果都显示,请注意结果X = 6,Y = 1缺失.
2. 它不会停止,除非我按Ctrl + C然后选择中止.

所以...我的问题是:

1. 这是为什么？我尝试转换"prod"和"sum".结果代码给了我所有结果.再说一遍,为什么？它仍然是死循环.
2. 如何解决？

我在无限循环中阅读了另一个答案.但我很感激有人根据这个场景做出回答.这对我很有帮助.

Answer 1

如果你想深入研究终止属性,那么使用后继算法的程序是一个理想的研究对象:你先前知道它们应该描述什么,所以你可以专注于更多的技术细节.您需要了解几个概念.

通用终止

解释它的最简单方法是考虑Goal, false.这将终止iff Goal普遍终止.那就是:查看跟踪器是最无效的方式 - 它们只向您显示一条执行路径.但你需要立刻了解所有这些!当你想要普遍终止时,也永远不会看答案,它们只会分散你的注意力.你已经看到了上面的内容:你有三个简洁而正确的答案,只有你的程序循环.所以更好地"关闭"答案false.这消除了所有分心.

失败片

您需要的下一个概念是失败切片.采用纯粹的单调逻辑程序并投入一些目标false.如果生成的故障片没有终止(普遍),原始程序也不会终止.在你的例子中,考虑:

prod(0,M,0) :- false.
prod(s(N), M, P) :-
    prod(N,M,K), false,
    sum(K,M,P).

这些false目标有助于删除程序中不相关的装饰:其余部分向您显示清楚,为什么prod(X,Y,s(s(s(s(s(s(0))))))).不终止.它不会终止,因为该片段根本不关心P!你希望第三个参数有助于prod/3终止,但是片段告诉你这一切都是徒劳的,因为P任何目标都不会发生.不需要繁琐的示踪剂.

通常,找到最小的故障切片并不容易.但是一旦找到了它,就可以确定它的终止或非终止属性.一段时间后,您可以使用您的直觉来想象切片,然后您可以使用您的理由来检查切片是否相关.

关于失败切片概念的显着之处在于:如果要改进程序,则必须在上面片段中可见的部分修改程序!只要你不改变它,问题就会持续存在.因此,故障切片是程序中非常重要的一部分.

终止推断

这是您需要的最后一件事:像cTI这样的终止推理器(或分析器)将帮助您快速识别终止条件.看看推断的终止条件prod/3和改进prod2/3 了!

编辑:由于这是一个家庭作业问题,我还没有发布最终的解决方案.但为了说清楚,以下是迄今为止获得的终止条件:

    prod(A,B,C)terminates_if b(A),b(B).
    prod2(A,B,C)terminates_if b(A),b(B);b(A),b(C).

所以新prod2/3的严格要比原来的程序好!

现在,您可以找到最终的程序.终止条件是:

   prod3(A,B,C)terminates_if b(A),b(B);b(C).

首先,尝试找到故障切片prod2(A,B,s(s(s(s(s(s(0)))))))!我们希望它终止,但它仍然没有.所以采取该程序并手动添加false目标!剩下的部分会告诉你钥匙!

作为最后的提示:您需要添加一个额外的目标和一个事实.

编辑:根据请求,这是失败切片prod2(A,B,s(s(s(s(s(s(0))))))):

prod2(0,_,0) :- false.
prod2(s(N), M, P) :-
   sum(M, K, P),
   prod2(N,M,K), false.

sum(0, M, M).
sum(s(N), M, s(K)) :- false,
    sum(N,M,K).

请注意显着简化的定义sum/3.它只说:0加任何东西都是什么.不再.因此,即使是更专业化的prod2(A,0,s(s(s(s(s(s(0)))))))意志循环,prod2(0,X,Y)优雅地终止...

Answer 2

第一个问题(为什么)很容易发现,特别是如果知道左递归.sum(A,B,C) 结合当C A和B 被结合,但原来的程序PROD(A,B,C)不使用绑定,以及不是与静止A,B未结合的递归.

如果我们交换sum,prod我们从sum中获得2个有用的绑定用于递归调用:

sum(M, K, P)

现在M被绑定,并将用于终止左递归.我们可以交换N和M,因为我们知道产品是可交换的.

sum(0, M, M).
sum(s(N), M, s(K)) :-
    sum(N, M, K).

prod3(0, _, 0).
prod3(s(N), M, P) :-
    sum(M, K, P),
    prod3(M, N, K).

注意,如果我们交换M,K(即sum(K,M,P)),当用P未知调用prod3时,我们再次有一个非终止循环,但总之.

?- prod3(X,Y,s(s(s(s(s(s(0))))))).
X = s(s(s(s(s(s(0)))))),
Y = s(0) ;
X = s(s(s(0))),
Y = s(s(0)) ;
X = s(s(0)),
Y = s(s(s(0))) ;
X = s(0),
Y = s(s(s(s(s(s(0)))))) ;
false.

OT我对cTI报告感到困惑:prod3(A,B,C)终止_if b(A),b(B); b(A),b(C).