Prolog 在目标重新​​排序后不会终止

Question

我目前正在研究 Learn Prolog Now 示例，对于一个 exercise，如果我对一条规则进行了微小的更改，我的 KB 就会用完本地堆栈。这是知识库：

byCar(auckland,hamilton). 
byCar(hamilton,raglan). 
byCar(valmont,saarbruecken). 
byCar(valmont,metz). 

byTrain(metz,frankfurt). 
byTrain(saarbruecken,frankfurt). 
byTrain(metz,paris). 
byTrain(saarbruecken,paris). 

byPlane(frankfurt,bangkok). 
byPlane(frankfurt,singapore). 
byPlane(paris,losAngeles). 
byPlane(bangkok,auckland). 
byPlane(singapore,auckland). 
byPlane(losAngeles,auckland).

travel(X,Y) :- byCar(X,Y).
travel(X,Y) :- byTrain(X,Y).
travel(X,Y) :- byPlane(X,Y).

及相关规则：

travel(X,Y) :- travel(X,Z), travel(Z,Y).

这是有问题的查询，它用完了堆栈：

?- travel(valmont,losAngeles).

但是如果我将规则更改为

travel(X,Y) :- travel(Z,Y), travel(X,Z).

然后就可以了。

如果我跟踪查询，我很快就会像这样卡住：

   Redo: (17) travel(raglan, _6896) ? creep
   Call: (18) byPlane(raglan, _6896) ? creep
   Fail: (18) byPlane(raglan, _6896) ? creep
   Redo: (17) travel(raglan, _6896) ? creep
   Call: (18) travel(raglan, _6896) ? creep
   Call: (19) byCar(raglan, _6896) ? creep
   Fail: (19) byCar(raglan, _6896) ? creep
   Redo: (18) travel(raglan, _6896) ? creep
   Call: (19) byTrain(raglan, _6896) ? creep
   Fail: (19) byTrain(raglan, _6896) ? creep
   Redo: (18) travel(raglan, _6896) ? creep
   Call: (19) byPlane(raglan, _6896) ? creep
   Fail: (19) byPlane(raglan, _6896) ? creep
   Redo: (18) travel(raglan, _6896) ? creep
...

但我不明白为什么。它不应该只是理解 raglan 是一个终端站，因此它必须再回溯一层吗？

谢谢！

编辑：我使用 SWI Prolog

编辑：我在一步步解决后发现了问题。 在插肩的情况下，任何地方都没有规则。因此，在尝试byPlane, byTrain, byCar 之后，它再次尝试travel(raglan, X)（最后一条规则的第一个目标），从而循环。 但我看不出另一条规则有什么更好的地方。

Answer 1

您需要澄清“它有效”的含义。事实上，谓词travel/2 的两个版本都不会终止。但碰巧找到了针对高度具体查询的解决方案。

现在询问?- travel(hamilton, losAngeles). 两者的循环。

因此，您的修复仅适用于某些查询，但不适用于其他查询。难道没有更可靠的出路吗？

一般来说，Prolog 产生的非常精确的答案替换序列很难预测。您将不得不模拟 Prolog 采取的每一个微小步骤。

另一方面，有一个非常相关的概念，称为（通用）终止，它更容易预测，因为它独立于程序中的许多细节，例如事实出现的顺序.查询通用终止的最简单方法是在查询末尾添加目标 false。

但您还可以进一步添加目标false，随心所欲¹。这种修改后的程序称为failure-slice。无论您如何插入 false，以下内容均成立：

如果故障片没有终止，那么你的原始程序也不会终止。

现在考虑travel/2 的两个变体的故障切片：

travel(X,Y) :- false, byCar(X,Y)。 travel(X,Y) :- false, byTrain(X,Y)。 travel(X,Y) :- false, byPlane(X,Y)。 旅行（X，Y）：-旅行（X，Z），false，旅行（Z，Y）。

还有你的其他版本：

travel(X,Y) :- false, byCar(X,Y)。 travel(X,Y) :- false, byTrain(X,Y)。 travel(X,Y) :- false, byPlane(X,Y)。 旅行（X，Y）：-旅行（Z，Y），false，旅行（X，Z）。

在两者中，X 和 Y 都不被考虑！所以这两个参数不影响终止。因此两个版本都不会终止。也就是说，它们从不终止。

现在将此结论与查看轨迹的更传统方法进行比较。虽然故障切片允许我们做出一般性结论（“...永不终止”），但特定跟踪只能向您显示特定执行的详细信息。

为了解决这个问题，您需要更改可见部分的某些内容。我的建议是使用closure/3。那就是：

travel(X, Y) :-
   closure(connexion, X, Y).

connexion(X,Y) :- byCar(X,Y).
connexion(X,Y) :- byTrain(X,Y).
connexion(X,Y) :- byPlane(X,Y).

或者使用更通用的path/4。

---

_{1 实际上，这只适用于纯单调程序。你的程序就是其中之一}

Answer 2

显然，在这种情况下，目标排序非常重要。正如您所知道的，您的第一个公式允许通过假设的另一个城市 Z 找到从插肩到任何地方的另一个假设连接，它的不存在永远不会被证明，因为您一直在寻找它无限递归。真的，trace 是你最好的朋友，但要做到这一点并非易事。您还必须考虑绑定一个、两个或一个参数的所有情况。

您的第二个公式一点也不好，只是碰巧在不同的情况下失败了：

travel(losAngeles, valmont).
ERROR: Out of local stack

我建议通过区分直接连接和多站旅程来使您的逻辑更安全：

connection(X,Y) :- byCar(X,Y).
connection(X,Y) :- byTrain(X,Y).
connection(X,Y) :- byPlane(X,Y).

travel(X,Y) :- connection(X,Y).
travel(X,Y) :- connection(X,Z), travel(Z,Y).

目标顺序现在无关紧要，因为travel 总是需要存在一些物理连接（而不是递归）才能继续。

这也使得记录旅程变得更容易，这是您无论如何都想要的（对吧？）：

connection(X,Y, car(X,Y))   :- byCar(X,Y).
connection(X,Y, train(X,Y)) :- byTrain(X,Y).
connection(X,Y, plane(X,Y)) :- byPlane(X,Y).

travel(X,Y,[Part])       :- connection(X,Y,Part).
travel(X,Y,[Part|Parts]) :- connection(X,Z,Part), travel(Z,Y,Parts).

?- travel(valmont, losAngeles, Journey).
Journey = [car(valmont, saarbruecken), train(saarbruecken, paris), plane(paris, losAngeles)] 

对于没有有效行程的情况：

travel(losAngeles, valmont, Journey).
false.