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

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

\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, HasEvenNumber 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

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)

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.

LargestTwinPrime(S) == CHOOSE x \in S:
                    /\ IsPrime(x)
                    /\  \/ IsPrime(x + 2)
                        \/ IsPrime(x - 2)
                    /\ \A y \in S:
                        IsPrime(y) => y <= x
                    * or y > x => ~IsPrime(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.