CSC 208-01 (Spring 2023)

Lab: 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. For example, in our model, the conditional:

[[ if 0 < 1 + 2:
       return 'hello'
   else:
       return 'goodbye' ]]

Evaluates as follows:

    [[ if 0 < 1 + 2:
           return 'hello'
       else:
           return 'goodbye' ]]
--> [[ if 0 < 3:
           return 'hello'
       else:
           return 'goodbye' ]]
--> [[ if True:
           return 'hello'
       else:
           return 'goodbye' ]]
--> [[ return 'hello' ]]
--> '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 to the expression of the return statement contained in that branch without the need for additional intermediate steps.

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

     [[ if 0 < 1 + 2:
            return 'hello'
        else:
            return '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 Python functions:

def f1(name):
    if name == 'Alice':
        return 0         # Point A
    elif name == 'Bob':
        return 1         # Point B
    elif name == 'Carol':
        return 2         # Point C
    elif name != 'Alice':
        return 3         # Point D
    elif name != 'Emily':
        return 4         # Point E

def f2(x, y):
    if y >= 1:
        return 0         # Point A
    elif x >= 1:
        return 1         # Point B
    elif x == -1:
        return 2         # Point C
    elif x <= -5 or y >= 3:
        return 3         # Point D
    elif x == 0:
        return 4         # Point E
    elif x == y:
        return 5         # Point F

For each of these 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 True.
  3. Are each of the conditionals exhaustive? If not, describe what values are not covered by the conditional

Problem 2: Capture

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

def report(hw_avg, quiz1, quiz2, quiz3):
    if hw_avg > 90 and quiz1 > 90 and quiz2 > 90 and quiz3 > 90:
        return 'excelling'
    elif hw_avg > 75 and quiz1 <= quiz2 and quiz2 <= quiz3:
        return 'progressing'
    elif hw_avg < 60 or quiz1 < 60 or quiz2 < 60 or quiz3 < 60:
        return 'needs help'
    else:
        return '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 recursive implementation of append for lists:

def head(l):
    return l[0]

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

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

def list_append(l1, l2):
    if l1 == []:
        return l2
    else:
        return cons(head(l1), list_append(tail(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 (Null Is An Identity on the Left): for any list l, list_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 list_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 list_append(l1, l2) \(\not\equiv\) list_append(l2, l1).

  3. Because list_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, list_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?