析取 G1 ; G2 vs. If-then-else Cond -> G1 ; G2

Question

我遇到了一个包含嵌套 if-then-else 形式的 Prolog 程序

p(X,Y) :-
     (cond1(X,Y) -> q(X)); true,
     (cond2(X,Y) -> q(Y)); true.

有意想不到的答案。此行为的原因与以下查询中的相同：

?- (true, (true -> X=a)); X=b.
X = a ;
X = b.

?- ((true -> X=a), true); X=b.
X = a ;
X = b.

?- (true -> X=a); X=b.
X = a.

第一个查询有两个答案，但第二个只有一个。不同行为的原因是什么？

P.S.：我知道其中的区别，但我还没有找到一个 SO question 来处理这个非常令人困惑的现象。那么为什么不以这种方式记录呢？

Answer 1

关于析取的可追溯性。 这两个查询在结构上是不同的：

trace, (true -> X=a); X=b.

trace, ((true -> X=a); X=b).

您可以使用 write_canonical/1 来查看区别：

?- write_canonical((trace, (true -> X=a); X=b)), nl.
;(','(trace,->(true,=(A,a))),=(A,b))
true.

?- write_canonical((trace, ((true -> X=a); X=b))), nl.
','(trace,;(->(true,=(A,a)),=(A,b)))
true.

而且它们的行为也不同：

?- trace, (true -> X=a); X=b.
   Call: (9) true ? creep
   Exit: (9) true ? creep
   Call: (9) _428=a ? creep
   Exit: (9) a=a ? creep
X = a 
   Call: (9) _428=b ? creep
   Exit: (9) b=b ? creep
X = b.

[trace]  ?- trace, ((true -> X=a); X=b).
   Call: (9) true ? creep
   Exit: (9) true ? creep
   Call: (9) _706=a ? creep
   Exit: (9) a=a ? creep
X = a.

只有第二个查询会测试 (true -> X=a); X=b。

Answer 2

首先让我们解决初始谓词：格式建议嵌套 if-then-else，但第二个主体周围的括号将第一个 true 分组到 else 分支：

?- listing(p).
p(A, B) :-
    (   cond1(A, B)
    ->  q(A)
    ;   true,
        (   cond2(A, B)
        ->  q(B)
        )
    ;   true
    ).

这就是我们最终得到以true, ... 开头的查询的方式。这里的第二个问题是; 的使用被重载：仅当G1 不是(Cond -> Goal) 形式时，G1; G2 形式的术语才被解释为析取项。否则，它被解释为 if-then-else。让我们看看不同的情况：

• (true, true -> X=a); X=b 将 ; 解释为析取，因为左侧的最外层函子是合取 ,。 Prolog 报告每个分支的答案替换。
• (true -> X=a, true); X=b: 同理是析取
• (true -> X=a); X=b: 是一个 if-then-else，因为左侧最外面的函子是 if-then 运算符 ->。 Prolog 只报告true 分支的答案替换。

有趣的是，当我们将条件放入变量时，这似乎不再起作用（在 SWI 8 上）：

?- G1 = (true -> (X = a)), (G1 ; X=b).
G1 =  (true->a=a),
X = a ;
G1 =  (true->b=a),
X = b.

当我将G1 包装成call/1 时，也会发生同样的情况：

?- G1 = (true -> (X = a)), (call(G1) ; X=b).
G1 =  (true->a=a),
X = a ;
G1 =  (true->b=a),
X = b.

如果我正确阅读了前面问题的answer，那么第一个问题应该不同。

我会假设不同的跟踪行为是断点干扰了 if-then-else 的检测。我在跟踪过程中的错误是点击enter 爬行但没有意识到我上报实际答案时需要输入;。