CSC 208-01 (Spring 2023)

Reading: Propositions and Symbolic Execution

Note: for each reading, you will need to complete a few exercises These daily drills are exercises marked with a double dagger, . There are two in this reading, concrete equivalences and quantified propositions. You can submit your answers via plaintext to Gradescope.

Don’t worry if you feel like you didn’t get the right answer for the daily drills! It is more important that you put in the effort, e.g., 10 minutes trying out each of the problems, and that you come to class with any questions about the content and the drills.

Propositions and Proofs

Our formal model of computation allows us to reason about the behavior of programs. But to what ends can we apply this reasoning? Besides merely checking our work, we can also use our formal model to prove propositions about our programs.

Proposition: a proposition is an assertion or statement, potentially provable.

Another word for a proposition is a claim. Here are some example propositions over programs that we could consider:

The first proposition is a fully concrete proposition of the sort we have previously considered. The second is an abstract proposition because it involves a variable, here l.

Ultimately, the first two propositions involve equivalences between expressions. But propositions do not need to be restricted to equivalences. The third proposition talks about the number of operations that one expression performs relative to another.

Furthermore, propositions don’t even need to be provable! For example, the final proposition is not provable. A counterexample to this proposition arises when we consider n = -1. 2 * -1 evaluates to -2, and -2 is not greater than -1!

“True” versus “Provable”: in our discussion of logic and its applications to program correctness, we will need to discuss both boolean expressions as well as propositions. There exist commonalities between both—they involve truth and falseness. However, booleans exist inside our model, i.e., at the level of programs. Propositions exist outside of the model as they ultimately are statements about the model.

To distinguish between the two, we’ll use the terms True and False when discussing booleans and “provable” and “refutable” when discussing propositions. We should think of boolean expressions as evaluating to True or False. In contrast, we will employ logical reasoning to show that a proposition is provable or refutable.

Equivalences Between Expressions

Of the many sorts of propositions possible, we will work exclusively with equivalences in our discussion of program correctness.

Program Equivalence: two expressions \(e_1\) and \(e_2\) are equivalent, written \(e_1 \equiv e_2\) (LaTeX: \equiv, Unicode: ≡) if \(e_1 \longrightarrow^* v\) and \(e_2 \longrightarrow^* v\).

Recall that \(e \longrightarrow e'\) (“steps to”, LaTeX: \longrightarrow) means that the (Python) expression \(e\) takes a single step of evaluation to \(e'\) in our mental model of computation. The notation \(e \longrightarrow^* e'\) (“evaluates to”, LaTeX: \longrightarrow^*) means that \(e\) takes zero or more steps to arrive at \(e'\). With this in mind, the formal definition of equivalence amounts to saying the following:

Two expressions are equivalent if they evaluate to identical values.

Thus, we can prove a claim of program equivalence by using our mental model to give a step-by-step derivation (an execution trace) of an expression to a final value. If both sides of the equivalence evaluate to the same value, then we know they are equivalent by our definition! The execution trace itself is a proof that the equivalence holds.

For example, consider the following recursive definition of factorial:

def factorial(n):
    if n == 0:
        return 1
    else:
        return n * factorial(n-1)

and subsequent claim about its behavior:

Claim: factorial(3) \(\equiv\) 6.

We can prove this claim by evaluating the left-hand side of the equivalence and observing that it is identical to the right-hand side:

Proof. The left-hand side expression evaluates as follows:

    factorial(3)
--> [[
      if 3 == 0:
          return 1
      else:
          return 3 * factorial(3-1)
    ]]
--> [[
      if False:
          return 1
      else:
          return 3 * factorial(3-1)
    ]]
--> [[
      return 3 * factorial(3-1)
    ]]
--> [[
      return 3 * factorial(2)
    ]]
--> [[ return 3 * [[
        if 2 == 0:
            return 1
        else:
            return 2 * factorial(2-1)
      ]]
    ]]
--> [[ return 3 * [[
        if False:
            return 1
        else:
            return 2 * factorial(2-1)
      ]]
    ]]
--> [[ return 3 * [[
        return 2 * factorial(2-1)
      ]]
    ]]
--> [[ return 3 * [[
        return 2 * factorial(1)
      ]]
    ]]
--> [[ return 3 * [[ return 2 * [[ 
          if 1 == 0:
              return 1
          else:
              1 * factorial(1-1)
        ]]
      ]]
    ]]
--> [[ return 3 * [[ return 2 * [[ 
          if False:
              return 1
          else:
              return 1 * factorial(1-1)
        ]]
      ]]
    ]]
--> [[ return 3 * [[ return 2 * [[ 
          return 1 * factorial(1-1)
        ]]
      ]]
    ]]
--> [[ return 3 * [[ return 2 * [[ 
          return 1 * factorial(0)
        ]]
      ]]
    ]]
--> [[ return 3 * [[ return 2 * [[ return 1 * [[
            if 0 == 0:
                return 1
            else:
                return 0 * factorial(0-1)
          ]]
        ]]
      ]]
    ]]
--> [[ return 3 * [[ return 2 * [[ return 1 * [[
            if True:
                return 1
            else:
                return 0 * factorial(0-1)
          ]]
        ]]
      ]]
    ]]
--> [[ return 3 * [[ return 2 * [[ return 1 * [[ return 1 ]] ]] ]] ]]
--> [[ return 3 * [[ return 2 * [[ return 1 * 1 ]] ]] ]]
--> [[ return 3 * [[ return 2 * [[ return 1 ]] ]] ]]
--> [[ return 3 * [[ return 2 * 1 ]] ]]
--> [[ return 3 * [[ return 2 ]] ]]
--> [[ return 3 * 2 ]]
--> [[ return 6 ]]
--> 6

Whew! This precise step-by-step analysis of the behavior of the expression rigorously proves our claim!

Formatting Proofs

We will use this standard format for writing formal proofs for the remainder of the course. In summary, we write:

Claim: (The claim to be proven)

Proof. (The proof of the claim)

In LaTeX, the \begin{proof} ... \end{proof} environment is used to typeset proofs. Additionally, in our lab .tex files, we define the \begin{claim} ... \end{claim} with the amsthm package to typeset claims. Here is a LaTeX template that uses these environments that you can use to achieve the desired effect:

\begin{claim}
  % The claim to be proven
\end{claim}
\begin{proof}
  % The proof of the claim
\end{proof}

Exercise (concrete equivalences, ‡): Prove the following claim over concrete expressions:

Claim: 1 + 2 + 3 \(\equiv\) (3 * (3 + 1)) / 2.

Write our your proof in the format described above.

Symbolic Execution

Previously, we introduced a model of computation for the Python programming language. This model allows us to prove program properties when concrete values are involved. However, we frequently wish to prove properties where the values are unknown. For example, we might consider a proposition about appending two lists which is accomplished via the + operator:

For all lists l1 and l2, len(l1) + len(l2) = len(l1 + l2)

This proposition ranges over unknown, rather than concrete, lists. We, therefore, need to upgrade our mental model to work with these unknown quantities.

Abstract Propositions

Up to this point, we have considered concrete expressions, i.e., expressions that do not contain variables. What happens if we allow expressions to contain variables. As an example, consider the following implementation of boolean and:

# N.B. non-short-circuiting version of `and`
def my_and(b1, b2):
    if b1:
        return b2
    else:
        return False

Now, let’s consider the following equivalence claim:

Claim: my_and(True, b)False

Here, b is a variable, presumed to be of boolean type. However, how do we interpret b? It turns out there are two interpretations we might consider:

The former interpretation is called an existential quantification of b. We alternatively say that b is existentially quantified or is an “existential.” Quantification refers to the fact that our interpretation tells us “how many” values of b to consider in the proposition. In existential quantification, we consider a single value.

In contrast, the latter interpretation is called a universal quantification of b. In universal quantification, we mean that the proposition holds for all possible values of b. Note that the above proposition is provable if b is interpreted existentially: if we let b be #f then:

    my_and(True, b)
  ≡ my_and(True, False)
  ≡ [[
      if True:
          return False
      else:
          return False
    ]]
--> [[ return False ]]
--> False

However, the proposition does not hold when b is universally quantified. More specifically, while it holds when b is False, it does not hold when b is True.

    my_and(True, b)
  ≡ my_and(True, True)
  ≡ [[
      if True:
          return True
      else:
          return False
    ]]
--> [[ return True ]]
--> True

Because of this, we must be explicit when introducing variables into our proposition. For each such variable, we must declare whether it is existentially quantified and universally quantified. To do so, we can use the words:

Furthermore, we reason about the variable differently depending on its quantification, as we see in the following sections.

Exercise (Quantified Propositions): write down an additional existential and universal claim involving the my-and function.

Existential Propositions

If a variable \(x\) appears as an existential in a proposition, we interpret that variable as: there exists a value for \(x\) such that the proposition holds. In other words, the proposition is provable if we can give a single value to substitute for \(x\) so that the resulting proposition is provable. Thus, to prove an existential claim, we can choose such a value, substitute for the existential variable, and then use concrete evaluation as before.

As an example, let’s formally prove the existential version of the my_and claim that we introduced above:

Claim: there exists a boolean b such that my_and(True, b)False.

Proof. Let b be False. Then we have:

    my_and(True, False)
--> [[
      if True:
          return False
      else:
          return False
    ]]
--> [[ return False ]]
--> False

Note how our proof has changed now that our proposition is abstract:

  1. In our claim, we explicitly quantify the variable b by declaring it existential by using “there exists” to describe it.
  2. In our proof, we explicitly choose a value for the existentially quantified variable (“Let b be False”).

We can also existentially quantify over multiple variables. In these situations, we provide instantiations for each variable but otherwise proceed as normal.

For example, consider the following function that compares two numbers:

def compare_score(s1, s2):
    if s1 > s2:
        return 's1 wins!'
    else:
        return 's2 wins!'

Claim: There exists numbers x and y such that compare_score(x, y)'s2 wins!

Proof. Let s1 = 0 and s2 = 1.

    compare_score(0, 1)
--> [[
      if 0 > 1:
          return 's1 wins!'
      else:
          return 's2 wins!'
    ]]
--> [[
      if False:
          return 's1 wins!'
      else:
          return 's2 wins!'
    ]]
--> [[ return 's2 wins!' ]]
--> 's2 wins!'

Exercise (Alternative Instantiations): revise the proof of compare_score above by choosing alternative instantiations for s1 and s2 and deriving an alternative execution trace for the expression.

Universal Quantification

When a variable is universally quantified, it stands for any possible value. Let’s take a look at a simple squaring function:

def square(n):
    return n * n

And a simple universal claim about this function:

Claim: for all numbers n, square(n)n * n

Because the claim holds for all possible values of n, we can’t choose an n like with existentials. Instead, we must hold n abstract, i.e., consider it to be an arbitrary number, and then proceed with the proof. In effect, because n is universally quantified, we treat n like a constant, yet unknown, quantity in our reasoning.

Variables versus Unknown Constants: it may seem pedantic to distinguish between a variable and a constant of unknown quantity. However, there a subtle yet essential difference between the two concepts. A variable is an object in a proposition that must be quantified to give it meaning. An unknown constant already has meaning—it is known to be a single value. However, we don’t assume anything about the variable’s identity beyond what we already know, e.g., whether it is a list or a number.

When we use our mental model of computation, we immediately arrive at a problem: both square(n) and n * n cannot take any evaluation steps! square(n) cannot step because n needs to be a value before we perform the function application, and we said that values were numbers, boolean constants, or lambdas. n * n cannot step because since we don’t know what n is, we don’t know what concrete value the multiplication will produce. We say that both expressions are stuck: they are not values, but they cannot take any additional evaluation steps.

We can’t reconcile the n * n case. Without knowing what n is, we cannot carry out the multiplication. However, if we treat the constant-yet-unknown n as a value, then we can proceed with the function application. Furthermore, when we reach the return statement, we can simply return the stuck evaluation as the result of the function call instead of trying to evaluate it to a value first!

    square(n)
--> [[ return n * n ]]
--> n * n

Even though the left- and right-hand sides of the equivalence are not values, they are identical. This fact is sufficient to conclude that the two original expressions are equivalent according to our definition of program equivalences! Let’s put these ideas together into a complete proof of the proposition:

Claim: for all numbers n, square(n)n * n.

Proof. Let n be an arbitrary number. Then the left-hand side of the equivalence simplifies as follows:

    square(n)
--> [[ return n * n ]]
--> n * n

Which is identical to the right-hand side.

In summary, when we encounter a universally quantified variable in a proposition, we:

  1. Consider the variable to be a constant, yet unknown value. For convenience, we keep the name of this constant to be the same as the (universally quantified) variable, but we understand that the two are different objects!
  2. When reasoning about the constant, we assume that it is a value for the purposes of our mental model of computation.

Case Analysis

Sometimes when we work with universally quantified variables, we can get away without thinking about their actual values. However, more often or not, our reasoning must consider their possible values. This reasoning will ultimately depend on the types of values involved, and this is where our proofs get more intricate in their design!

As an introduction to these concepts, let’s consider the case where we know the type in question only allows for a finite set of values. At present, only the boolean type has this property. Booleans only allow for two values, True and False, whereas there are an infinite number of numbers and functions to choose from!

To see how we can take advantage of the finiteness of the boolean type in our proofs, let’s consider the following simple claim, again using the my_and function:

Claim: for all booleans b, my_and(b, False)False.

If we let b be arbitrary, we can begin evaluating the left-hand expression.

    my_and(b, False)
--> [[
      if b:
        return False
      else:
        return False
    ]]

We can see pretty readily that no matter how the conditional evaluates, we will return False. Be careful, though; this intuition is not sufficient for formal proof! We must instead rely on our evaluation model directly to ultimately show that this intuition is correct. However, if b is unknown, we don’t know which branch the conditional will produce.

Thankfully, we assumed that b was a boolean, so it must either be True or False. Therefore, we can proceed by case analysis: we will consider two separate cases, b is True and b is False, and show that the claim holds in both cases. If the claim holds for both cases, we know that the claim holds for every possible value of b and, thus, have completed the proof.

Proof. Let b be an arbitrary boolean. The left-hand side of the equivalence evaluates as follows:

    my_and(b, False)
--> [[
      if b:
        return False
      else:
        return False
    ]]

Because b is a boolean, either b is True or b is False.

  • b is True. Then:

    --> [[
        if True:
            return False
        else:
            return False
        ]]
    --> [[ return False ]]
    --> False
  • b is #f. Then:

    --> [[
        if False:
            return False
        else:
            return False
        ]]
    --> [[ return False ]]
    --> False

In both cases, the left-hand side steps to False, precisely the right-hand side of the equivalence.

Typesetting Cases: when performing a case analysis, it is imperative to state the proof’s different cases explicitly. To format this in LaTeX, use a bulleted lists, e.g.,

Because \verb|b| is a boolean, either \verb|b| is \verb|True| or \verb|b| is \verb|#f|.

\begin{itemize}
  \item \textbf{\verb|b| is \verb|True|}. Then:
    \begin{verbatim}
    --> [[
        if True:
            return False
        else:
            return False
        ]]
    --> [[ return False ]]
    --> False
    \end{verbatim}

  \item \textbf{\verb|b| is \verb|False|}. Then:
    Then:
    \begin{verbatim}
    --> [[
        if False:
            return False
        else:
            return False
        ]]
    --> [[ return False ]]
    --> False
    \end{verbatim}

In both cases, the left-hand side steps to \verb|#f|, precisely the right-hand side of the equivalence.

Note how I bold each case at the start of the bullet to clearly separate the statement of the case from the subsequent proof.

Exercise (Order of Reasoning): in the previous proof, we performed the case analysis on b after partially evaluating my_and. Rewrite the proof so that the case analysis happens before any evaluation occurs.

Exercise (Quantified Propositions, ‡): consider the following Python definition of the boolean disjunction, or, function:

def my_or(b1, b2):
    if b1:
        return True
    else:
        b2

Prove the following claims over this function:

  • Claim 1: there exists booleans b1 and b2 such that my_or(b1, b2)False.
  • Claim 2: for all booleans b, my_or(b, True)True.