TLA+ 中是否有异或（异或）中缀运算符？

Question

TLA+ 是否将异或运算符定义为语言本身的一部分，还是我必须自己定义？

Answer 1

在A \in BOOLEAN /\ B \in BOOLEAN的假设下，命题逻辑中称为"XOR"的不等式：

A # B

在同样的假设下相当于~ (A <=> B)。当A, B取非布尔值时，这两个公式不一定等价。以下公理可以描述运算符 <=>

THEOREM
    ASSUME
        /\ A \in BOOLEAN
        /\ B \in BOOLEAN
    PROVE
        (A <=> B)  =  (A = B)

对于A和B的非布尔值，不指定A <=> B的值。在布尔运算符的适度解释中，未指定 A <=> B 是否对非布尔值 A 或 B 采用非布尔值。在布尔运算符的自由解释中，\A A, B: (A <=> B) \in BOOLEAN，如 TLA Version 2: A Preliminary Guide.

中所述

另见第 10 页（定义了参数布尔值的布尔运算符）和第 10 节。 TLA+ book 的 16.1.3。公式

(A \/ B) /\ ~ (A /\ B)

对于标识符 A 和 B 的非布尔值也有意义（TLA+ 是无类型的）。所以

(15 \/ "a") /\ ~ (15 /\ "a")

是一个可能的值。不知道TLA+是否指定了这个公式是否和

有相同的值

15 # "a"

另请参阅 Appendix A, Page 201, line 10 of Practical TLA+ 上的评论。

TLA+ 中是否有异或（异或）中缀运算符？

Is there an xor (exclusive or) infix operator in TLA+?

tla+