Prolog终止域:我怎么知道哪些问题会返回有限数量的答案？

Question

假设我有一个prolog程序来连接这样的列表:

concat([],X,X).
concat([Head|Tail],X,[Head|R]) :- concat(Tail,X,R).

我怎么知道哪些问题会返回有限数量的答案？例如,问

concat(X,Y,[1,2,3,4]).

将返回有限解集:

X = [],
Y = [1, 2, 3, 4] ;
X = [1],
Y = [2, 3, 4] ;
X = [1, 2],
Y = [3, 4] ;
X = [1, 2, 3],
Y = [4] ;
X = [1, 2, 3, 4],
Y = [] ;
false.

在提问时

concat(X,[2,3],Z).

将返回一组无限的解决方案:

X = [],
Z = [1, 2, 3] ;
X = [_G24],
Z = [_G24, 1, 2, 3] ;
X = [_G24, _G30],
Z = [_G24, _G30, 1, 2, 3] ;
X = [_G24, _G30, _G36],
Z = [_G24, _G30, _G36, 1, 2, 3] ;
X = [_G24, _G30, _G36, _G42],
Z = [_G24, _G30, _G36, _G42, 1, 2, 3] ;
X = [_G24, _G30, _G36, _G42, _G48],
Z = [_G24, _G30, _G36, _G42, _G48, 1, 2, 3] ;
X = [_G24, _G30, _G36, _G42, _G48, _G54],
Z = [_G24, _G30, _G36, _G42, _G48, _G54, 1, 2, 3]

等等(基本上,每个可能的列表以[1,2,3]结尾.

那么如何判断逻辑程序中哪些问题会结束？

Answer 1

您正在询问如何确定逻辑程序的终止和非终止属性 - 这里意味着纯粹的,单调的Prolog程序.有一个好消息:是的,有很多技术可以找出这些属性并附带很多有用的概念.

但在进入任何细节之前,请记住,无法为所有查询回答您的问题.也就是说,有些查询我们无法比实际执行查询更好地确认终止.但是不要让你被诸如不可判断之类的可怕言辞所吓倒.他们在这里回避焦虑.就像旧的海图一样 展示了像红海蛇一样可怕的怪物.毫无疑问,海上存在问题:天气,营养不良,航行,叛变,海盗,瘟疫,死水,冰山,地雷......你说出来.但是,遇到海怪的风险是可控的.

如今,我们拥有自己的海怪,避开了许多聪明的头脑来攻击有趣的问题.几十年来终止的不可判断性就是其中之一.在过去的二十年里,情况变得更好了.所以:不要害怕!

首先要考虑的是逻辑程序要描述的实际关系.你甚至不需要一个具体的程序来回答这个问题.想象一下这种关系.首先,询问有多少解决方案.如果有很多,那么你就完成了这一部分,因为没有固有的原因你的程序无法终止.(在您的示例中,一般关系包含无限多个解决方案:只需看到第三个参数中列表的长度无限多.)

如果有无限多,请尝试查找有限的查询子集.(在你的例子中,如果第三个参数是基础的,那么只有有限的解决方案.如果第一个参数和第二个参数是地面的话,请注意.但是,请注意,如果只有第一个参数被研磨,情况并非如此!)

另一个正交方向是考虑解决方案在Prolog中如何表示为答案的方式.一些无限的解决方案可以用有限的答案紧凑地表示.在约束的情况下,这变得特别有趣.(在你的例子中,考虑连接[]和[X].这里,第三个参数有无限多个解决方案,但它们都由一个答案替换代表A3 = [X].)

基于上述考虑,我们粗略估计了我们对逻辑程序的期望:如果查询的解决方案集只能由无限的答案集表示,则程序不得终止.但是,如果解决方案可以由有限多个答案表示,则具体程序可能会终止.唉,为了保证程序实际终止,我们需要进一步挖掘并查看实际程序.

如果您现在查看您的程序,您可能会发现与预期关系存在一些差异.在您的示例中,查询concat([],[],[])失败,但它应该成功.但也concat([],nonlist,L)成功了.前者绝对是一个错字,后者是一种通常被认为是可接受的概括.

要了解具体查询的终止属性,请考虑目标Query, false.通过这种方式,您可以专注于相关属性,id est,终止并忽略不相关的属性,如找到的具体解决方案.

您现在可以查阅具体程序以确定程序的终止属性.考虑cTI,它确实推断了程序的终止和非终止属性.以这种方式,可以确定推断的属性是否是最佳的.

另一种方法是使用失败片来确定程序的非终止片段.有关更多信息,请参阅此类答案.