序言中的等价关系

Question

我想在Prolog代码中实现一个简单的当且仅当关系。下面是我想要的一个简单的例子：

?- a_iff_b(a, b).
true.
?- a_iff_b(x, x).
true.
?- a_iff_b(a, x).
false.
?- a_iff_b(x, b).
false.

你明白了——如果第一个参数是a，第二个参数是b，或者第一个参数既不是a，也不是第二个b，那么谓词应该为true。我希望这是有道理的。从数学上讲，X = a <==> Y = b。

这是我的尝试：

a_iff_b(X, Y) :-
X = a, Y = b;
X = a, Y = b.

但这段代码引入了一个选择点：

?- a_iff_b(a, b).
true ;
false.

为什么？似乎以下作品，我的意思是它没有介绍选择点：

a_iff_b(X, Y) :- (X = a -> Y = b; Y = b).

然而，我发现这有点不太可读，特别是因为在我的实际谓词中，等价的两边更复杂(也是谓词(。

Answer 1

您的代码引入了一个选择点，因为它包含;运算符引入的一个选择。你可能会认为这是一个"；逻辑或"逻辑"；运算符，在某种程度上是非正式的；在这里引入一个选择点，在回溯时，也探索第二个分支"操作人员

的确，一个功能强大的Prolog编译器™可能能够认识到这里的两个分支是互斥的，但您的Prolog系统似乎没有那么强大。如果你能免费获得的Prolog能够在没有选择点的情况下做到这一点，我至少会有点惊讶。尤其是如果你的实际情况更复杂，正如你所说。

如果你想让它更可读，一些提示：

• 通常，从不在一行的末尾使用;，就好像它只是,的变体一样。人们很容易错过它，因为一般的期望是行以,结尾。尝试以某种方式格式化代码，使;真正突出(请参阅下面的示例(。

• 通常，如果您想使用;(而不是_ -> _ ; _(，特别是作为子句中的单个顶级目标，请考虑使用单独的子句：

  a_iff_b(a, b).
  a_iff_b(X, Y) :-
  X = a,
  Y = b.
  

在任何情况下，以下都是减少选择的可能方法：

a_iff_b_1(a, b) :-
!.
a_iff_b_1(X, Y) :-
X = a,
Y = b.
a_iff_b_2(X, Y) :-
(   X = a, Y = b
->  true
;   X = a, Y = b ).
a_iff_b_3(X, Y) :-
(   X = a, Y = b,
!
;   X = a, Y = b ).
a_iff_b_4(X, Y) :-
(   X = a, Y = b
;   X = a, Y = b ),
!.
a_iff_b_5(X, Y) :-
once(( X = a, Y = b
; X = a, Y = b )).