Note: for each reading, you will need to complete a few exercises These daily drills are exercises marked with a double dagger, ‡. There are two in this reading, concrete equivalences and quantified propositions. You can submit your answers via plaintext to Gradescope.

Don’t worry if you feel like you didn’t get the right answer for the daily drills! It is more important that you put in the effort, e.g., 10 minutes trying out each of the problems, and that you come to class with any questions about the content and the drills.

Propositions and Proofs

Our formal model of computation allows us to reason about the behavior of programs. But to what ends can we apply this reasoning? Besides merely checking our work, we can also use our formal model to prove propositions about our programs.

Another word for a proposition is a claim. Here are some example propositions over programs that we could consider:

• (string-length "hello world!") is equivalent to 12.
• There exists a list l for which (length l) is 0.
• (insertion-sort l) performs more comparison operations than (mergesort l) for any list l.
• For any number n, (* 2 n) is greater than n.

The first proposition is a fully concrete proposition of the sort we have previously considered. The second is an abstract proposition because it involves a variable, here l.

Ultimately, the first two propositions involve equivalences between expressions. But propositions do not need to be restricted to equivalences. The third proposition talks about the number of operations that one expression performs relative to another.

Furthermore, propositions don’t even need to be provable! For example, the final proposition is not provable. A counterexample to this proposition arises when we consider n = -1. (* 2 -1) evaluates to -2, and -2 is not greater than -1!

Equivalences Between Expressions

Of the many sorts of propositions possible, we will work exclusively with equivalences in our discussion of program correctness.

Recall that \(e \longrightarrow e'\) (“steps to”, LaTeX: \longrightarrow) means that the (Racket) expression \(e\) takes a single step of evaluation to \(e'\) in our mental model of computation. The notation \(e \longrightarrow^* e'\) (“evaluates to”, LaTeX: \longrightarrow^*) means that \(e\) takes zero or more steps to arrive at \(e'\). With this in mind, the formal definition of equivalence amounts to saying the following:

Two expressions are equivalent if they evaluate to identical values.

Thus, we can prove a claim of program equivalence by using our mental model to give a step-by-step derivation (an execution trace) of an expression to a final value. If both sides of the equivalence evaluate to the same value, then we know they are equivalent by our definition! The execution trace itself is a proof that the equivalence holds.

For example, consider the following recursive definition of factorial:

(define factorial
  (lambda (n)
    (if (zero? n)
        1
        (* n (factorial (- n 1))))))

and subsequent claim about its behavior:

We can prove this claim by evaluating the left-hand side of the equivalence and observing that it is identical to the right-hand side:

    (factorial 3)
--> (if (zero? 3) 1 (* 3 (factorial (- 3 1))))
--> (if #f 1 (* 3 (factorial (- 3 1))))
--> (* 3 (factorial (- 3 1)))
--> (* 3 (factorial 2))
--> (* 3 (if (zero? 2) 1 (* 2 (factorial (- 2 1)))))
--> (* 3 (if #f 1 (* 2 (factorial (- 2 1)))))
--> (* 3 (* 2 (factorial (- 2 1)))
--> (* 3 (* 2 (factorial 1)))
--> (* 3 (* 2 (if (zero? 1) 1 (* 1 (factorial (- 1 1))))))
--> (* 3 (* 2 (if #f 1 (* 1 (factorial (- 1 1))))))
--> (* 3 (* 2 (* 1 (factorial (- 1 1)))))
--> (* 3 (* 2 (* 1 (factorial 0))))
--> (* 3 (* 2 (* 1 (if (zero? 0) 1 (* 0 (factorial (- 0 1)))))))
--> (* 3 (* 2 (* 1 1)))
--> (* 3 (* 2 1))
--> (* 3 2)
--> 6

This precise step-by-step analysis of the behavior of the expression rigorously proves our claim!

Formatting Proofs

We will use this standard format for writing formal proofs for the remainder of the course. In summary, we write:

Symbolic Execution

Previously, we introduced a model of computation for the Racket programming language. This model allows us to prove program properties when concrete values are involved. However, we frequently wish to prove properties where the values are unknown. For example, we might consider a proposition about the standard list-append function:

For all lists l1 and l2, (+ (length l1) (length l2)) = (length (list-append l1 l2))

This proposition ranges over unknown, rather than concrete, lists. We, therefore, need to upgrade our mental model to work with these unknown quantities.

Abstract Propositions

Up to this point, we have considered concrete expressions, i.e., expressions that do not contain variables. What happens if we allow expressions to contain variables. As an example, consider the following implementation of boolean and:

; N.B. non-short-circuiting version of `and`
(define my-and
  (lambda (b1 b2)
    (if b1
        b2
        #f)))

Now, let’s consider the following equivalence claim:

Claim: (my-and #t b) ≡ #f

Here, b is a variable, presumed to be of boolean type. However, how do we interpret b? It turns out there are two interpretations we might consider:

• Does there exist a boolean value to b so that the proposition is provable?
• Is the proposition provable for all possible boolean values that b can take on?

The former interpretation is called an existential quantification of b. We alternatively say that b is existentially quantified or is an “existential.” Quantification refers to the fact that our interpretation tells us “how many” values of b to consider in the proposition. In existential quantification, we consider a single value.

In contrast, the latter interpretation is called a universal quantification of b. In universal quantification, we mean that the proposition holds for all possible values of b. Note that the above proposition is provable if b is interpreted existentially: if we let b be #f then:

    (my-and #t b)
--> (my-and #t #f)
--> (if #t #f #f)
--> #f

However, the proposition does not hold when b is universally quantified. More specifically, while it holds when b is #f, it does not hold when b is #t.

    (my-and #t b)
--> (my-and #t #t)
--> (if #t #t #f)
--> #t

Because of this, we must be explicit when introducing variables into our proposition. For each such variable, we must declare whether it is existentially quantified and universally quantified. To do so, we can use the words:

• For all for universal quantification, e.g., “for all lists l ” and
• There exists for existential quantification, e.g., “there exists a number n …”.

Furthermore, we reason about the variable differently depending on its quantification, as we see in the following sections.

Existential Propositions

If a variable \(x\) appears as an existential in a proposition, we interpret that variable as: there exists a value for \(x\) such that the proposition holds. In other words, the proposition is provable if we can give a single value to substitute for \(x\) so that the resulting proposition is provable. Thus, to prove an existential claim, we can choose such a value, substitute for the existential variable, and then use concrete evaluation as before.

As an example, let’s formally prove the existential version of the my-and claim that we introduced above:

    (my-and #t #f)
--> (if #t #f #f)
--> #f

Note how our proof has changed now that our proposition is abstract:

1. In our claim, we explicitly quantify the variable b by declaring it existential by using “there exists” to describe it.
2. In our proof, we explicitly choose a value for the existentially quantified variable (“Let b be #f”).

We can also existentially quantify over multiple variables. In these situations, we provide instantiations for each variable but otherwise proceed as normal.

    (list-append '() '(1 2 3))
--> (if (null? '())
        '(1 2 3)
        (cons (car '()) (list-append (cdr '()) '(1 2 3))))
--> (if #t
        '(1 2 3)
        (cons (car '()) (list-append (cdr '()) '(1 2 3))))
--> '(1 2 3)

Universal Quantification

When a variable is universally quantified, it stands for any possible value. Let’s take a look at a simple squaring function:

(define square
  (lambda (n)
    (* n n)))

And a simple universal claim about this function:

Because the claim holds for all possible values of n, we can’t choose an n like with existentials. Instead, we must hold n abstract, i.e., consider it to be an arbitrary number, and then proceed with the proof. In effect, because n is universally quantified, we treat n like a constant, yet unknown, quantity in our reasoning.

When we use our mental model of computation, we immediately arrive at a problem: both (square n) and (* n n) cannot take any evaluation steps! (square n) cannot step because n needs to be a value before we perform the function application, and we said that values were numbers, boolean constants, or lambdas. (* n n) cannot step because since we don’t know what n is, we don’t know what concrete value the multiplication will produce. We say that both expressions are stuck: they are not values, but they cannot take any additional evaluation steps.

We can’t reconcile the (* n n) case. Without knowing what n is, we cannot carry out the multiplication. However, if we treat the constant-yet-unknown n as a value, then we can proceed with the function application:

    (square n)
--> (* n n)

Even though the left- and right-hand sides of the equivalence are not values, they are identical. This fact is sufficient to conclude that the two original expressions are equivalent according to our definition of program equivalences! Let’s put these ideas together into a complete proof of the proposition:

In summary, when we encounter a universally quantified variable in a proposition, we:

1. Consider the variable to be a constant, yet unknown value. For convenience, we keep the name of this constant to be the same as the (universally quantified) variable, but we understand that the two are different objects!
2. When reasoning about the constant, we assume that it is a value for the purposes of our mental model of computation.

Case Analysis

Sometimes when we work with universally quantified variables, we can get away without thinking about their actual values. However, more often or not, our reasoning must consider their possible values. This reasoning will ultimately depend on the types of values involved, and this is where our proofs get more intricate in their design!

As an introduction to these concepts, let’s consider the case where we know the type in question only allows for a finite set of values. At present, only the boolean type has this property. Booleans only allow for two values, #t and #f, whereas there are an infinite number of numbers and functions to choose from!

To see how we can take advantage of the finiteness of the boolean type in our proofs, let’s consider the following simple claim, again using the my-and function:

If we let b be arbitrary, we can begin evaluating the left-hand expression.

    (my-and b #f)
--> (if b #f #f)

We can see pretty readily that no matter how the conditional evaluates, we will return #f. Be careful, though; this intuition is not sufficient for formal proof! We must instead rely on our evaluation model directly to ultimately show that this intuition is correct. However, if b is unknown, we don’t know which branch the conditional will produce.

Thankfully, we assumed that b was a boolean, so it must either be #t or #f. Therefore, we can proceed by case analysis: we will consider two separate cases, b is #t and b is #f, and show that the claim holds in both cases. If the claim holds for both cases, we know that the claim holds for every possible value of b and, thus, have completed the proof.

    (my-and b #f)
--> (if b #f #f)

Because `b` is a boolean, either `b` is `#t` or `b` is `#f`.

+   **`b` is `#t`**. Then `(if #t #f #f) --> #f`.
+   **`b` is `#f`**. Then `(if #f #f #f) --> #f`.

In both cases, the left-hand side steps to `#f`, precisely the right-hand side of the equivalence.

(define my-or
  (lambda (b1 b2)
    (if b1
        #t
        b2)))