Shorthand for Program Derivations

Most of the functions we will encounter from this point forward are simple conditionals, but our mental model can be quite verbose in these situations. For example, in our model, the conditional (if (< 0 (+ 1 2)) "hello" "goodbye") evaluates as follows:

    (if (< 0 (+ 1 2)) "hello" "goodbye")
--> (if (< 0 3) "hello" "goodbye")
--> (if #t "hello" "goodbye")
--> "hello"

While precise, these steps will obscure the broader argument we are trying to make for our program.

To make our program derivations more readable, we will use shorthand for this lab when evaluating conditionals.

You are free to evaluate a function whose body is a conditional, cond, or match expression directly to the branch that it evaluates to without the need for showing intermediate steps.

The execution of the above conditional would then be written as:

     (if (< 0 (+ 1 2)) "hello" "goodbye")
-->* "hello"

We use the notation -->* (LaTeX: \longrightarrow^*, Unicode: ⟶*) to mean that multiple evaluation steps happened between the two lines of the derivation.

Problem 1: Narrowing Down the Possibilities

Consider the following Racket functions:

(define f1
  (lambda (name)
    (cond [(equal? name "Alice")        0]      ; Point A
          [(equal? name "Bob")          1]      ; Point B
          [(equal? name "Carol")        2]      ; Point C
          [(not (equal? name "Daniel")) 3]      ; Point D
          [(not (equal? name "Emily"))  4])))   ; Point E

(define f2
  (lambda (x y)
    (cond
          [(>= y 1)                0]     ; Point A
          [(>= x 1)                1]     ; Point B
          [(== x -1)               2]     ; Point C
          [(or (<= x -5) (>= y 3)) 3]     ; Point D
          [(== x 0)                4]     ; Point E
          [(== x y)                5])))  ; Point F

For each of the Racket functions

1. Identify the types of each of the parameters
2. Describe the set of assumptions we know are true about the parameters inside the branch expression at each labeled point, i.e., when that branch’s guard is #t.
3. Are each of the conditionals exhaustive? If not, describe what values are not covered by the cond expression.

Problem 2: Capture

Consider the following Racket function that computes a report for a student given their current grades in a course:

(define report
  (lambda (hw-avg quiz1 quiz2 quiz3)
    (cond [(and (> hw-avg 90) (> quiz1 90) (> quiz2 90) (> quiz3 90)) "excelling"]
          [(and (> hw-avg 75) (<= quiz1 quiz2) (<= quiz2 quiz3))      "progressing"]
          [(or (< hw-avg 60) (< quiz1 60) (< quiz2 60) (< quiz3 60))  "needs help"]
          [else                                                       "just fine"])))

1. Describe the preconditions (both in terms of types and general constraints) on the parameters.
2. Describe the conditions under which (report hw-avg quiz1 quiz2 quiz3) will return "just fine".
3. Are there any conditions under which the function reports an inappropriate string, given the arguments.

Problem 3: Looking Ahead

In this problem, we’ll motivate our discussion for next week on recursion and induction. Consider the standard append function for lists.

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

1. While the function is recursive, our substitutive model of computation is capable of modeling the behavior of this function. Thus, we can prove properties about append just like any other function. Prove this one as an exercise:

   Claim (Nil Is An Identity on the Left): for any list l, (append '() l) ≡ l.

2. We say that an operation is commutative if we can swap the order of the objects involved, i.e., if \(x \equiv y\) then \(y \equiv x\) and vice versa. This is true for some operations, e.g., integers and addition, but not other, e.g., integers and subtraction. It turns out that append is not commutative for lists! Prove this fact by way of a counterexample:

   Claim (Append is Not Commutative): there exists lists l1 and l2 such that (append l1 l2) \(\not\equiv\) (append l2 l1).

3. Because append is not commutative, this means that just because the empty list is an identity on the left-hand side of the function, it is not necessarily an identity on the right-hand side. With a little bit of thought, though, we can convince ourselves this ought to be the case. However, proving this fact is deceptively difficult! Attempt to prove this claim:

   Claim (Nil Is An Identity on the Right): for any list l, (append l '()) ≡ l.

   (Hint: you can perform case analysis on each new list you encounter in your proof, even the tail of the original list!)

   At some point, you will get stuck, ideally at a point where you start seeing that your reasoning will go on infinitely. Check with an instructor that you have indeed gotten stuck at the “right point.”

4. Finally, reflect on your experience. Answering the following questions in a few sentences each:

   • Why were you able to directly prove the left-identity claim?
   • Why is the right-identity claim more difficult to prove?
   • What information do you need in order to break the chain of infinite reason that you found in the previous proof?