CS代考计算机代写 Haskell ocaml scheme 1 2 3 4
1 2 3 4
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.
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
) 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.
1 2 3 4 5
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.
+ nk.
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