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 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 {}.

Assuming Sum(S) returns the sum of the elements of S, write an operator that, for a given set of integers S and integer N, returns if there are N elements in S that sum to 0. eg

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 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.

\A x \in {}: FALSE is still true!

Given a set and an operator, determine whether the operator is commutative over all elements in the set.

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

Alternatively, we could put them on the same line:

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.

Without looking back at the introduction, write an operator that returns the maximum number of a set.

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.


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)

A prime number p is a twin prime if p-2 is prime or p+2 is prime. Find the largest twin prime in S.

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)

Now return the largest pair of twin primes, ordered by value. Assume that S may be missing numbers and, if one of the twin primes is missing, the pair is invalid. For example, the largest pair in {3, 5, 13} is <<3, 5>>, not <<5, 13>>.

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

Given stockprices is a tuple of positive integers representing the value of a stock at a given time of day, write an operator that determines the maximum profit you could make by buying and selling a single stock. Assume for this problem that you cannot short; you must buy before you sell.

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]

Note this will crash if there is no possible pair, which is preferrable to paying trading fees twice on a zero-dollar profit.