Logic

In this section, we’ll introduce the basics of propositional logic. Even if you’re unfamiliar with the idea, you’ve almost certainly used it in programming before.

\E

\E means “exists”. We write \E x \in S : P(x) to say “there is at least one x in the set such that P(x) is true.” It’s the equivalent of a python any() or a Ruby any?. If we wanted to check that a set had an even number in it, we could write HasEvenNumber(S) == \E x \in S : IsEven(x)

~\E is the opposite: it says that there are no such elements. \E x \in {}: Foo is always false, since there are no elements in {}.

SumsToZero({1, 2, -7, 4, 11}, 2) = FALSE
SumsToZero({1, 2, -7, 4, 11}, 4) = TRUE
SumsToZero({1, 2, -7, 4, 11}, 5) = FALSE

SumsToZero(S, N) == \E s \in SUBSET S:
                      /\ Cardinality(s) = N
                      /\ Sum(s) = 0

\A

\A means “all”. We write \A x \in S : P(x) to say “For every x in the set, P(x) is true.” If we wanted to check that a set had no odd numbers in it, we could write OnlyEvenNumbers(S) == \A x \in S : IsEven(x). If there are only even numbers, OnlyEvenNumbers is true. Otherwise it’s false. Simple.

~\A is the opposite: it says that there is at least one element where P(x) is false. \A x \in {}: Foo is always true, since there are no elements in {}, so all zero elements pass the test.

IsCommutative(Op(_,_), S) == \A x \in S :
                          \A y \in S : Op(x,y) = Op(y,x)

IsCommutative(Op(_,_), S) == \A x \in S, y \in S : Op(x,y) = Op(y,x)

=> and <=>

P => Q means “If P is true, then Q must also be true.” Note that P can be false and Q can be true, or both can be false. It’s equivalent to writing ~P \/ Q, which is how TLC interprets it.

P <=> Q means “Either both P and Q are true or both are false.” It’s equivalent to writing (~P /\ ~Q) \/ (P /\ Q). P <=> ~Q is P XOR Q.

Max(S) == CHOOSE x \in S : \A y \in S : y <= x

Both => and <=> follow the same precedence rules as logical junctions. In other words, TLC interprets

/\ A
/\ B
  => C

as A /\ (B => C), whereas without the indent it’s interpreted as (A /\ B) => C.

CHOOSE

While we introduced the CHOOSE operator back in sets, it really comes into its own when we add the logical operators. Many quantified properties, such as “the largest x such that P”, can be expressed as “the x where all larger elements don’t have P” or “the x where all of the other elements with P are smaller”. For example, what is the largest prime in a set S?

IsPrime(x) == x > 1 /\ ~\E d \in 2..(x-1) : x % d = 0

LargestPrime(S) == CHOOSE x \in S:
                    /\ IsPrime(x)
                    /\ \A y \in S:
                        IsPrime(y) => y <= x
                    \* or y > x => ~IsPrime(y)

IsTwinPrime(x) == /\ IsPrime(x)
                  /\ \/ IsPrime(x + 2)
                     \/ IsPrime(x - 2)


LargestTwinPrime(S) == CHOOSE x \in S:
                    /\ IsTwinPrime(x)
                    /\ \A y \in S: IsTwinPrime(y) => y <= x
                    * or y > x => ~ IsTwinPrime(y)

LargestTwinPair(S) == CHOOSE <<x, y>> \in S \X S:
                         /\ IsPrime(x)
                         /\ IsPrime(y)
                         /\ x = y - 2
                         /\ \A <<w, z>> \in S \X S:
                            /\ IsPrime(z)
                            /\ IsPrime(w)
                            /\ w = z - 2
                            => z < y

MaxProfit(stockprices) ==
    LET sp == stockprices \* clean it up a bit
        TimePair == (1..Len(sp)) \X (1..Len(sp))
        Profit[p \in TimePair] == sp[p[2]] - sp[p[1]]
        best == CHOOSE best \in TimePair :
            /\ best[2] > best[1] \* Buy after sell
            /\ Profit[best] > 0 \* Make money plz
            /\ \A worse \in TimePair :
                worse[2] > worse[1] => Profit[best] >= Profit[worse]
    IN Profit[best]