prolog - 析取运算符的等价性和具有若干规则的定义

Question

我只是偶然发现了 ;/2 的定义在 SWI Prolog Manual其中指出:

The `or' predicate is defined as:

Goal1 ; _Goal2 :- Goal1.
_Goal1 ; Goal2 :- Goal2.

那是不是意味着 ;/2行为就像我们编写自己的由两个规则组成的辅助谓词一样？我已经记住了 ;/2是一个不纯的构造(但我有可能将它与 if-then-else 混为一谈)但这个定义是纯的(尽管元逻辑)。
;/2的语义在 ISO 标准的第 7.8.6 段中定义，但这是根据当前状态、选择点等的操纵来完成的。

SWI 手册中的定义是否等同于 ISO 定义？如果不是，你知道它们不同的例子吗？

Answer 1

Wouldn't that mean that ;/2 behaves exactly as if we wrote our own helper predicate consisting of two rules?

不。术语到正文的转换很重要。

但首先，它的 (;)/2这在 7.8.6(析取)和 7.8.8(if-then-else)中都有定义——正如 7.8.6 中的第一句话所暗示的那样。对于 ; 周围的圆括号参见 7.1.6.6 中的注释。

因此，第一个问题是，如果您看到 ( G_0 ; H_0 )，如何确定适用哪个子条款。在你的程序中。这与调用 (;)/2 时存在的实例化无关。而是取决于术语到正文转换期间的实例化(7.6.2)。

?- G_0 = ( true -> X = si ), ( G_0 ; X = nisi ).
   G_0 =  (true->si=si),
   X = si
;  G_0 =  (true->nisi=si),
   X = nisi.

?- G_0 = ( true -> X = si ), call( ( G_0 ; X = nisi ) ).
   G_0 =  (true->si=si),
   X = si.

在第一个查询中，词到正文的转换替换了析取 G_0来自 call(G_0)因此

( call( ( true -> X = si ) ) ; X = nisi ) )

将被执行。

在第二个查询中，有两次术语到正文的转换，一次用于整个查询，一次用于显式 call/1 ，但两者都保持原样，因此

call( ( true -> X = si ; X = nisi ) )

将被执行，else 情况被排除在外。

由于术语到正文转换的进一步差异是由于畸形正文导致的切割和错误。