这个Prolog程序有一个简单的停止证明吗？

Question

:-  p(f(X),f(f(Y)),f(f(b))).

p(f(a),f(X),f(f(X))).
p(f(a),f(a),f(f(X))).
p(X,f(f(Y)),X) :- p(Y,f(f(Y)),f(f(X))).
p(f(X),Y,Z) :- p(X,f(Y),f(f(Z))).

我相信我有一个使用归纳法的证明，并且需要几个子案例，其中一些是：

p(f(X),f(f(X)),f(f(b))) grows (i.e. does not halt) is a corollary from:

p( X, f^n(X), f^(n+1)(b) ) grows (i.e. does not halt)

p(f^k(b),f^l(b),f^m(b)) fails if 0 <= k < m.

p(f^k(b),f^l(b),f^k(b)) fails if l-k mod 3 = 0

where f^n(X) means n iterations: f(f(...f(X)...)).

我会尝试完成证明，但我想知道是否有一个更简单的非停止证明。通过“停止”，我假设标准的 Prolog 过程语义：子句的顺序排序以及（尽管在本示例中不相关）子目标从左到右的执行。

Answer 1

在 Prolog 中，我们通常谈论普遍终止和存在终止。普遍终止更为相关。目标

G_0

普遍终止，当且仅当

G_0, false

有限失败。因此，让我们考虑一下程序的以下failure-slice：

：- p(f(X)，f(f(Y))，f(f(b)))，假。

p(f(a),f(X),f(f(X))) :- 假。
p(f(a),f(a),f(f(X))) :- 假。
p（X，f（f（Y）），X）：- 假，p（Y，f（f（Y）），f（f（X）））。
p(f(X),Y,Z) :- p(X,f(Y),f(f(Z))), false。

如果这个故障片没有终止，那么整个程序也不会终止。这是纯 Prolog 程序的理想特性之一。

显然，

Y

和

Z

对终止都没有任何影响。两者（在此故障切片中）都是终止中立的。所以剩下的就是导致程序终止的第一个参数，如果它是绑定的（有限的和基本的）。通过一次推理，第一个

f(X)

被剥离，并保留一个（无别名）变量。因此，这个程序（带有给定的查询）不会普遍终止。 □

现在是存在主义的终止。也就是说，虽然程序不会普遍终止，但它仍然可以找到解决方案。想像这样的查询

?- length(L,N).
   L = [], N = 0
;  L = [_A], N = 1
;  L = [_A,_B], N = 2
;  L = [_A,_B,_C], N = 3
;  ... .
?- length(L,N), false.
   loops.

它不会普遍终止，但仍然会产生有用的答案，从而存在地终止。

存在性终止通常有一个捷径：如果没有解并且程序不会普遍终止，那么它也不会存在性终止。那将是一个快速的射击！可惜，这里的情况并非如此。其中一种解决方案是

?- p(f(f(a)),f(f(b)),f(f(b))).
   true
;  false.

还有更多。所以这个程序是否能找到解决方案仍然是一个悬而未决的问题。

现在有一件事情让我觉得奇怪：第三个子句没有任何作用（除了不终止）。我通过添加一个额外的参数来获得迭代加深来观察到这一点：

% p([n],_,_,_).
p([a],f(a),f(X),f(f(X))).
p([b],f(a),f(a),f(f(X))).
p([c|L],X,f(f(Y)),X) :- p(L,Y,f(f(Y)),f(f(X))).
p([d|L],f(X),Y,Z) :- p(L,X,f(Y),f(f(Z))).

?- length(L,N), p(L, A1,A2,f(f(b))).
   L = "a", N = 1, A1 = f(a), A2 = f(b)
;  L = "b", N = 1, A1 = f(a), A2 = f(a)
;  L = "da", N = 2, A1 = f(f(a)), A2 = f(f(b))
;  L = "db", N = 2, A1 = f(f(a)), A2 = a
;  L = "dda", N = 3, A1 = f(f(f(a))), A2 = f(f(f(b)))
;  L = "ddda", N = 4, A1 = f(f(f(f(a)))), A2 = f(f(f(f(b))))
;  L = "dddda", N = 5, A1 = f(f(f(f(f(a))))), A2 = f(f(f(f(f(b)))))
;  L = "ddddda", N = 6, A1 = f(f(f(f(f(f(a)))))), A2 = f(f(f(f(f(f(b))))))
;  L = "dddddda", N = 7, A1 = f(f(f(f(f(f(f(a))))))), A2 = f(f(f(f(f(f(f(b)))))))
;  ... .

所以当第三条规则最初使用一次时，没有找到解决方案，程序也不会终止。因此证明这部分无解就等于证明目标

p(X,f(f(X)),f(f(f(f(b)))))

无解。

我还没有完成这一部分，但似乎可以将论证缩小到以下观察结果：第一个参数始终采用

f*a

形式，但第二个参数采用

f*b

形式，因此不可能存在解决方案。