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:

# One of our helper functions to get Scheme-like list behavior
# from Python lists. l[1:] returns all the elements of l,
# starting with index 1, i.e., without the head.
def tail(l):
    return l[1:]

def list_length(l):
    if l == []:
        return 0
    else:
        return 1 + list_length(tail(l))

We will prove the following claim:

Claim: (list_length [21, 7, 4]) ≡ 3.

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 my_length([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:

   ~~~latex

   And here it is it looks (roughly) when rendered:

   ---

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

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

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

   (Note: the long arrow --> is really - - > but the font I use for the website supports ligatures which renders the arrow as a single character instead.)

Problem 2: More Equivalences

Consider the following additional Racket functions:

# Helpers for Scheme-like manipulation of Python lists
def head(l):
    return l[0]

def cons(x, l):
    return [x] + l

def tail(l):
    return l[1:]

def list_replicate(x, n):
    if n == 0:
        return 0
    else:
        return cons(x, list_replicate(x, n-1))

def list_append(l1, l2):
    if l1 == []:
        return l2
    else:
        return cons(head(l1), append(tail(l1), l2))

define list_filter(f, l):
    if l == []:
        return []
    elif f(head(l)):
        return cons(head(l), list_filter(f, tail(l)))
    else:
        return list_filter(f, tail(l))

Prove the following statements of equivalence. In your derivations, you may evaluate a function call to the (yet-to-be-evaluated) expression it returns in a single step of execution.

1. list_replicate('!', 3) ≡ ['!', '!', '!'].
2. (list_length(list_append [1, 2] [3, 4, 5])) ≡ list_length([1, 2]) + list_length([3, 4, 5])
3. list_length(list_filter(lambda x: x >= 0, [1, 2, 3, 4, 5])) <= 5 ≡ True

Problem 3: Dispute (Optional)

Show that the following equivalence does not hold by carrying through the evaluation and observing that both sides evaluate to different values.

• list_append(['a', 'b', 'c'], ['d']) ≡ list_append(['d'], ['a', 'b', 'c'])