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

Question

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

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 第 2 版：初步指南中所述。

另请参见第 10 页（它为参数的布尔值定义了布尔运算符）和 Sec。TLA+ 书的 16.1.3 。公式

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

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

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

是一个可能的值。我不知道 TLA+ 是否指定这个公式是否具有相同的值

15 # "a"

另请参阅实用 TLA+ 的第 201 页第 10 行附录 A的评论。