Lab: Exploring Python

Today, we’ll explore our first mathematical model, a substitutive semantics for Python programs.

LaTeX and the CSC208 Package

For each lab and demonstration exercise, you will submit a final LaTeX-generated PDF with your solutions. To help format your files, we’ve created a LaTeX template template for you to use. You can download the template here:

• csc208_template.tex

The template includes a number of standard packages and formats the document to look like a more traditional document, i.e., not in narrow column format.

To get started, simply download the file and import it into a new Overleaf project. Make sure to fill in the \title, \author, and \grinnellusername macros at the top of the file with the appropriate information!

For each problem, you should use the \begin{problem} ... \end{problem} environment to format your solutions by problem. Note that the environment puts each problem on a new page!

Problem 1: What’s in a name?

A strength of possessing an explicit computation model is explaining tricky corner cases in the language’s design. In this problem, we’ll look at some of the issues arising with names in Python.

Consider the following function definitions.

def f1(x, y):
    return x + y + x

def f2(n):
    return n * 3

def f3(n):
    return f2(4) + f2(n) + n

1. Give execution traces for each of the following expressions. Try to let each member of your group take the lead on writing down the derivation, so everyone gets their practice in. The remaining members of the group should check their work.

   When formatting your traces, use the \begin{verbatim} ... \end{verbatim} environment. Importantly, verbatim will allow a chunk of text to leak off the page if it is too big. If this is the case, please properly format your document by introducing newlines and/or breaking up your trace into multiple verbatim blocks!

   • f1(1+2, 7)
   • f2(f2(f3(5)))
   • f3(11)

2. Consider an alternative definition of f2 given below:

   def f2(x):
       return x * 3
   

   Compare the second expression’s execution from the last part (f2(f2(f5(5)))) with the old and new definitions of f2. In a few sentences:

   • Comment on the behavior of both versions of f2. Do they behave the same or differently?
   • From this example, what can you say about the choice of names of function parameters between different functions. Does it matter what names you choose? Why or why not?

3. Now consider the following top-level declarations:

   value = 12              # A
   
   print(value)            # 1
   
   def f(value):           # B
       x = value           # 2
       value = 5           
       return x + value    # 3
   
   f(value)                # 4
   print(value)            # 5
   

   Give an execution trace for the expression on line 4. Double-check your final result in Python.

4. Based on your derivation, determine which definitions of value (points labeled A–C) are used for each usage of value in f, i.e., the points labeled 1–5.

5. Give a rule for determining which of the definitions of a variable applies to some use of that variable. Once you have a candidate rule, check your answer with a member of the course staff.

Problem 2: Loop the Loop

Another corner case in the evaluation of Python programs concerns non-termination. Consider the following recursive function:

# Returns a new list that is l with x in head position
def cons(x, l):
    return [x, *l]

def mystery(n, x)
    if n == 0:
        return []
    else:
        return cons(x, mystery(n - 1), x)

1. Give execution traces for each of the following expressions. Again, let every group member take lead on at least one of the expressions. Note that we didn’t talk about recursion in the reading! However, there is nothing new to say here—recursion “just works” in this model, so follow your nose!

   • mystery(0, 10)
   • mystery(1, "a")
   • mystery(3, False)

   In a sentence or two describe what this function does.

2. Now, trace the execution of this expression. What happens to your execution trace for this expression? Give enough of your trace to explain what is going on.

   • mystery(-1, "q")

3. Run this expression in Python. What happens? Try to reconcile explain the behavior of Python in terms of how your trace played out.

4. Try tracing this curious expression:

   • (lambda x: x(x))(lambda x: x(x))

   Be very careful about variable names and substitution here! What happens to your execution trace for this expression? Give enough of your trace to explain what is going on.

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

def is_empty(l):
    return len(l) == 0

def head(l):
    return l[0]

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

def cons(x, l)
    return [x, *l]

def list_length(l):
    if is_empty(l):
        return 0
    else:
        return 1 + list_length(tail(l))

We will prove the following claim:

~~~admonish problem title=”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 `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:

~~~admonish check title="Sample Proof"
    Claim: `5 * pow(2, 3) - 1` ≡ `39`.

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

    ```python
        5 * pow(2, 3) - 1
    --> 5 * 8 - 1
    --> 40 - 1
    --> 39
    ```
    □