Prolog 终止域：我如何知道哪些问题会返回有限数量的答案？答案

【问题标题】：Prolog termination domain: How can I know which questions will return a finite number of answers?Prolog 终止域：我如何知道哪些问题会返回有限数量的答案？
【发布时间】：2013-10-01 15:02:42
【问题描述】：

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

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] 结尾。

那么我如何推断逻辑程序上哪些问题会结束？

【问题讨论】：

标签： prolog failure-slice non-termination

【解决方案1】：

你在问如何确定一个逻辑程序的终止和非终止属性——这里指的是一个纯粹的、单调的 Prolog 程序。有一个好消息：是的，有很多技术可以找出这些属性以及很多有用的概念。

但在详细介绍之前，请记住，您的问题无法针对所有查询进行回答。也就是说，有些查询我们无法比实际执行查询更好地确认终止。但是不要让你被诸如不确定性之类的可怕词吓倒。他们来这里是为了回避焦虑。就像old sea-maps 展示可怕的怪物，比如红海蛇。毫无疑问，海上存在问题：天气、营养不良、航行、叛乱、海盗、瘟疫、死水、冰山、地雷……你能说出来。不过，遇到海怪的风险是可控的。

如今，我们拥有自己的海怪，它们使许多聪明的头脑无法解决有趣的问题。终止的不确定性过去几十年来一直如此。在过去的二十年里，情况变得更好了。所以：不要害怕！

首先要考虑的是您的逻辑程序打算描述的实际关系。你甚至不需要一个具体的程序来回答这个问题。想象一下这种关系。首先，问有多少解决方案。如果数量有限，那么这部分就完成了，因为没有内在的原因您的程序无法终止。（在你的例子中，一般关系包含无限多的解决方案：只要看到第三个参数中的列表有无限多的长度就足够了。）

如果有无限多，请尝试查找查询的有限子集。（在您的示例中，如果第三个参数是接地的，则只有有限多个解决方案。同上，如果第一个参数和第二个参数是接地的。但是，请注意，如果只有第一个参数是接地的，情况并非如此！）

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

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

如果您现在查看您的程序，您可能会发现与预期关系有些不同。在您的示例中，查询 concat([],[],[]) 失败，但它应该成功。而且concat([],nonlist,L) 也成功了。前者肯定是错别字，后者是一种概括，通常被认为是可以接受的。

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

您现在可以参考具体程序来确定程序的终止属性。考虑cTI，它确实推断程序的终止和非终止属性。通过这种方式，可以确定推断的属性是否是最优的。

另一种方法是使用failure-slices 来确定程序的非终止片段。有关更多信息，请参阅this one 之类的答案。

【讨论】：

【解决方案2】：

我通常使用这些规则：

必须使用不同的参数方向/类型测试每个新谓词。在你的情况下，方向是 (+, +, -), (+, -, +), (-, +, +), (-, -, +), (-, +, -), (+, - , -), (-, -, -)。 “-”表示未绑定的变量，+ - 已绑定一些成员的变量。如果在同一位置带有“-”的情况有效，则“+”的情况将始终有效。因此，实际上您只能执行 4 次测试。我认为任何谓词都不会在 (-, -, ...) 模式下工作。只需从解释器命令行进行测试，您还不需要编写单元测试。
如果您发现某些结果不合适，请重新设计您的谓词。例如
```
con_fin([],X,X).
con_fin(A,X,[Head|R]) :- nonvar(A), A=[Head|Tail], con_fin(Tail,X,R).
```
将始终返回一组有限的答案。如果你还不能一次写出完美的两行谓词（完美的谓词是有效地适用于所有可能方向的谓词）为不同的模式/类型写几行，让类型检查像 var、nonvar、@987654323 @、is_set/1 等成为你的朋友。
在测试之后做出明确的评论。您应该始终提及参数的可能类型和方向，并将谓词定义为某些模式的 det、semidet 或 nondet。 我认为您的问题不是“(-, +, -) nondet”情况的无限解决方案，而是不会警告用户可能存在无限递归。
```
B=[1, 2], con(A, B, C), A=[0].
```
只需与以下案例进行比较
```
B=[1,2], con(A, B, C), proper_length(C, 4), !.
```
无效但正确且具有确定性。
添加模式和类型检查。使用不当抛出异常。 ISO 标准为某些情况预定义了例外情况 (http://www.deransart.fr/prolog/exceptions.html)，良好的设计应遵循其建议。
编写一个涵盖所有可能使用情况的单元测试（通常不会超过 15 分钟，但将来会节省更多）。
享受你的生活
如果您找到了更好的解决方案（Eureka！），只需重写谓词，现在单元测试就是您最好的朋友。

通常，Prolog 允许编写非常紧凑和智能的代码，但与其他语言相比需要更多的工作。可以像俳句一样在几年内改进一条小线。但是该语言的实际本质是try->test->use->redesign原则，因为在Prolog中很容易做实验。

【讨论】：

【解决方案3】：

你的程序 concat 并不完全正确，它应该是：

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

注意第二行[Head|R] 中的|。您无法分析它是否会像@DanielLyons 所说的那样停止。您可以做的是使用“！”修剪解决方案树。

【讨论】：

当我只想要一个解决方案时，我特别喜欢使用once/1 作为修剪解决方案树的一种很好的声明方式。当然它没有剪裁那么灵活。