Assumptions in proofs

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. Consider the following toy function:

(define f
  (lambda (x)
    (if (< 0 (+ x 2))
        "hello"
        "goodbye")))

For example, in our model, the function call (f 1) evaluates as follows:

    (f 1)
--> (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 function calls:

You are free to evaluate a function call whose body is a conditional or match directly to the branch expression of that conditional or match that is eventually chosen.

If the expression above came about from a function call, say (f 1), we would write the evaluation of that call as:

     (f 1) 
-->* "hello"

Skipping over the explicit execution of the statement-expression that the function call evaluates to in our model. We use the notation -->* (LaTeX: \longrightarrow^*, Unicode: ⟶*) to mean that multiple evaluation steps happened between the two lines of the derivation.

Be aware that whenever we skip steps, we introduce the possibility of making an error in our reasoning! So double-check your work whenever you skip steps in this manner!

Problem: Narrowing Down the Possibilities

Consider the following functions:

(define f1
  (lambda (name)
    (cond
      [(equal? name "Alice")
       0] ; Point A
      [(equal? name "Bob")
       1] ; Point B
      [(equal? name "Carol")
       2] ; Point C
      [(equal? name "Daniel")
       3] ; Point D
      [(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
      [(zero? x)
       4] ; Point E
      [(= x y)
       5]))) ; Point F

For each of the functions:

1. Identify the types of each of the parameters
2. Describe the set of assumptions we know are true about the parameters inside each branch 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 if-else statements.

Problem: Capture

Consider the following 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". Describe them in terms of properties that ought to hold on each parameter to the function.
3. Are there any conditions under which the function reports an inappropriate string, given the arguments and your interpretation of the function's intended behavior?

Problem: Looking Ahead

In this problem, we'll motivate our discussion for next period 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)))))

Part 1: Simple Reasoning About Append

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:

Part 2: (Not) Commutativity

We say that an operation is commutative if we can swap the order of the objects involved, i.e., if x ≡ y then y ≡ 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:

Part 3: A Humble Attempt

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:

(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."

Part 4: Reflection

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?