Есть ли в TLA+ инфиксный оператор xor (исключительный или)?

Question

Есть ли в TLA+ оператор xor, определенный как часть самого языка, или я должен определить свой собственный?

Answer 1

При условии, что A \in BOOLEAN /\ B \in BOOLEANто, что известно в логике высказываний как "XOR", является неравенством:

A # B

что при том же предположении эквивалентно ~ (A <=> B), когда A, B принимать не булевы значения, эти две формулы не обязательно эквивалентны. Оператор <=> означает следующее

/\ A \in BOOLEAN
/\ B \in BOOLEAN
/\ A = B

Так

(~ (A <=> B)) <=> \/ ~ A \in BOOLEAN
                  \/ ~ B \in BOOLEAN
                  \/ ~ (A = B)

Таким образом, если первые два дизъюнкта являются ложными, то <=> а также = эквивалентны. В противном случае может случиться так, что

/\ A \notin BOOLEAN
/\ A = B

который мог бы удовлетворить A <=> B, Смотрите также п.10 и гл. 16.1.3 книги TLA+. Формула

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

имеет значение также для небулевых значений идентификаторов A а также Bпотому что TLA+ нетипизирован. Так

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

это возможное значение. Насколько я знаю, язык не определяет, имеет ли эта формула такое же значение, как

15 # "a"