Chapter 3 Induction
“On theories such as these we cannot rely. Proof we need. Proof!”
Yoda, Jedi Master
In this chapter, we will briefly discuss how to prove properties about ML programs using induction. Proofs by induction are ubiquitous in the theory of programming languages, as in most of computer science. Many of these proofs are based on one of the following principles: mathematical induction and structural induction. In this chapter we will discuss these most common induction principles.
Copyright By PowCoder代写 加微信 powcoder
3.1 Mathematical induction
Mathematical induction is the simplest form of induction. When we try to prove a property for every natural number n, we first show the property holds for 0 (in- duction basis). Then we assume the property holds for n and establish it for n + 1 (induction step). Basis and step together ensure that the property holds for all natu- ral numbers.
There are small variations of this scheme which can be easily justified. For exam- ple, we may start by proving the property holds for 1, if we want to prove a property for all positive integers. There may also be two base cases, one for 0 and one for 1.
As an example, let us consider the following program power.
(* Invariant: power:int >=0 *)
let rec power(n, k)=
if k=0 then 1 else n * power(n, k-1)
How can we prove that this program indeed computes nk? – To clearly distinguish between the natural number n in our on-paper formulation and its representation
33 c B. Pientka – Fall 2020
Chapter 3: Induction 3.1 Mathematical induction
and use in a program, we will write n to denote the latter. Moreover, we will use the following notation
e + v expression e evaluates in multiple steps to the value v.
e ) e0 expression e evaluates in one steps to expression e0.
e )⇤ e0 expression e evaluates in multiple steps to expression e0.
In this example, we want to prove that power(n, k) evaluates in multiple steps to the value nk.
Theorem 1. power(n, k) + nk for all k 0 Proof. By induction on k.
Base Case k = 0
power(n, 0)
if 0 = 0 then 1 else n *power(n, 0-1) if true then 1 else n *power(n,0-1) 1 = 1 = n0
by program by evaluation rules for equality by evaluation rules for if-expressions
Step Case Assume that power(n,k) + nk. We have to show that power(n, k + 1) + nk+1 .
power(n, k + 1)
) if k+1 =0then1else n*power(n,(k+1)-1) byprogram ) if false then 1 else n * power(n, (k + 1) – 1) by evaluation rules for equality
) n * power(n, (k + 1) – 1) ) n * power(n, k)
) n ⇤ nk = nk+1
by evaluation rules for if-expressions by evaluation rules for – by induction hypothesis by evaluation rules for ⇤
This proof emphasizes each step in the evaluation of the program1. Often, we may not want to go through each single step in that much detail. However, it il- lustrates that when reasoning about programs, we must know about the underlying
1Note, in class we assumed the property holds for k – 1 and showed the property for k. Both are fine
34 c B. Pientka – Fall 2020
Chapter 3: Induction 3.2 Complete induction
operational semantics of the programming language we are using, i.e. how will a given program be executed.
3.2 Complete induction
The principle of complete induction formalizes a frequent pattern of reasoning. To prove a property by complete induction we first need to establish the induction basis for n = 0. Then we prove the induction step for n 0 by assuming the property for all n0 < n and establishing it for n. One can think of it like mathematical induction, except that we are allowed to appeal to the induction hypothesis for any n0 < n and not just the immediate predecessor.
These two principles should be familiar to you and are the basis for proving some fundamental properties about programs. As an example, we define a program for power which is more efficient and defined via pattern matching.
Lemma 1. For all n, nk*nk + n2k. Theorem 2. power(n, k) + nk for k 0.
Proof. By complete induction on k.
Base Case k = 0 power(n, 0)
) 1 by program
Step Case k > 0
Assume that power(n, k0) + nk0 for any k0 < k. We have to show that power(n, k)
let rec power (n,k) = match k with | 0 -> 1
| _ -> if even(k) then
let r = power(n, k / 2) in r * r else n * power (n, k-1)
To prove that this program works correctly, we rely on the following properties which we state as lemmas without proofs.
35 c B. Pientka – Fall 2020
Chapter 3: Induction 3.3 Structural induction
power(n, k)
) if even (k) then (letr = power(n,k/ 2) in r * r)
else n*power(n,k-1)
Now we will distinguish subcase, whether k is even or odd.
Sub-Case1k=2k0 forsomek0
if x = y then Node(e, l, r)
(if x < y then Node((y,d’), insert e l, r)
Node((y,d’), l, insert e r))
let rec lookup x t = match t with | Empty -> None
| Node ((y,d), l, r) ->
if x = y then Some(d)
(if x < y then lookup x l
else lookup x r)
Let’s try to prove that when we have inserted an element (x,d) into a binary search tree t, and then look up the data corresponding to the key x, we will get back the date d. In the proof below we will write ) ⇤ when we skip over some intermediate steps.
Theorem 3. If t is a binary search tree, then lookup x (insert (x,d) t) + Some(d) Proof. By structural induction on t.
BaseCase t=Empty
lookup x (insert (x,d) Empty)
) lookupx(Node((x,d),Empty,Empty)) )⇤ Some(d)
StepCase t=Node((y,d’),l,r)
byprograminsert by program lookup
We can assume the property holds for the sub-trees l and r.
37 c B. Pientka – Fall 2020
Chapter 3: Induction
1. lookup x (insert (x,d) l) + Some(d) 2. lookup x (insert (x,d) r) + Some(d)
Sub-case: x = y
lookup x (insert (x,d) (Node((y,d’), l, r)))
)⇤ lookup x (Node((x,d), l, r)) )⇤ Some(d)
Sub-case: x < y
lookup x (insert (x,d) (Node((y,d’), l, r)))
)⇤ lookup x (Node((y,d’), insert (x,d) l, r))
)⇤ lookup x (insert (x,d) l)
) Some(d) Sub-case: y < x
3.4 Generalizing the statement
by program insert by program lookup
by program insert by program lookup by i.h.
by program insert by program lookup by i.h.
lookup x (insert (x,d) (Node((y,d’), l, r))) lookup x (Node((y,d’), l, insert (x,d) r)) lookup x (insert (x,d) r)
Generalizing the statement
From the examples, it may seem that induction is always straightforward. Often this is indeed the case. Sometimes however we will encounter functions whose cor- rectness property is more difficult to prove. This is often because we need to prove something more general than the final result we are aiming for. This is also referred to as generalizing the induction hypothesis. There is no general recipe for generalizing the induction hypothesis, but one common case is the following.
Consider the following two programs for reversing a list. The first one is the naive version, while the second one is the tail-recursive version.
We would like to prove that both programs yield the same result. Essentially we would like to say rev l returns the same result as calling rev’ l [].
38 c B. Pientka – Fall 2020
let rec rev l = match l with |[] ->[]
| x::l -> (rev l) @ [x]
let rec rev’ l acc = match l with | [] -> acc
| h::t -> rev’ t (h::acc)
Chapter 3: Induction 3.4 Generalizing the statement
revl +l’iffrev’l[] +l’
We will simplify this statement a little bit, and try to prove
rev l = rev’ l []
The problem arises in the step-case, when we attempt to prove
rev (x::t) = rev’ (x::t) []
On the left, the program rev’ evaluates as follows: rev’ (x::t) []
) rev’ t (x::[])
) rev’ t [x]
But now we are stuck. We cannot apply the induction hypothesis, because the
statement we attempt to prove requires that the second argument to rev’ is the empty list! The solution is to generalize the statement in such a way that the desired result follows easily.
The following theorem generalizes the problem appropriately. Theorem 4. For any list l, = rev’ l acc
Proof. Induction on l. BaseCase l=[]
( rev’[]acc
StepCase l=x::t
Assuming, for any acc’, = rev’ t acc’, we must prove = rev’ (x::t) acc’ .
= rev’ (t) (x::acc) ( rev’(x::t)acc
byprogramrev byprogram@ byprogramrev’
byprogramrev byassociativityof@ byunrollingthedefinitionof@ by i.h. byprogram
c B. Pientka – Fall 2020
Chapter 3: Induction 3.5 Conclusion
We want to emphasize that you should always state lemmas (i.e. properties) you are relying on. In the previous example, we need to know properties of append for example.
3.5 Conclusion
We presented several important induction principles and examples of induction proofs. While in practice, we will rarely verify programs completely, we may want to prove certain properties about them in practice, for example we may want to prove that some confidential data is not leaked, or only some designated principals will have access to a given resource. These properties will typically follow the same induction principles we have seen in these notes.
There is a wide spectrum of properties we would like to enforce about programs. Types, as we encounter them in a language such as OCaml, SML, or Haskell enforce fairly simple properties. For example, the type of the lookup function is ’a * (’a * ’b)tree -> ’b option. While this gives us a partial correctness guarantee, it does for example not ensure that the tree passed is a binary search tree. On the other hand, type systems are great because they enforce a property statically. When you change your program, the type-checker will verify if it still observes this type property. If it doesn’t the type checker will give precise error messages, so the programmer can fix the problem. Inductive proofs can typically enforce stronger properties about pro- grams than types. In fact, we can prove full correctness. However, inductive proofs have to be redone every single time your program changes. Doing them by hand is time-consuming. What is it we actually need to prove? How do we know when to generalize an induction hypothesis? What happens if a proof fails? Can we give meaningful error messages in this case? A key question is therefore how we can make type systems stronger so they can check stronger properties statically, while re- taining all their good properties. and discovered that there is an isormophic relationship between propositions and types; moreovoer, the proof that a proposition is valid corresponds to a program. This relationship is gener- ally known as “propositions-as-types” and “proofs-as-programs”. Fundamentally the Curry-Howard correspondance, allows us to write programs with very rich types (i.e. types which correspond to first-order formulas and encode the full specification of a given function); if the program type checks, it is correct by construction. But that’s a question for a different course :–).
40 c B. Pientka – Fall 2020
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com