Search code examples
tla+

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

Does TLA+ have an xor operator defined as part of the language itself, or do I have to define my own?

Solution

  • Under the assumption that A \in BOOLEAN /\ B \in BOOLEAN, what is known in propositional logic as "XOR" is inequality:

    A # B

    which under the same assumption is equivalent to ~ (A <=> B). When A, B take non-Boolean values, these two formulas are not necessarily equivalent. The following axiom could describe the operator <=>

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

    For non-Boolean values of A and B, the value of A <=> B is not specified. In the moderate interpretation of Boolean operators it is unspecified whether A <=> B takes non-Boolean values for non-Boolean A or B. In the liberal interpretation of Boolean operators, \A A, B: (A <=> B) \in BOOLEAN, as described in the TLA Version 2: A Preliminary Guide.

    See also page 10 (which defines the Boolean operators for Boolean values of the arguments) and Sec. 16.1.3 of the TLA+ book. The formula

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

    is meaningful also for non-Boolean values of the identifiers A and B (TLA+ is untyped). So

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

    is a possible value. I do not know if TLA+ specifies whether this formula has the same value as

    15 # "a"

    See also the comment on Appendix A, Page 201, line 10 of Practical TLA+.