In general, I really liked doing complete induction on recursive correctness proofs because it really exercised proof by cases (which I enjoy) and complete induction (which is cool because it interweaves into this subject of program correctness, and you get the opportunity to practice being careful in translating the induction hypothesis to the recursive calls).
Iterative correctness is certainly tougher... In general, I find that to prove an iterative proof, I need to:
1) Find an appropriate LI (loop invariant) which helps prove the postconditions from the preconditions,
2) Prove that precons (preconditions) imply term (termination) implying postcons (postconditions) using the incoming LI,
3) Prove term by finding a decreasing sequence in the natural numbers to show that the loop does terminate.
Proof of recBinSearch(x, A, b, e), which returns index p such that A[p - 1] < x <= A[p], except for boundaries:
Precons: 1) x and elements of A comparable,
2) e and b valid indices, b <= e,
3) A[b...e] sorted non-decreasing.
Postcons: 1) b <= p <= e + 1,
2) b < p implies A[p - 1] < x,
3) p <= e implies x <= A[p].
My major concern here was with postcons 2 and 3. I thought that what was returned was p such that A[p] = x, when in actuality it is such that A[p - 1] < x <= A[p]. This makes postcons 2 and 3 important because the hidden implications of the latter (A[p - 1] < x <= A[p], except for boundaries). Firstly, b < p implying A[p - 1] < x means that we return the index p of the "first occurrence" of x in A[b...e], since A is sorted in non-decreasing order (even if p = e + 1 in line 5). Secondly, p <= e implying x <= A[p] means that p != e + 1 (since by postcon 1, p <= e + 1, p can't be any larger than that), so line 2's if statement is true, so x <= A[b = p]. The important thing to take out of this is that it is possible for A[p - 1] < x < A[p] (so A[p] != x, so p is not returned such that A[p] = x). An example of this occurring is when x is "beyond the boundaries" (hence the "except for boundaries" part), so x is less than A[b = p] like with recBinSearch(0, [0, 0, 1, 1, 4, 6, 8], 2, 3) or when x is in an index beyond p = e + 1, like with recBinSearch(100, [0, 1, 2, 3, 5, 6, 8, 13, 56, 67, 100, 130], 0, 8).
Proof of MergeSort(A, b, e): with A'[b...e] as the same elements of A[b...e], but sorted in non-dec order and all other elements of A' from A unchanged:
- Interesting that it needs to be unchanged, to ensure that recursive calls do not have lists that mess up each other's elements.
- Proving Merge:
--> Interesting that we needed to create a strictly decreasing sequence (to find the last iteration using WOP), it's very clever.
--> About the loop invariant for merge, being e + 1 - i, I need to find out where the + 1 comes from (length of the list making index fall out perhaps?).
Proof of power(x, y), returning z = x^y, with y a natural number and x a real number:
- Way the proof works seems similar to mult'n proof in textbook.
- In proving termination, i.e. {y - m_i} is a decreasing sequence in the natural numbers, I was wondering why we didn't need to use induction. Instead, we showed that having an (i + 1)th iteration of the loop implies y - m_i < y - m_(i + 1).
"Correctness by Design":
- This was I thought of as a very powerful technique. First, it is possible to rewrite recursive functions as iterative ones, and vice-versa - but here, careful iterative and recursive correctness techniques are used in combination to understand how to design the actual function "correctly" (so we can prove correctness afterwards).
- I liked how we could extrapolate how our function would work by the drawing out of the lists of A and how it is before, during, and after sorting. It seems a crucial technique for finding loop invariants.
- I really wish this could be covered in detail again, it kind of makes me nervous if the short coverage of this topic is used as a cover for very complex questions on the exam. But it also gives room for more creative, interesting questions (#0).
#0: It excites me - now if only it wasn't for my horrid exam schedule...
----------------------------------------------------------------------------------------------------------------------------------
Final words on complexity examples:
- Discussed the closest points pair problem with Danny, it made much more sense knowing:
1) The computer sees the set of points P (as) = [(x0, y0), (x1, y1), ...], but the actual values held by the tuples carry no meaning in terms of sortedness. That is why we need to create two sorted lists immediately after: Px = {p in P | sorted by x} and Py = {p in P | sorted by y}, which is passed onto the recursive function. The sorting will each take O(nlogn) when doing a mergesort of P - the end result for the entire algorithm that we expect is still O(nlogn), so we don't care if part of the algorithm already does O(nlogn)
2) The sorted lists are used to walk through (O(n) to walk through each list) first in one direction, say the x direction, in order to see if the points are close that way, then we do recursive calls as the "map" of points sorted by x is split into left and right parts. On the way "up"/ to "merge" to find a minimum between the set of points on the left and right, we consider the smallest distance delta which is the minimum of the minimums found on the left and right.
3) We can use delta to examine the points closest to the splitting line, and we check if any distance in that neighbourhood is less than delta (since the distance that is across the line, between points, has not yet been examined). We do this by using the second direction of the sorted lists, say the y direction sorted list. For every two consecutive points in the list (imagine yourself as the computer, moving through the list of tuples sorted by y) whose distance in the y direction is less than delta, we can check if the euclidean distance is less than delta, and this will determine if there is a closer delta than the one that is the distance between two points isolated to one side of the splitting line.
Program correctness:
- Recursive: Need to practice writing proofs/counterexamples to whether recBinSearch(x, A, b, e) is correct when m = ceiling((e + b) / 2) or when x < A[m], and finally to edit the code to find the last of duplicate elements probably going over than during Exam time since it takes some extra time.
- Iterative: Need to practice with Merge correctness (pg 67 of course notes), but I'll probably do that during the Exam practice time, since the proof seems large-scale.
- In both cases, I'll have to hold off till exam time to do intense practice.
- Need practice for correctness by design.
No comments:
Post a Comment