This document can be found on HTTP://WWW.CSI.UOttawa.CA/~luigi/csi5109/recursive.html
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.
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))
Another inductively defined data structure is the list. We may define lists of integers using a constant, nil, and a function, pre, thus
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.
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
Write programs for the following functions, using the notation above. Specify the types of any subsidiary functions which you define.
length: List(alpha) -> nat
occurs: alpha,list(alpha) -> nat
subs: alpha,alpha,list(alpha) -> list(alpha)
intersec: list(alpha),list(alpha) -> list(alpha)
appears: list(alpha),list(alpha) -> truthvalWe 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.
If n is a natural number then either n=0 or n=succ(m) for some natural number m but not both
If n and m are natural numbers then succ(n)=succ(m) implies n=m
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
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
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.
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]
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
§
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
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.
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 joinjoin(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
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:-
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.
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.
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.
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.
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.
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).
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,...)
length(rev(l)) = length(l)