析取运算符的等价性及多规则定义

Question

我刚刚在 SWI Prolog Manual 中偶然发现了 ;/2 的定义，其中指出：

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

据我所知，定义

p(X) :- G1 ; G2 .

等同于定义

p(X) :- G1 .
p(X) :- G2 .

是的，您将此 ; 与有些相关但完全不同的 _ -> _ ; _ 混合在一起。

Answer 2

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 情况被忽略。

术语到正文转换的进一步差异是由于正文格式不正确导致的删减和错误。

析取运算符的等价性及多规则定义

Equivalence of disjunction operator and definition with several rules

prolog

iso-prolog