Program Equivalence Proofs

Problem 1: Equivalence Propositions

Exploring a model for interesting corner cases and behavior is one thing. However, we are ultimately interested in using our model to formally prove properties of programs. We call such properties propositions, statements about the world that are (potentially) provable. A proof is a logical argument that the proposition is indeed true.

There are many kinds of propositions we might consider when we think about program correctness. The most fundamental of these is program equivalence, asserting that two programs produce the same value.

Let's try writing our first proof and writing it down in LaTeX. Here is a recursive function definition over lists:

(define list-length
  (lambda (l)
    (if (null? l)
        0
        (+ 1 (list-length (cdr l))))))

We will prove the following claim:

The equivalence symbol (≡) (LaTeX: \equiv) acts like equality in that it asserts that the left- and right-hand sides of the symbol are equivalent. We say that two programs are equivalent if they evaluate to the same final value.

1. Before we write anything, we must prove the claim first! To show that an equivalence between two expressions holds, it is sufficient to show that both sides evaluate to identical values. The right-hand side of the equivalence is already a value, 3, so we need to show that the left-side of the equivalence evaluates to this same value. Use our mental model of computation to give an evaluation trace of (list-length (list 21 7 4)).

2. Now, let's write the proof in your lab write-up. When writing proofs, we will always:

   • Restate the claim.
   • Give the proof.

   For example, here is a proof of a simple arithmetic equivalence in this style:

   Sample Proof

   Claim: `(- (* 5 (pow 2 3)) 1)` ≡ `39`.
   

   Proof. The left-hand side of the equivalence evaluates as follows:

       (- (* 5 (pow 2 3)) 1)
   --> (- (* 5 8) 1)
   --> (- 40 1)
   --> 39
   

Problem 2: Symbolic Reasoning with Xor

Consider the following definition of the boolean xor function:

(define xor
  (lambda (b1 b2)
    (if b1
       (not b2)
       b2)))

Prove the following claims about this function:

For this final equivalence, you may evaluate individual calls to and, or, and not, in a single step of evaluation.