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

• (i) 0 is a number
• (ii) succ(n) is a number if n is a number.

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

• (i) 0 evaluates to 0
• (ii) succ(E) evaluates to succ(E)
• (iii) plus (E1,E2) is evaluates by matching E1 and E2 against the left hand sides of equations (1) and (2) above.

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

• list = nil or pre(nat,list)
• (i) nil is a list
• (ii) pre(n,1) is a list if n is a number and 1 is a list.
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

• (i) It is often convenient to use a bracket notation for lists, even though this disguises the function/ argument structure. Thus 1,2,3,4 is short for 1::2::3::4::nil.
• (ii) We can make lists of other things besides numbers, e.g. lists of lists of numbers like [[1,2,3],[4,5,6],[7,8,9,10]]

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

• (i) Look at the definitions to see which positions on the left contain a term rather than a variable.
• (ii) Look at the expressions in the theorem and see which variables appear in such positions.
• (iii) Choose one of these variables, preferably one occurring in such a position on each side.

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)  `