Reasoning about recursive programs

Course notes of Prof. R.M. Burstall - University of Edinburgh

This document can be found on HTTP://WWW.CSI.UOttawa.CA/~luigi/csi5109/recursive.html

1. Introduction

This course teaches you how to reason mathematically about programs. For example to show that two different programs compute the same result (say a straightforward one and a faster trickier one), to show that a procedure with two arguments produces the same result if they are interchanged, or to show that a program produces results satisfying some mathematical specification.

Why bother? Normally anything we say about one of our programs rests upon (i) intuitive reasoning as we write or read it and (ii) debugging. But (i) is prone to mistakes and optimism, and (ii) only tells us about the behavior of the program for a (small) finite number of test inputs; it can only refute general statements about the programs, never prove them.

So mathematical proof gives us confidence in asserting general facts about the results of a program for all inputs.

Now a proof can be wrong, so have we just replaced bug- ridden programs by bug-ridden proofs?

There are easily mechanized ways to find syntactic errors in programs, but no easy way to find logical errors in programs.

There are easily mechanized ways to find syntactic errors in (formal) proofs, and easily mechanized ways to find logical errors in (formal) proofs (that is what formal logic's all about).

But how do we discover proofs (as opposed to checking them)? That is the big snag; it is hard work and machines can only render limited help. To get the advantage of machine- checkable proofs we need to express them in an absolutely formal language, very tedious for a human to use. If we use ordinary informal mathematical language it is easier for us to discover proofs but we cannot machine-check them.

A reasonable aim is a program which accepts an outline of proof from a human (main lemmas) and then discovers the proof itself (gap filling) and check it. Such programs exist but they are still too unhelpful and hard to use and so fail to make program proof an economic proposition. We are stuck with unreliable programs, never knowing if we have removed the last error.

So these lectures have a more modest aim; to show you how it is possible to say precise things about simple programs and then prove them. The extension to realistic programs is conceptually simple but practically still in the future.

2. Recursion equations: a simple programming language

We can do proofs for programs with assignment, jumps and procedures, but it is easier if we use a very simple recursive programming language, the 'recursion equation language'.

We use data structures of an expression-like (tree-like) form, defined inductively. The simplest of these is the natural numbers

So 1 is succ(0), 2 is succ(succ(0)) etc.

We can define functions over these data structures by recursion equations, for example

plus (0,n)      <= n                     (1)
plus(succ(m),n) <= succ(plus(m,n))       (2)

This forms a simple programming language. having defined some functions we can evaluate expressions using them. How does an interpreter for the language evaluate, say, plus(plus(succ(0),succ(0)),succ(0))?

We evaluate the innermost leftmost term first, as follows

When a match is found it defines values for the variables, m and n say, and these values are substituted in the right hand side of the equation and this is itself evaluated to give the result.

Example: evaluation of plus(plus(succ(0),succ(0)),succ(0))

Eval 0              - 0
Eval succ(0)        - succ(0)
Eval 0              - 0
Eval succ(0)        - succ(0)
Eval plus (succ(0), succ(0))
 Try (1)  - fails
 Try (2)  - succeeds, m=0, n=succ(0)
             results:    Eval succ(succ(0)) which gives succ(succ(0))

Eval 0           - 0
Eval succ(0)     - succ(0)
Eval plus(succ(succ(0)),succ(0))
 Try (1)  - fails
 Try (2)  - succeeds, m=succ(0), n=succ(0)
          - result: Eval succ(plus(succ(0), succ(0))
                 Eval 0 - 0
                 etc.
                 Eval plus(succ(0), succ(0))
                    .........
                 result: Eval succ(plus(0,succ(0)))
                         which gives succ(succ(0)))
               succ(succ(succ(0)))

We could write this more briefly, just noting which recursion equations are used, thus

plus(plus(succ(0),succ(0)),succ(0))           by (2)
  <= plus(succ(plus(0,succ(0))),succ(0))      by (1)
  <= plus(succ(succ(0)),succ(0))              by (2)
  <= succ(plus(succ(0),succ(0)))              by (2)
  <= succ(succ(plus(0,succ(0))))              by (1)
  <= succ(succ(succ(0)))

If expression m evaluates to expression n, we write m=n. Note that if m does not evaluate to n nothing can be concluded about equality or inequality of m and n.

Now let us try another definition

     times(0,n)          <=   0                   (3)
     times(succ(m),n)    <=   plus(times(m,n),n)  (4)
So
     times(succ(succ(0)), succ(succ(0)))
     <= plus(times(succ(0),succ(succ(0))),succ(succ(0)))
     <= etc.

It is convenient to write n' for succ(n). Here is another example

     equal(0,0)    <=  true           (5)
     equal(0,n')   <=  false          (6)
     equal(m',0)   <=  false          (7)
     equal(m',n')  <=  equal(m,n)     (8)

It is sometimes convenient to introduce conditions on equations, thus for example

     f(m,n)      <= 0            if equal(m,n)
     f(m,n)      <= plus(m,n)    if not(equal(m,n))

Exercises for Section 2

  1. Complete the evaluation of times(0'',0'') started above.
  2. Evaluate equal (0'',0').
  3. Write recursion equations for m to the power n, pow(m,n).
  4. Write recursion equations for m greater than n, gr(m,n).
  5. Write recursion equations for not, and, or.
  6. Write recursion equations for greatest common denominator for m and n, gcd(m,n), using a subsidiary function for difference, minus(m,n), only defined when m is greater than or equal to n.

3. Lists

Another inductively defined data structure is the list. We may define lists of integers using a constant, nil, and a function, pre, thus

So nil, pre(1,nil), pre(1,pre(2,nil)) are lists.

We can define functions on lists recursively, for example a function to make a list with a certain element on the end.

     post(n,nil)       <= pre(n,nil)          (1)
     post(n,pre(m,l))  <= pre(m,post(n,l))    (2)
so
     post(3,pre(1,pre(2,nil)))
        <= pre(1,post(3,pre(2,nil)))          by (2)
        <= pre(1,pre(2,post(3,nil)))          by (2)
        <= pre(1,pre(2,pre(3,nil))            by (1)

It is convenient to write n::l for pre(n,l), where this operator associates to the right, thus

     1::2::3::nil   means  pre(1,pre(2,pre(3,nil)))
Here is a function to double a list of numbers
     double(nil)    <= nil
     double(n::l)   <= times(2,n)::double(l)

so double (1::2::3::nil) = 2::4::6::nil

Here is a function to join two lists
     join(nil,l)  <= l
     join(n:k,l)  <= n::join(k,l)

so join(1::2::nil,3::4::nil) = 1::2::3::4::nil

Here is a function to reverse a list
     rev(nil)   <=  nil
     rev(n::l)  <=  post (n,rev(1))

so rev(1::2::3::nil) = 3::2::1::nil

Here is another way to reverse a list
     move(nil,l)   <=  l
     move(n::k,l)  <=  move(k,n::l)
so move(1::2::nil,3::4::nil) = 2::1::3::4::nil

Notice that for any list 1, move(k,l), move(l,nil) = rev(l), and more generally move(k,l) = join(rev(k),l). These are the sort of facts we should like to prove.

Here is a simple way of sorting a list of numbers

     insert(m,nil)  <= m::nil         sort(nil)  = nil
     insert(m,n::l) <= n::insert(m,l) if gr(m,n)  sort(m::l) = insert(m,sort(l))
     insert(m,n::l) <= m::n::l        if not(gr(m,n))

We notice that if l is in ascending order so is insert(m,l) and hence sort(l) is in ascending order.

Types

We have met three data types so far, numbers, truth values and lists of integers. It is helpful to specify the argument types and the result type for each function. For this we use a declaration of the form f: argl,...,argn -> result. We call the types nat, truthval and list. The constants and functions defined above have types as follows (alpha is a type variable)

nil                                -> list(alpha)
:: :     alpha,list(alpha)         -> list(alpha)
post:    alpha, list(alpha)        -> list(alpha)
double:  list(nat)                 -> list(nat)
join:    list(alpha), list(alpha)  -> list(alpha)
rev:     list(alpha)               -> list(alpha)
move:    list(alpha), list(alpha)  -> list(alpha)
insert:  nat,list(nat)             -> list(nat)
sort:    list(na)                  -> list(nat)

Two points in conclusion

Exercises for Section 3

Write programs for the following functions, using the notation above. Specify the types of any subsidiary functions which you define.

  1. Length of a list
    length: List(alpha) -> nat
    e.g. Length([1,3,5,1]) = 4
  2. Number of occurrences of an element in a list
    occurs: alpha,list(alpha) -> nat
    e.g. occurs(1,[1,3,5,1]) = 2
  3. Substitute an element for another element in a list
    subs: alpha,alpha,list(alpha) -> list(alpha)
    e.g. subs(6,1,[1,3,5,1]) = [6,3,5,1]
  4. Given two lists without repetition make a list of the elements common to both (intersection)
    intersec: list(alpha),list(alpha) -> list(alpha)
    e.g. intersec([1,2,9,6],[9,3,1,5])=[1,9]
  5. Find whether one list appears within another
    appears: list(alpha),list(alpha) -> truthval
    e.g. appears([2,9,6],[1,2,9,6,7,7]) = true
  6. Find the number of integers in a list of lists of integers.

4. Axioms above natural numbers and lists

We need some axioms about the natural numbers and about lists to enable us to prove facts about the functions which we have defined over them.

Natural number axioms

  1. CASES
    If n is a natural number then either n=0
    or n=succ(m) for some natural number m but not both
  2. UNIQUENESS
    If n and m are natural numbers then
    succ(n)=succ(m) implies n=m
  3. INDUCTION
    For any property P of natural numbers
    if P(0)                                      [Base]
    and for all m, P(m) implies P(succ(m))       [Step]
    then for all n, P(n)                         [Conclusion]

Considering lists over some arbitrary type T, we have

List axioms

  1. CASES
    If l is a T-list then either l=nil
    or l=t::k for some t in T and some T-list k but not both
    
  2. UNIQUENESS
    If l1 and l2 are both T-lists and
    t1 and t2 are both in T then
    t1::l1=t2::l2 implies t1=t2 and l1=l2.
    
  3. INDUCTION
    For any property P of T-lists
    if P(nil)                                    [Base]
    and for all t, l, P(k) implies P(t::k)       [Step]
    then for all l, P(l)                         [Conclusion]
    

5. Proofs about functions over natural numbers

We take m and n to be natural numbers throughout. Recall the definition of plus (which we now write as +)

     0+n          <= n
     succ(m)+n    <= succ(m+n)

Proposition 5.1. For all n, n+0=n

Proof. By induction on n

     Base  We show 0+0=0, thus
            0+0 = 0                  by def. of +
     Step  We assume m+0=m and show
            succ(m)+0 = succ(m), thus
            succ(m)+0 = succ(m+0)    by def. of +
                      = succ(m)      by induction hypothesis
§

Notes

  1. Using the definition 0+n evaluates in one step, but n+0 takes n steps to evaluate, so we need an inductive proof to reason about this arbitrarily long evaluation.
  2. The form of the proof: by induction on n
            Base  We show P(0), thus...
            Step  We assume P(m) and show P(succ(m)), thus ...
            (using P(m), the induction hypothesis)
         §
         In the above P(n) is For all n, n+0=n
    
  3. § means 'end of Proof'.

Proposition 5.2. For all m, n, m+succ(n)=succ(m+n)

Proof. By induction on m. Exercise.

Proposition 5.3. (Commutativity of +) For all m, n, m+n=n+m

Proof. By induction on m
     Base  We show 0+n=n+0, thus
            0+n = n                    by def. of +
                = n+0 by Prop. 1 (luckily we proved that first)
     Step  We assume m+n=n+m and show
            succ(m)+n = n+succ(m),  thus
            succ(m)+n = succ(m+n)      by def. of +
                      = succ(n+m)      by Induction Hypothesis
            n+succ(m) = succ(m+n)      by Prop. 2 (lucky again)
§

Now Recall the definition of times (*)

     0*n        <= 0
     succ(m)*n  <= (m*n)+n

Proposition 5.4. (Distributivity of *) For all m,i,j, m*(i+j)=(m*i)+(m*j)

Proof. By induction on m.

Try it. You will get stuck. What is the property of + which you need to complete the proof? Prove this property as a separate proposition.

Exercises for Section 5

  1. Complete proof of Proposition 5.2.
  2. Complete proof of Proposition 5.4.
  3. Prove commutativity and associativity of *.
  4. Complete and prove the following proposition i+m=j+m implies...

6. Proofs about functions over lists

We take l, k and h to be T-lists throughout and n, t to be elements f type T (e.g. natural numbers).

Recall the definition of join
   join(nil,l)  <= l
   join(s::k,l) <= s::join(k,l)

Proposition 6.1. (Associativity of join) For all lists l, k, and h, join(l,join(k,h))=join(join(l,k),h)

Proof. By induction on l
   Base  We show for all k,h,join(nil,join(k,h))=join(join(nil,k),h)
          thus
          join(nil,join(k,h))  =join(k,h)              by def.
          join(join(nil,k),h)) =join(k,h)              by def.
   Step  We assume
          for all k,h, join(l,join(k,h))=join(join(l,k),h)
          and show
          for all k,h, join(s::l,join(k,h))=join(join(s::l,k),h)
          thus
          join(s::l,join(k,h)  =s::join(l,join(k,h))   by def
                               =s::join(join(l,k),h)   by Ind. Hyp.
          join(join(s::l,k),h) =join(s::join(l,k),h)   by def.
                               =s::join(join(l,k),h)   by def
§

Proposition 6.2. For all lists of natural numbers l and k, double(join(k,l))=join(double(k),double(l))

Proof. Exercise.

Proposition 6.3. For all lists l,k rev(join(l,k))=join(rev(k),rev(l))

Proof. By induction on l, using two lemmas about join given below.

     Base  Show rev(join(nil,k))=join(rev(k),rev(nil))
        rev(join(nil,k))      = rev(k)                          def.
        join(rev(k),rev(nil)) = join(rev(k),nil)                def.
                              = rev(k)                          Lemma 6.1
     Step  Assume rev(join(l,k))=join(rev(k),rev(l)) for all k
        and show rev(join(s::l,k))=join(rev(k),rev(s::l)) for all s,k
        rev(join(s::l,k)) = rev(s::join(l,k))                   def.
                          = post(s,rev(join(l,k)))              def.
                          = post(s,join(rev(k),rev(l)))         Ind. Hyp.
        join(rev(k),rev(s::l)) = join(rev(k),post(s,rev(l)))    def.
                               = post(s,join(rev(k),rev(l)))    Lemma 6.2
§

Lemma 6.1. For all l, join(l,nil)= l

Proof. By induction on l. Exercise.

Lemma 6.2. For all s,k,l, join(k,post(s,l))=post(s,join(k,l))

Proof. By induction on k. Exercise.

Proposition 6.4. For all l, rev(rev(l))=1

Proof. By induction on l, using lemma 6.1 below.

     Base  rev(rev(nil))=rev(nil)=nil
     Step  Assume rev(rev(l))=l.
       Show rev(rev(s::l))=s::l for all s.
        rev(rev(s::l)) = rev(post(s,rev(l)))
        s::l           = s::rev(rev(l))       by Ind. Hyp.
                       = rev(post(s,rev(l)))  by lemma 6.3
§

Lemma 6.3. rev(post(s,l))=s::rev(l)

Proof. By induction on l. Exercise

7. Heuristic method for discovering induction proofs

This kind of proof gets rather routine with a little practice. Could it not be done machine? Boyer and Moore wrote an elegant and efficient program for carrying out such proofs (see their paper in Jnl. of ACM., Jan. 1975).

The method we used above may be outlined as:-

  1. choose a variable to do induction on.
  2. Set up base and step subproblems, and for each:-
  3. Reduce the proposition to be proved as far as possible by using function definitions
  4. (In the Step subproblem). Use the induction hypothesis
  5. If 4 is impossible or does not complete the proof, formulate a helpful lemma.
  6. Prove the lemma (subproblem) and use it to complete the main proof.

Now (2), (3) and (4) can all be done by rule in a mechanical manner. So can (6), given that it involves a recursive call on the whole proof discovery procedure to prove the lemma, which may itself generate sublemmas.

Ingenuity is required for steps (1) and (5), choosing the induction variable and formulating a lemma.

Assume that we are trying to prove a proposition which is an equation. This keeps the explanation simpler.

Choosing the induction variable

The process of using the function definitions to reduce an expression is a symbolic version of the ordinary evaluation method. It works on expressions with variables instead of on data expressions. Unlike ordinary evaluation, symbolic evaluation can get stuck: this is when we try to evaluate f(E) and E does not match the left hand side of any equation for f, e.g. when E is a variable. This gives us a clue to which variable should be chosen to do induction on. Consider the defining equations of a function such as join

     join(nil,l)     <= l
     join(s::k,l)    <= s::join(k,l)

Suppose we want to prove

     join(join(m1,m2),m3) = join(m1,join(m2,m3))

Our first idea might be to try to simplify these expressions using the definitions. Looking at the inner expression on the left we compare join(m1,m2) with join(nil,l) and with join(s::k,l). We find that the first argument m1 is not of the form nil or s::k. So we can't simplify.

However if we take m1 as induction variable we can simplify because we have to prove

     join(join(nil,m2),m3) = ...          (Base case)
     join(join(s::m1,m2)),m3) = ...       (Induction step)
        assuming join(join(m1,m2),m3) = ...
These both match the definition nicely.

So the following heuristic (due to Boyer and Moore) can be used to choose the induction variable

For example, the only variable in such a position on the left of the theorem above is m1, and the variables in such positions on the right are m1 and m2. So we choose m1.

We call an argument position for a function f an induction position if in some defining equation for f the left hand side has a term using constructors in that position.

So defining + and * by
     0+n    <= n                 0*n    <= 0
     m'+n   <= (m+n)'            m'*n   <= m*n+n

for each of them only the first position is an induction position. To prove l*(m+n) = (l*m)+(l*n) we note that l and m are in induction positions on the left, only l on the right.

So we choose l. To prove m+n = n+m we have m in induction position on the left , n on the right. The heuristic gives no preference and we choose either m or n.

Formulating a lemma

Look back at the proofs of Propositions 6.3 and 6.4. Where did we get stuck and have to introduce a lemma?

The expressions which we would have liked to be equal were

        RHS                               LHS

(a)     join(rev(k),nil)                  =?rev(k)
(b)     post (s,join(rev(k),rev(l)))      =?join(rev(k),post(s,rev(l)))
(c)     rev(post(s,rev(l)))               =?s::rev(rev(l))

The lemmas we invented were

(a)     join(l.nil)        =  l
(b)     post(s,join(k,l))  =  join(k,post(s,l))
(c)     rev(post(s,l))     =  s::rev(l)

What is the trick? These are just the expressions we had difficulty with but one or more subexpressions (rev(l) or rev(k) or both) have been replaced by variables. We generalise the equation we want to prove by replacing one or more expressions in it by variables ( a heuristic due to Boyer-Moore). For example

  join(l,nil) = l                         (for all l)

is more general than

  join(rev(k),nil) = rev(k)               (for all k)

because the latter can be deduced from the former by taking l to be rev(k).

The point of making the generalisation is to prove the new lemma by induction, indeed by induction on the new variable introduced. So it is best to introduce this variable in an induction position.

The induction positions for rev, join and post are l, 1, 2 respectively, so in the above examples the terms in induction positions are

        LEFT                              RIGHT

(a)     rev(k)
(b)     rev(k),join(rev(k),rev(l))        rev(k),rev(l)
(c)     rev(l),post(s,rev(l))             rev(l)

Where possible we choose a term in induction position on each side, thus

(a)     rev(k)
(b)     rev(k)
(c)     rev(l)

There is another kind of generalisation (due to Aubin) which is useful on occasion, replacing a variable which occurs more than once in an expression by separate variables. For example to prove

  i+(i+k) = (i+i)+k

The variable in induction position on each side is i. Inducing on it

Base  0+(0+k) = (0+0)+k.                 proof  Immediate.
Step  Assume i+(i+k) = (i+i)+k and show i'+(i'+k) = (i'+i')+k

  That is show (i+(i'+k))' = (i+i')'+k.
  We can't use the induction hypothesis.
  But the more general theorem
    i+(j+k) = (i+j)+k is easy to prove.

A more substantial example

Here is an example of a proof which requires several lemmas. When we do an inductive proof we may get stuck having simplified the left and right hand expressions, but not succeeded in making them equal. The task of proving the simplified expressions equal is a subgoal. To achieve the subgoal we make a lemma by generalisation, either by replacing a term by a variable or by separating a repeated variable into two different ones. We just sketch the proof showing subgoal and lemmas.

Proposition. (Distributivity of *) For all natural numbers l,m,n l*(m+n) = (l*m)+(l*n)

Proof. By induction on l.

  Base  Put l=0.     Immediate by definition.
  Step  suc(l)*(m+n) = (m+n)+(l*m+l*n)
        using defn. and induction hypothesis
     (suc(l)*m)+(suc(l)*n) = (m+l*m)+(n+l*n)
        using defn.
      Subgoal        (m+n)+(l*m+l*n) = (m+l*m)+(n+l*n)
        Generalising by separating the variable m we invent
      Lemma 7.1  (m+n)+(l*i+l*n) = (m+l*i) + (m+l*n)
      Remark  A more general lemma would be
       (m+n)+(j+k) = (m+j)+(m+k)
       or indeed we could use associativity and commutativity of +
       as lemmas.  But Lemma 7.1 suffices.        
§

Lemma 7.1

Proof. by induction on m.

  Base  Gives Subgoal n+(l*i+l*n) = (l*i)+(n+l*n)
     Generalising this by separating the variable n we obtain

  Lemma 7.2 n+(l*i+l*k) = (l*i)+(n+l*k)
  Step  Straightforward                  
§

Lemma 7.2.

Proof. By induction on n.

  Base  immediate. 

Step Using definitions and induction hypothesis we get Subgoal suc((l*i)+(n+l*k)) = (l*i)+suc(n+l*k) Now we notice the term l*i appearing in an induction position on both sides and generalise it to j. (The alternative of proof by induction on n fails.) Lemma 7.3 suc(j+(n+l*k)) = j+suc(n+l*k) §

Lemma 2.3. Proof by induction on j: straightforward.

Exercises for Section 7

  1. Define ** by
               int ** (list(int)) -> list(int)
               i ** nil         <= nil
               i ** (j::l)      <= (i*j)::(i**l)
    
    What is the induction position for **? To show
     
           i ** (join(l,m)) = join(i**l,i**m) 
    what variable would you induce on, according to the heuristic? Complete the proof.

  2. Fill in the details of the proofs of distributivity of *, doing at least one lemma in full.

    Show how the choice of induction variable and choice of generalisation for each subgoal could have been made using the Boyer-Moore-Aubin heuristic (by identifying the induction positions on left and right of the theorem or subgoal).

  3. Define member by
           member(int,list(int)) -> list(int)
           member(i,nil)               <= false
           member(i,j::l)              <= true if i=j
                                       <= member(i,l) if not
    
    Show, making heuristic choice of an induction variable, that

    member(i,join(l,m)) = member(i,l) or member(i,m) where

           true or p  <= true
           false or p <= p
    
    (Hint. Do a case analysis, e.g. Case 1 i=j,... Case 2 i < > j,...)
  4. Define length of a list, giving the number of elements in it and show, by heuristically formulating a lemma, that
           length(rev(l)) = length(l)