And so, after 10 fun filled sLOG entries, this adventure in computational theory has come to an end.
I won't lie and say I loved the course. There was nothing wrong with it, it just never really was the most interesting material to me (although I do love me some regular expressions). But it was definitely educational. I do feel I got a lot out of it, even if a lot of what I got out of it was years off my life from the stress of Assignments 2 and 3.
At the end of the day, I learned a lot about proofs and am much more comfortable with them than I was at the beginning. It's hard to believe there was a time when I thought CSC165 was hard. It seems like kindergarden compared to this course, but I guess that's the point. It shows that I learned a lot.
And like I said, it wasn't all painful for me. I really did like DFSAs, NFSAs and regular expressions. They are rather intuitive to me, and are of a subject I find a lot more interesting.
So now it's just study and get ready for the final exam. I honestly feel pretty good about it, despite my sometimes poor understanding of this course. I always somehow come through in the end with enough knowledge to not only pass, but actually get a decent mark so I'm not going to stress too hard. More than ever I feel confident with the material too, since I started focusing more on the course and studying it.
Anyway, good luck to everyone for the exam. And thanks to the professor and the TAs for having taught it well. As much as I may have been lost at times, it was never for lack of organization or teaching skills.
Time to wrap it up. Much like this adventure, this post also has to end. Carter signing off.
Tuesday, 4 December 2012
Assignment 3: The Process
Because I like cutting things close, this entry of the sLOG, the most crucial one, will here be posted on the last day before the due date, 22 minutes before midnight. I decided while writing Assignment 3, that I would keep notes on my process, and type them up here once the deadline passed. I've only included questions 2, 3 and 4 here however, since I never actually took notes on my process for question 1 due to time pressures.
Question 2
Prove that the following terminates, given the precondition x is an element of the natural numbers:
y = x * x
while not y == 0 :
x = x - 1
y = y - 2 * x - 1
Hint: Trace through the code for a few small values of x, then derive (and prove) a loop invariant that helps prove termination.
The very first thing I did to solve this problem was do exactly what the hint suggested, something I always start with. Tracing code for a few, usually small, values. This is how I always prove things to myself. It's no secret to anyone who reads this sLOG that I'm not the most thrilled with structured proofs. I prefer to justify things to myself with extrapolation of patterns. Kind of like unit testing while programming. Anyway, after having traced through the loop step by step for x=0 through x=5, I had justified to myself that yes, it does indeed terminate. Furthermore, since I had been writing everything down in a list, it was very easy to see that the value of y was always equal to x^2. Even though I was very, very sure, from these tests, as well as just looking at the loop and it's simple nature, I coded the loop up in Python, and ran it with print statements and high values of x. The pattern was always true.
And so, like that I had both proved (to myself) that the loop invariant was x' = x-1, y' = (x')^2 (where x' is x after an iteration, y' is y after an iteration), and that the loop would terminate. Now all that was left was to actually prove it.
The loop invariant proof was actually a lot simpler than I was expecting. By just subbing in the values defined in the loop invariant into the two lines of code inside the loop, I was able to rather easily show that assuming the loop invariant held on the ith iteration, and that there was an (i+1)th iteration, the invariant held. I will say though that, despite the ease, it felt really nice to see it all work out in the end, probably because I didn't at any point get frustrated with this question.
From there, it was trivial to prove termination. The value of x was decreasing by one each time, and since y was x^2, when x was 0, y was 0. The loop would terminate when y was 0. So neither x, nor y, could ever be a value less than 0. Therefore, it was a decreasing finite series, and termination could be proved.
And just like that, it was done. This was the first question I did, since it seemed the easiest. After having done them all, I think I was right in that assumption.
Question 3
Design a DFSA that accepts the language of binary strings over {0, 1} that have a multiple of 4 1s. Devise, and prove a state invariant, and explain how it shows that your DFSA accepts this language.
The natural first thing to do here was draw out the DFSA diagram. I rather thought this was one of the simpler DFSAs we've looked at in this course, but I wasn't by any means complaining. Below is the DFSA I designed; drawn horribly in MS Paint. Bathe in it's glory.
From there it was easy to create a state invariant, although I confess, I did have to refer to the course notes to know what that was. Once I knew, I had seen it before, and quickly drew one up. I'd write it out here, but its remarkably difficult to express simply with the text options available on Blogger. So I'll say that it follows from the above diagram. If the number of 1s can be expressed as 4k, where k is a natural number, then it is in the q0 state, 4k+1 in the q1 state, and so forth.
I felt this was something that was quite obvious, but proving it was a lot less so. I struggled quite a bit with this proof despite it being outlined right in the course notes. I was literally staring at the proper form, but didn't understand it. I got the concept. I knew what it was showing - that any given string can be expressed as a string with one less character, and then either a 1 or a 0. For the substring, it can be assumed that the state invariant holds true using complete induction. Then that fact can be used to prove for the two cases (the next character is 1 and the next character is 0) that the state invariant still holds.
I just didn't understand the structure that was being used. I felt the proof shown wasn't very clear about one of the steps. I'd love to detail which one, but honestly, it's hard to express using the text options here, and describing it would just make my lack of terminological knowledge apparent. Suffice it to say that it was an intermediate step, the one in which the assumption regarding the substring led to the conclusion about the string. After probably two hours of looking at it, I finally figured it out. I was looking at the problem all wrong. It was in fact, quite clear. I had just been in the wrong mindset. I was expecting it to follow in a way that it did not follow in. I realize this all sounds cryptic, but I don't know how else to say it.
Once I realized what I was doing, it was simple from there to write it out. Though it took a remarkably long time to type up in Microsoft Word. Using equation tools gives you some nice looking work, but man does it take forever.
Question 4
Design an iterative binary search algorithm that is correct with respect to the following precondition/postcondition pair:
Precondition: A has elements that are comparable with x, |A| = n > 0, and A
is sorted in non-decreasing order.
Postcondition: binSearch(x, A) terminates and returns an index p that satisfies:
A[0 ... p] x < A[p + 1 ...n - 1]
-1 <= p <= n - 1
Prove that if the precondition is satisfied, then your algorithm terminates and satisfi es the postcondition.
Hint: Use the approach from lecture (no need to provide the pictures) where you
develop a loop invariant as you write the code.
When I saw this question I had no idea of the personal hell it would put me through. I figured it would be quite easy. In fact, at first, it was. I began with the obvious first step: looking at the postcondition and understanding it. And as I understood it, my binary search was to return the highest index of x in A. If x was not present, it would return -1. So I wrote some code that simply found x, and then I added functionality that would allow it to find the highest index.
def binSearch(x, A):
n = len(A)
if n == 1 and A[0] != x:
return -1
p= n / 2
if x == A[p]:
while x == A[p + 1]:
p = p + 1
return p
elif x < A[p]:
return binSearch(x, A[:p])
else:
return p + 1 + binSearch(x, A[p+1:])
It was a few hours later that I ended up realizing that I had misinterpreted the post-condition. My algorithm was not supposed to return -1 if x was not in A. I was supposed to return the index with the highest value less than x if x not in A. This proved a significantly harder to write. It was rather finicky, but I got it done.
def binSearch(x, A):
n = len(A)
p = n / 2
if x > A[n - 1]:
return n - 1
elif x < A[0]
return -1
elif x == A[p]:
while (p + 1 < n) and (x == A[p+1]):
p = p + 1
return p
elif x < A[p]:
return binSearch(x, A[:p])
else:
return p + 1 + binSearch(x, A[p+1:])
Satisfied with this latest algorithm, I wrote up a proof. For the sake of briefness, I'm not going to outline how I came to this proof, but it was a Complete Induction proof due to my algorithm being recursive, and had five cases, due to the five different possible return statements. Happy with my work, I moved on to other questions, and didn't think much of this question again.
At least, I didn't until two days later, when, after a math lecture that I had with a friend who was also in 236, he mentioned in passing something about this question being iterative. "Oh, I did it recursively," I said. "You can't do that. It says on the assignment sheet to do it iteratively." He then pulled up the assignment sheet on his tablet. Sure enough. "Write an iterative binary search algorithm". A stream of expletives flew from my mouth, which I shan't repeat here. All that time writing and refining my algorithm. All that time proving it. All down the drain. I was back to square one. I might as well have not started. Not only had I not understood the postcondition right the first time I looked at it, but I hadn't even understood the question. Clearly I need to work on my detail orientation. I also guess I need to remove any claim to being detail oriented from my resumé.
I went home to work on a new algorithm. It was harder than ever. We were told in lecture once that binary search is a difficult algorithm to write for programmers, as it often ends up off by one in at least one circumstance. Story of this question right here. Try as I might, there was always one case where my algorithm didn't work. I refined it and refined it and refined it. I tried all kinds of things. I scrapped it. I rewrote it. After hours of frustration I finally got it working. But there was still a problem: it didn't allow for a nice proof structure. No matter what, one iteration of the loop would always occur. It made any base case much more complex than it needed to be. I kept fiddling with it. All the other questions were done at this point. Midway through the afternoon on the due date, I finally had a functional, and simple algorithm. An algorithm that was designed with the knowledge that I would have to prove it, and thus was built to be proven. One with better names for variables to prevent confusion in the proof. One that didn't make any iterations in a base condition.
def binSearch(x, A):
b = len(A) - 1
a = 0
while a <= b:
m = (a + b)/2
if A[m] > x:
b = m - 1
else:
a = m + 1
return b
I wasn't out of the woods yet though. I struggled to find a loop invariant. Obviously I wanted the loop invariant to help prove the post condition, so I wanted it roughly in that format, but the obvious choice A[a] <= x < A[b] was not actually correct. Alas, while I had designed my algorithm to be highly provable, I had to make one caveat. Upon loop termination, index a had to be greater than index b. Which meant that A[a] would be greater or equal to A[b] since A was non-decreasing. As such the loop invariant would not hold on the final iteration.
After much thought, and a lack of help from the help centre beyond telling me to write the algorithm differently, I stumbled onto the following loop invariant: A[a-1] <= x < A[b+1]. It seems kind of obvious in retrospect since decreasing a by one, and increasing b by one would obviously make the relationship work, but it really wasn't apparent to me. The second part of the invariant wasn't as difficult, and doesn't require much explanation since it follows from the algorithm and the first part of the invariant: 0 <= a <= b+1 <= length(A). The worst was over. I could see the light at the end of the tunnel. I just now had to prove it.
I regret to say that here I have limited documentation of my process. There were less than six hours remaining until the deadline, and I had to not only finish writing this proof, but type it, and most of the other proofs for the other questions up as well. I threw myself into it. Those almost six hours are mostly a blur of stress, cluttered piles of papers with letters and numbers scrawled all over them, and lots of Red Bull. Most memorably, I had an entire proof for the loop invariant written up, only to realize it was dependent on a being strictly less than b, which was simply not true at all, and I frantically rushed to rewrite the proof to instead function with the relationship in question changed to a < b +1 with less than three hours left, and no typing up even begun on Question 4.
Once I proved the loop invariant, the rest fell into place though. The proof of termination somewhat inelegantly used a fact from halfway through the proof of the invariant as a basis for everything, but hey, it worked, showing that the distance between a (the lower bound on the index of x in the list) and b (the upper bound of the index of x in the list) were decreasing with each iteration as the algorithm zeroed in the location of x. And because I'd been thinking about the overall proof while working on the invariant, the invariant pretty much handed me the correctness proof. It almost wrote itself.
I finished typing it up at 11:54 PM, six minutes before I thought it was due (although in actuality, thirty-six minutes before it was due). I didn't get time to really look it over, although that's largely okay, since I was happy with my proof. But in retrospect I did forget one thing. I didn't quite prove the post-condition. I concluded that since A[a-1] <= x < A[b + 1] and -1 <= p <= n - 1 the post condition held. But that's not quite true. I ought to have said that A[p] <= x < A[p + 1] since p = b = a - 1. They're technically equivalent, but it isn't really clear. Worse is that I never stated anywhere how this actually related to the precondition. It wouldn't have taken much. Since A was non-decreasing,
A[p] <= x < A[p + 1] implies A[0 ... p] x < A[p + 1 ...n - 1], but I never actually said that anywhere.
Unfortunate, but that's how it goes when rushing to meet a deadline.
Question 2
Prove that the following terminates, given the precondition x is an element of the natural numbers:
y = x * x
while not y == 0 :
x = x - 1
y = y - 2 * x - 1
Hint: Trace through the code for a few small values of x, then derive (and prove) a loop invariant that helps prove termination.
The very first thing I did to solve this problem was do exactly what the hint suggested, something I always start with. Tracing code for a few, usually small, values. This is how I always prove things to myself. It's no secret to anyone who reads this sLOG that I'm not the most thrilled with structured proofs. I prefer to justify things to myself with extrapolation of patterns. Kind of like unit testing while programming. Anyway, after having traced through the loop step by step for x=0 through x=5, I had justified to myself that yes, it does indeed terminate. Furthermore, since I had been writing everything down in a list, it was very easy to see that the value of y was always equal to x^2. Even though I was very, very sure, from these tests, as well as just looking at the loop and it's simple nature, I coded the loop up in Python, and ran it with print statements and high values of x. The pattern was always true.
And so, like that I had both proved (to myself) that the loop invariant was x' = x-1, y' = (x')^2 (where x' is x after an iteration, y' is y after an iteration), and that the loop would terminate. Now all that was left was to actually prove it.
The loop invariant proof was actually a lot simpler than I was expecting. By just subbing in the values defined in the loop invariant into the two lines of code inside the loop, I was able to rather easily show that assuming the loop invariant held on the ith iteration, and that there was an (i+1)th iteration, the invariant held. I will say though that, despite the ease, it felt really nice to see it all work out in the end, probably because I didn't at any point get frustrated with this question.
From there, it was trivial to prove termination. The value of x was decreasing by one each time, and since y was x^2, when x was 0, y was 0. The loop would terminate when y was 0. So neither x, nor y, could ever be a value less than 0. Therefore, it was a decreasing finite series, and termination could be proved.
And just like that, it was done. This was the first question I did, since it seemed the easiest. After having done them all, I think I was right in that assumption.
Question 3
Design a DFSA that accepts the language of binary strings over {0, 1} that have a multiple of 4 1s. Devise, and prove a state invariant, and explain how it shows that your DFSA accepts this language.
The natural first thing to do here was draw out the DFSA diagram. I rather thought this was one of the simpler DFSAs we've looked at in this course, but I wasn't by any means complaining. Below is the DFSA I designed; drawn horribly in MS Paint. Bathe in it's glory.
I felt this was something that was quite obvious, but proving it was a lot less so. I struggled quite a bit with this proof despite it being outlined right in the course notes. I was literally staring at the proper form, but didn't understand it. I got the concept. I knew what it was showing - that any given string can be expressed as a string with one less character, and then either a 1 or a 0. For the substring, it can be assumed that the state invariant holds true using complete induction. Then that fact can be used to prove for the two cases (the next character is 1 and the next character is 0) that the state invariant still holds.
I just didn't understand the structure that was being used. I felt the proof shown wasn't very clear about one of the steps. I'd love to detail which one, but honestly, it's hard to express using the text options here, and describing it would just make my lack of terminological knowledge apparent. Suffice it to say that it was an intermediate step, the one in which the assumption regarding the substring led to the conclusion about the string. After probably two hours of looking at it, I finally figured it out. I was looking at the problem all wrong. It was in fact, quite clear. I had just been in the wrong mindset. I was expecting it to follow in a way that it did not follow in. I realize this all sounds cryptic, but I don't know how else to say it.
Once I realized what I was doing, it was simple from there to write it out. Though it took a remarkably long time to type up in Microsoft Word. Using equation tools gives you some nice looking work, but man does it take forever.
Question 4
Design an iterative binary search algorithm that is correct with respect to the following precondition/postcondition pair:
Precondition: A has elements that are comparable with x, |A| = n > 0, and A
is sorted in non-decreasing order.
Postcondition: binSearch(x, A) terminates and returns an index p that satisfies:
A[0 ... p] x < A[p + 1 ...n - 1]
-1 <= p <= n - 1
Prove that if the precondition is satisfied, then your algorithm terminates and satisfi es the postcondition.
Hint: Use the approach from lecture (no need to provide the pictures) where you
develop a loop invariant as you write the code.
When I saw this question I had no idea of the personal hell it would put me through. I figured it would be quite easy. In fact, at first, it was. I began with the obvious first step: looking at the postcondition and understanding it. And as I understood it, my binary search was to return the highest index of x in A. If x was not present, it would return -1. So I wrote some code that simply found x, and then I added functionality that would allow it to find the highest index.
def binSearch(x, A):
n = len(A)
if n == 1 and A[0] != x:
return -1
p= n / 2
if x == A[p]:
while x == A[p + 1]:
p = p + 1
return p
elif x < A[p]:
return binSearch(x, A[:p])
else:
return p + 1 + binSearch(x, A[p+1:])
It was a few hours later that I ended up realizing that I had misinterpreted the post-condition. My algorithm was not supposed to return -1 if x was not in A. I was supposed to return the index with the highest value less than x if x not in A. This proved a significantly harder to write. It was rather finicky, but I got it done.
def binSearch(x, A):
n = len(A)
p = n / 2
if x > A[n - 1]:
return n - 1
elif x < A[0]
return -1
elif x == A[p]:
while (p + 1 < n) and (x == A[p+1]):
p = p + 1
return p
elif x < A[p]:
return binSearch(x, A[:p])
else:
return p + 1 + binSearch(x, A[p+1:])
Satisfied with this latest algorithm, I wrote up a proof. For the sake of briefness, I'm not going to outline how I came to this proof, but it was a Complete Induction proof due to my algorithm being recursive, and had five cases, due to the five different possible return statements. Happy with my work, I moved on to other questions, and didn't think much of this question again.
At least, I didn't until two days later, when, after a math lecture that I had with a friend who was also in 236, he mentioned in passing something about this question being iterative. "Oh, I did it recursively," I said. "You can't do that. It says on the assignment sheet to do it iteratively." He then pulled up the assignment sheet on his tablet. Sure enough. "Write an iterative binary search algorithm". A stream of expletives flew from my mouth, which I shan't repeat here. All that time writing and refining my algorithm. All that time proving it. All down the drain. I was back to square one. I might as well have not started. Not only had I not understood the postcondition right the first time I looked at it, but I hadn't even understood the question. Clearly I need to work on my detail orientation. I also guess I need to remove any claim to being detail oriented from my resumé.
I went home to work on a new algorithm. It was harder than ever. We were told in lecture once that binary search is a difficult algorithm to write for programmers, as it often ends up off by one in at least one circumstance. Story of this question right here. Try as I might, there was always one case where my algorithm didn't work. I refined it and refined it and refined it. I tried all kinds of things. I scrapped it. I rewrote it. After hours of frustration I finally got it working. But there was still a problem: it didn't allow for a nice proof structure. No matter what, one iteration of the loop would always occur. It made any base case much more complex than it needed to be. I kept fiddling with it. All the other questions were done at this point. Midway through the afternoon on the due date, I finally had a functional, and simple algorithm. An algorithm that was designed with the knowledge that I would have to prove it, and thus was built to be proven. One with better names for variables to prevent confusion in the proof. One that didn't make any iterations in a base condition.
def binSearch(x, A):
b = len(A) - 1
a = 0
while a <= b:
m = (a + b)/2
if A[m] > x:
b = m - 1
else:
a = m + 1
return b
I wasn't out of the woods yet though. I struggled to find a loop invariant. Obviously I wanted the loop invariant to help prove the post condition, so I wanted it roughly in that format, but the obvious choice A[a] <= x < A[b] was not actually correct. Alas, while I had designed my algorithm to be highly provable, I had to make one caveat. Upon loop termination, index a had to be greater than index b. Which meant that A[a] would be greater or equal to A[b] since A was non-decreasing. As such the loop invariant would not hold on the final iteration.
After much thought, and a lack of help from the help centre beyond telling me to write the algorithm differently, I stumbled onto the following loop invariant: A[a-1] <= x < A[b+1]. It seems kind of obvious in retrospect since decreasing a by one, and increasing b by one would obviously make the relationship work, but it really wasn't apparent to me. The second part of the invariant wasn't as difficult, and doesn't require much explanation since it follows from the algorithm and the first part of the invariant: 0 <= a <= b+1 <= length(A). The worst was over. I could see the light at the end of the tunnel. I just now had to prove it.
I regret to say that here I have limited documentation of my process. There were less than six hours remaining until the deadline, and I had to not only finish writing this proof, but type it, and most of the other proofs for the other questions up as well. I threw myself into it. Those almost six hours are mostly a blur of stress, cluttered piles of papers with letters and numbers scrawled all over them, and lots of Red Bull. Most memorably, I had an entire proof for the loop invariant written up, only to realize it was dependent on a being strictly less than b, which was simply not true at all, and I frantically rushed to rewrite the proof to instead function with the relationship in question changed to a < b +1 with less than three hours left, and no typing up even begun on Question 4.
Once I proved the loop invariant, the rest fell into place though. The proof of termination somewhat inelegantly used a fact from halfway through the proof of the invariant as a basis for everything, but hey, it worked, showing that the distance between a (the lower bound on the index of x in the list) and b (the upper bound of the index of x in the list) were decreasing with each iteration as the algorithm zeroed in the location of x. And because I'd been thinking about the overall proof while working on the invariant, the invariant pretty much handed me the correctness proof. It almost wrote itself.
I finished typing it up at 11:54 PM, six minutes before I thought it was due (although in actuality, thirty-six minutes before it was due). I didn't get time to really look it over, although that's largely okay, since I was happy with my proof. But in retrospect I did forget one thing. I didn't quite prove the post-condition. I concluded that since A[a-1] <= x < A[b + 1] and -1 <= p <= n - 1 the post condition held. But that's not quite true. I ought to have said that A[p] <= x < A[p + 1] since p = b = a - 1. They're technically equivalent, but it isn't really clear. Worse is that I never stated anywhere how this actually related to the precondition. It wouldn't have taken much. Since A was non-decreasing,
A[p] <= x < A[p + 1] implies A[0 ... p] x < A[p + 1 ...n - 1], but I never actually said that anywhere.
Unfortunate, but that's how it goes when rushing to meet a deadline.
Subscribe to:
Posts (Atom)