Optional: Setup Markdown

Normally, I will encourage you to write your solutions to the labs on paper using Latex. However, for this lab, you can also use Markdwon to complete the first demonstration exercise. Individually, you and your group members should learn about Markdown and set up a Markdown environment with this supplementary reading:

• About Markdown

To complete this first problem, copy-and-paste the example Markdown source found at the end of the reading into the Problem 0 section of your document. Review this snippet to get an overview of how to structure your documents in the future. In particular, make sure to use top-level headings, e.g.,

# Problem 0: Setup Markdown

...

To indicate your answer to each problem.

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

Claim: (list-length '(21 7 4)) ≡ 3.

The equivalence symbol (≡), (LaTeX: \equiv) is 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 '(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:

   **Claim**: `(- (* 5 (expt 2 3)) 1)` ≡ `39`.
   
   _Proof_.
   The left-hand side of the equivalence evaluates as follows:
   
   ```racket
       (- (* 5 (expt 2 3)) 1)
   --> (- (* 5 8) 1)
   --> (- 40 1)
   --> 39
   ```

   And here it is how it actually looks 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:

(define list-replicate
  (lambda (x n)
    (if (zero? n)
        '()
        (cons x (list-replicate x (- n 1))))))


(define list-append
  (lambda (l1 l2)
    (if (null? l1)
        l2
        (cons (car l1) (list-append (cdr l1) l2)))))

Prove the following statements of equivalence. In your derivations, you may evaluate a function call to the its selected pattern match branch 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))).

Problem 3: 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.