Computer Aided Formal Reasoning Fall, 1995 Lecture notes 1 Rod Burstall and Judith Underwood

The course now has a home page, accessible from the main LEGO page at

         http://www.dcs.ed.ac.uk/generated/package-links/lego/

Electronic copies of lecture notes and other information will appear here regularly.

The first tutorials on LEGO will be Friday, 13 October, in or near room 2501. Two periods have been scheduled, at 10:00am and 4:00pm.

Both lectures next week will be informal tutorials, starting in room 3317 as usual but possibly moving to 2501.

Functional programming with recursion operators

We define a simple functional language with limited data types. This will illustrate the language definition method on a fairly familiar example. It also introduces programming with recursion operators instead of general recursion. This means that evaluation terminates for all terms.

Types and terms

Notation: We use the following meta-variables to explain the syntax and rules:

s, t types
m ,n general terms
b, c bool

i, j nat

k, l list
f, g function
u, w pair
x, y variables

Construction of types and terms: The language includes pairs, functions, booleans, natural numbers and lists.

Type constructor Introduction operators Elimination operators

s#t              (m, n)               mn.1 mn.2
s->t             [x:  s] m            f m
bool             true, false          bool rec m n b
nat              zero, suc            nat rec m f i
list t           nil t , cons         list rec m f l

Note that [x:s] m is conventionally written “λ x: s. m”. The type of lists takes a parameter, t, which is the type of the elements of the list. Note also

that nil has a “subscript” t to show that it is an empty list of elements of type t. In LEGO, this will appear as “nil t”. For all other terms you can find the type by inspection using the following rules.

Typing rules:

We use G to denote a context, a sequence of variables with types, e.g. x:nat, b:bool.

Type  Introduction operators  Elimination operators

   s#t       \frac{G|-m:s    G|-n:t}{G|-(m, n):s#t}       \frac{G|-u:  s#t}{G|-u.1:s} \frac{G|-u:  s#t}{G|-u.2:t}

  s->t     \frac{G, x:s |-m:t}{G|-[x:s] m :  s->t}                     \frac{G|-f:s->t   G|-m:s}{G|-f m:t}

  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
               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}

Evaluation rules

We need an evaluation rule for each elimination operator.

Notation: m[n/x] means m with n substituted for x (see below for definition).

(m,n).1                  => m
(m,n).2                  => n
([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)

Free variables and substitution

We first the define the free variables of a term

FV(x)  = x
FV(m,n)  = FV(m) ∪ FV(n)
FV(u.1)  = FV(u)
FV(u.2)  = FV(u)
FV([x:t] m) = FV(m) -{x}
FV(m n)  = FV(m) ∪ FV(n)
FV(true)  = {}

and so on– the set of free variables of other terms is just the union of the sets of free variables of the subterms.

Now we define substitution, m[n/x], m with n substituted for x. Usually we think of all this as a notation needed to explain the functional language, rather than presenting further rules of evaluation.

The main point is that when we substitute a term for a variable we must make sure that no free variables get captured by a lambda, i.e. by [.. : ..]. For example, if we substitute f x for something we had better not let it get inside [x:t] because the x would get “captured”.

    x[n/x]          =  n
    y[n/x]          =  y  if y≠x
    (m,m')[n/x]     =  (m[n/x], m'[n/x])
    m.1[n/x]        =  m[n/x].1
    m.2[n/x]        =  m[n/x].2
    (m m') [n/x]    =  (m[n/x] ) (m'[n/x] )
    ([x:t] m)[n/x]  =  [x:t] m
    ([y:t] m)[n/x]  =  [y:t] (m[n/x] )  if y≠x and y is not in FV(n)

([y:t] m)       =  ([z:t] m[z/y])  if z is not in FV(m) (called rule α)

    true [n/x]      =  true

and so on.

Defining functions in this language

If you are used to a functional programming language like Lisp or Scheme, using a recursion operator may seem strange at first.

For example, consider the addition function plus. In another language we might write this as:

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

Note that i is not changed in the body of the function, so that if we consider a fixed i, we can look at this as a function which adds i to its argument. Let’s make this a bit more explicit by giving this function a name, plus i:

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

Now it is clear that we are defining plus i 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 g = nat rec i f is applied to suc(n), f 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 i, the value when j=zero is i, so that is the first argument to nat rec. The value when j= suc(n) is just the successor of the value of plus i 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 i = [j:nat] nat rec i ([k:nat] suc) j

giving (finally!)

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

As an example of 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] suc) j) (s (s 0)) (s (s 0))
  = ([j:nat] nat rec (s (s 0) ([k:nat] suc) j) (s (s 0)))
  = (nat rec (s (s 0)) ([k:nat] suc) (s (s 0)) )
  = (([k:nat] s) (s 0)) (nat rec (s (s 0)) ([k:nat] suc) (s (s 0)) )
  = s (nat rec (s (s 0)) ([k:nat] suc) (s 0))
  =

and so on.

Exercises

1. Complete the calculation above to get the answer s(s(s(s 0))).

2. Define times – you may use plus.

3. Define factorial.

4. Define not on type bool.

5. Define and on bool.

6. Define append of two lists and reverse of a list.

7. Define the sum of the elements of a list.