Computer Aided Formal Reasoning 1996/7 Lecture notes 5 Judith Underwood

Data types and computation

We have been looking at a proof system for propositional logic with proof terms. The proof terms correspond to simply typed lambda calculus, with extra operators for pairing and disjoint union. We also saw how these proof terms computed, so that one proof might reduce to another proof. This partly justifies our interpretation of these proof terms as a programs, though we have not yet seen any particularly useful programs. For this, we really need data for the programs to operate on.

Today, then, we’ll shift emphasis somewhat to the interpretation of formulas and proofs as types and programs. For now, the words “formula” and “type” are virtually interchangeable; since I want to think of programs, I’ll tend to use the word “type”, but keep in mind that this includes the formulas we’ve used before. We’ll extend the proof system for formulas to include proofs (and therefore programs) involving natural numbers, booleans, and lists. We’ll also look at the computational meaning of proof terms through their reduction rules.

We extend the language of formulas/types with two base types, bool for Booleans and nat for natural numbers, and a parameterized type list t, where t is a type. (This parameterization works in much the same way as the quantified axiom schemas we saw last time.) Just as we saw with formulas, we will have introduction and elimination rules for each type. The introduction rules for data types will determine how elements of the type are created. The elimination rule for a type defines how elements of that type may be used in computation.

Rules

Recall we use G to denote our list of assumptions, which will now be interpreted as a sequence of variables with types, e.g. x:nat, b:bool. In the rules below, s and t are type variables, i.e. they can be replaced with any type.

Type  Introduction operators  Elimination operators

     bool
                  G ⊢ true:bool

                                                   \frac{G ⊢ m:t   G ⊢ n:t   G ⊢ b:bool}{G ⊢ bool rec m n b:t}

                 G ⊢ false:bool
      nat
                  G ⊢ zero:nat

                                               G ⊢ m:t   G ⊢ f:nat->t->t    G ⊢ i:nat
                                                       G ⊢ nat rec m f i :  t

                  \frac{G ⊢ i:nat}{G ⊢ suc i:nat}

    list t
                 G ⊢ nil t:list t

                                         \frac{G ⊢ m:t   G ⊢ f:s->(list s) ->t ->t   G ⊢ l:list s}{G ⊢ list rec m f l:t}

             \frac{G ⊢ m:t   G ⊢ l:list t}{G ⊢ cons m l:list t}

The introduction rules for bool say that true and false are elements of bool. Note that false is not the same as absurd – false has type bool, whereas since absurd is a formula, it has type Prop.

The introduction rules for nat mean that elements of nat are either zero or suc applied to zero some number of times, e.g. suc (suc (suc zero)). suc is short for “successor”, so suc zero is one, suc (suc zero) is two, and so forth. For convenience, the Lego library lib nathas defined the names for numbers up to ten to be the appropriate element of nat, so that you can

type five instead of suc (suc (suc (suc (suc zero)))).

The introduction rules for list t mean that elements of list t are either the empty list of type t (called nil t), or they are the result of applying cons to a term of type t and a list of type t. Thus, the list “(1 2 3)” would be written

                   cons one (cons two (cons three (nil nat)))

This is an element of the type list nat; note that the final element of the list is nil nat, the empty list of type nat. Leaving out the type of nil will give you an error message.

Note: These are really inductive definitions of the datatypes. The mechanism by which they work is somewhat hidden – it lies in the fact that proofs themselves are inductively defined. So, the assertion that

                   cons one (cons two (cons three (nil nat)))

is an element of nat list is justified by the following derivation:

          ⋮ . ; ⊢ one:  nat

                        ⋮ . ; ⊢ two:  nat ⋮ .

                                      ⊢ three:  nat

                                                      nil nat:  list nat
                                      ⊢ cons three (nil nat):  list nat
                          ⊢ cons two (cons three (nil nat)):  list nat
             ⊢ cons one (cons two (cons three (nil nat))):  list nat

where I’ve left off the derivation of one:nat, etc.

It is slightly odd to think of these derivations as proofs. One way to do this is to interpret zero, suc zero, suc (suc zero), etc. as different proofs that there is something in the type of natural numbers. It is much easier to see that they are typing judgements.

The elimination rules allow us to define functions from each type to another type t. The operator bool rec is used to define functions from type bool to any other type; similarly, nat rec and list rec are used to define functions which respectively take a nat and a list t as arguments. We can type the elimination operators by quantifying over types, as we did last time:

bool_rec : {t|Type}t->t->bool->t
nat_rec :  {t|Type}t->(nat->t->t)->nat->t
list_rec : {s,t|Type}t->(s->(list s)->t->t)->(list s)->t

Notice that after the type variables have been instantiated, each operator takes two arguments and returns a function from the appropriate type to the type t. In order to compute with these functions, however, we need evaluation rules for them.

Evaluation and function definition

Defining evaluation rules for the elimination operators will allow us to treat proof terms as a programming language. The evaluation rule for each elimination operator shows how elements of each type are broken down and used in computation.

The evaluation rules are:

               ([x:t] m) n              => m[n/x]
               bool rec m n true        => m
               bool rec m n false       => n
               nat rec m f zero         => m
               nat rec m f (suc i)      => f i (nat rec m f i)
               list rec m f nil         => m
               list rec m f (cons n l)  => f n l (list rec m f l)

Recall the notation that m[n/x] means m with n substituted for x in a way that avoids capture of free variables.

Exercise: Check that applying an evaluation rule does not change the type of a term.

If you are used to a functional programming language like Lisp or Scheme, using an explicit recursion operator may seem strange at first. However, using these operators guarantees that our functions will terminate.

The simplest operator is bool rec. Because there are only two boolean values, there is no way to break down a boolean into something smaller. So, bool rec is just a kind of if with the arguments written in a different order. (In fact, if is defined in the library lib_bool_funs so that if b m n is the same as bool rec m n b.) For example, a function of type bool -> nat which returns one when applied to true and zero when applied to false can be defined

bool to nat = [b:bool] bool rec one zero b

This can be simplified. Any term of the form [x:A]f x is equivalent to the function f (at least in terms of the input and output values of the function), so we may write this function as

bool to nat = bool rec one zero

Exercise: Check that the type of [b:bool] bool_rec one zero b is bool -> nat using the rules above.

The nat_rec operator is more complex. We use it to define a function inductively, by giving a base case and an inductive case. For example, consider the function plus_two which returns its argument plus two. In another language we might write this as: plus two:

plus two = lambda j.  case j = zero return two
                           j = (suc n) return suc (plus two n)

We are defining plus two by induction on its argument j. In the base case, when j=zero, we return i. In the inductive case, when j= suc n, we define the value of the function on j by using the value on j-1 (= n). This is an example of a general pattern of well-founded inductive definitions – provide a base case and a function which, given information about the current stage of the computation and the value of the function on a smaller argument, computes the value of the function on the current argument. This is what nat rec does. The first argument to nat rec is the value of the function on zero. The second argument is a function which describes what to do in the inductive case. In particular, if the function g = nat rec i f is applied to suc n, then the function f (which describes the inductive case) is applied to two arguments, n and the value of g on n, to produce the value of g on suc n.

In the case of plus two, the value when j=zero is two, so that is the first argument to nat rec. The value when j= suc n is just the successor of the value of plus two on n – we do not need to use n explicitly to compute it. Hence, the second argument to nat rec is [k:nat][v:nat]suc v. This is equivalent to [k:nat]suc , so now we have

                  plus two = [j:nat] nat rec two ([k:nat] suc) j

We can now make this a general addition function by adding another argument i and returning i as the base case:

                 plus = [i:nat][j:nat] nat rec i ([k:nat] suc) j

To see how this evaluates, let’s look at 2 + 2. Using s for suc and 0 for zero we have

plus(s (s 0)) (s (s 0))
    = ([i:nat][j:nat] nat rec i ([k:nat] s) j) (s (s 0)) (s (s 0))
    = ([j:nat] nat rec (s (s 0) ([k:nat] s) j) (s (s 0)))
    = (nat rec (s (s 0)) ([k:nat] s) (s (s 0)) )
    = ([k:nat] s) (s 0) (nat rec (s (s 0)) ([k:nat] s) (s 0))
    = s (nat rec (s (s 0)) ([k:nat] suc) (s 0))
    = s ([k:nat] s) 0 (nat rec (s (s 0)) ([k:nat] s) 0)
    = s (s (nat rec (s (s 0)) ([k:nat] s) 0))
    = s (s (s (s 0)))

The list_rec operator is similar, except that the function which computes the inductive case takes three arguments: the head of the list, the tail of the list, and the value of the function on the tail. For example, given plus as defined above we can add all the elements of a list nat with the function:

list_rec zero
         [head:nat][tl:list nat][sum_tl:nat] plus h sum_tl

In Lego, you can write programs like this by refinement. For example, here is how I wrote the example above:

Lego> Goal sum_list:(list nat) -> nat;
Goal
  ?0 : (list nat)->nat
Lego> Refine list_rec;
Refine by  list_rec
  ?3 : nat
  ?4 : nat->(list nat)->nat->nat

Lego has determined that in order to get a function from list nat to nat using list_rec, I need to supply a base case and inductive case of the types given. First, the base case:

Lego> Refine zero;
Refine by  zero
  ?4 : nat->(list nat)->nat->nat

And then the inductive case:

Lego> intros head tl sum_tl;
intros (3) head tl sum_tl
  head : nat
  tl : list nat
  sum_tl : nat
  ?5 : nat
Lego> Refine plus head sum_tl;
Refine by  plus head sum_tl
Discharge..  sum_tl tl head
*** QED ***

I gave the variables introduced descriptive names (as one should always do) and then described how to compute the inductive case. Notice that this doesn’t depend on the tail of the list (tl); Lego replaces unused variable names by the dummy variable marker _as seen below:

Lego> Save;
"sum_list"  saved as global
Lego> sum_list;
value of sum_list = list_rec zero
        ([head:nat][_:list nat][sum_tl:nat]plus head sum_tl)
type  of sum_list = (list nat)->nat

Now that we can write functions, we will want to reason about them. Before we can prove interesting theorems, we need two important things: a notion of equality and a method for doing proofs by induction. We’ll do these next week.

Exercises:

  1. Given plus, write times: nat -> nat -> nat.

2. Write pred:nat->nat, the predecessor function which, given n, returns n-1. Consider that the predecessor of zero is zero.

3. Write minus:nat->nat->nat. Consider that the result is zero if the second argument is larger than the first.

4. Write iszero:nat->bool, which returns true if its argument is zero and false otherwise.

5. Write length:{t|Type}(list t)->nat. If you begin with this as a goal, you will have to introduce the type variable with an initial intros t command.

6. Write append:{t|Type}(list t)->(list t)->(list t). which concatenates its argu-

ments.

7. Write contains_zero:(list nat) -> bool, which returns true if and only if zero is in

the list. Hint: you will need both list_rec and bool_rec. You will probably want to use iszero as well.