BEGIN 16_11_15_InvariantExamples.lhs =========================================== BEGIN EXAMPLE 1 Here is the pseudocode of a function FUN, which we want to execute with two non-negative integers x and y as input arguments: FUN (x, y): p := 1 q := 0 while p < x: p := p * y q := q + 1 return q QUESTION: What value does FUN (x,y) return? To get a sense of what FUN does, we try it on a few arguments (with paper and pencil): x y FUN (x,y) -------------------------------------------------------- 0 any number 0 1 any number 0 x >= 2 y <= 1 no output (loops forever) 2 2 1 3 2 2 4 2 2 5 2 3 6 2 3 7 2 3 8 2 3 9 2 4 10 2 4 ... ... ... 2 3 1 3 3 1 4 3 2 5 3 2 ... ... ... 2 4 1 3 4 1 4 4 1 5 4 2 ... ... ... It is getting difficult (and boring!) to correctly guess what is the function FUN. So we may try instead to implement it in Haskell. However, FUN (x,y) is written imperatively with a WHILE-loop. But this is not a problem, because every WHILE-loop (and every REPEAT-loop, FOR-loop, etc.) can be translated into a RECURSIVE definition -- in fact, into a TAIL-RECURSIVE definition. Here is one way of doing this: > fun :: Int -> Int -> Int > fun x y = help x y 1 0 > where > help x y p q = > if p >= x > then q > else help x y (p * y) (q + 1) It is still difficult to guess what FUN is, although we may run the Haskell program to confirm the values we obtained above with paper and pencil. However, if we define an INVARIANT property of the WHILE-loop (in the pseudocode), we will get a better indication of what FUN computes. Let's try to define an INVARIANT about p and q, because these are the variables that are changing with every iteration of the WHILE-loop. The variables x and y do not change in this example. Before the loop, we have p = 1 and q = 0. After the first iteration, we have p = y and q = 1. After the second iteration, we have p = y^2 and q = 2. Now we can guess a general INVARIANT, namely: (1) p = y^q or also (because an INVARIANT is not uniquely defined): (2) (p = y^q and p < x) or also: (3) (p = y^q and p < x) and (if x and p are natural numbers, then so are p and q) The invariants in (1), (2), and (3), are only "guesses". We need to prove that they are indeed invariants. How we do this? Consider (2) only, which is good enough to reach our conclusion of what the function FUN is. We prove by INDUCTION on the number of iterations of the WHILE-loop that (p = y^q and p < x) is indeed an INVARIANT property. FACT: Proving an invariant correct ALWAYS involves some kind of induction, because an INVARIANT is none other than an INDUCTION HYPOTHESIS. So, what is the value of p and q when execution of the WHILE-loop stops? For that we need to answer: How many times is the WHILE-loop executed and this is given by the fact that we always have "p < x" -- which is part of the INVARIANT in (2) and (3). We conclude that FUN (x,y) returns the integer q such that: q is the largest integer such y^(q-1) < x END EXAMPLE 1 =============================================== BEGIN EXAMPLE 2 The following is the pseudocode of a function FOO, written in imperative style: FOO (x): y := x; z := 0; while y > 0 { y-- ; z++ ; } return z; The variables y and z are the only variables that change with every iteration of the WHILE-loop. EXERCISE: Prove by induction on the number of iterations that: y + z = x is an INVARIANT of the WHILE-loop. Together with the fact that on the last iteration y becomes 0, conclude that this invariant implies that x = z when the WHILE-loop terminates. EXERCISE: Write a Haskell implementation in tail-recursive form of the pseudocode of the function FOO (use the function FUN in Example 1 above to guide you). END EXAMPLE 2 =============================================== BEGIN EXAMPLE 3 Consider the following pseudocode in imperative style: BAR (x): y := 0; for ( i = 0; i <= x; i++ ) { y += 2^i ; } return y; EXERCISE: What is the value of y after the loop terminates? Hint 1: Try to find an INVARIANT of the FOR-loop that holds at the start of every loop iteration. Hint 2: Prove by induction that, at the end of the i-th iteration of the FOR-loop, it holds that y = 2^i -1. Hint 3: Conclude that when execution terminates, we have y = 2^(x+1) - 1. EXERCISE: Write a Haskell implementation in tail-recursive form of the pseudocode of the function BAR (use the function FUN in Example 1 above to guide you). END EXAMPLE 3 =============================================== BEGIN EXAMPLE 4 Consider the following pseudocode in imperative style: Binary_Search (A, target): lo := 0; hi := len (A) - 1; while lo <= hi : mid := (lo + hi) / 2; if A[mid] == target : return mid elif A[mid] < target : lo := mid + 1 else: hi := mid - 1 EXERCISE: Assuming that 'target' is actually an element in the array A, prove by induction on the number of iterations that A[lo] <= target <= A[hi] is an INVARIANT of the WHILE-loop. Conclude that the program is correct, i.e., that it correctly returns the index of 'target' in the array A. EXERCISE: How will you adjust the invariant and its proof if 'target' is not in the array A? EXERCISE: Write a Haskell implementation in tail-recursive form of the pseudocode of the function Binary_Search (use the function FUN in Example 1 above to guide you). END EXAMPLE 4 =============================================== BEGIN EXAMPLE 5 Consider the following pseudocode of the GCD function: GCD_Euclid (a, b): while a ≠ b if a > b a := a − b; else b := b − a; return a; (This is Euclid's form of the GCD as written some 2,300 years ago.) A different version of the GCD, using integer-division (i.e. with 'mod') instead of subtraction, is the following pseudocode: GCD_Modern (a, b): while b ≠ 0 t := b; b := a mod b; a := t; return a; EXERCISE: Define an appropriate INVARIANT of the WHILE-loop in GCD_Euclid (Hint: Search the Web) and prove that it is indeed an invariant by induction on the number of iterations. EXERCISE: Define an appropriate INVARIANT of the WHILE-loop in GCD_Modern (Hint: Search the Web) and prove that it is indeed an invariant by induction on the number of iterations. END EXAMPLE 5 =============================================== END 16_11_15_InvariantExample.lhs