Problem-Solving Episode

Since I feel most uncomfortable with proving the recursive, so I was looking for some kind of proof related to recursive function . Luckily, though I was in the morning section but I know someone in the evening section who is able to borrow his second term test to me. I found a interesting one:

def CheckPal(s):
1 #Precondition: s is a python string.
2 if len(s) <>
3 else:
4 s_inner = s[1:len(s) - 1]
5 return s[0] == s[len(s)-1] and CheckPal(inner)
6 # Post return true if s is a palindrome.

1. Understanding the problem
As the function is never tested on a machine, we can read through it and find it might work, but that would not be sufficient to justify this function behaves exactly what we expect. The function is known, and to prove it is correct is what we are heading for.

2.Devising a plan
According to standard proof "pattern" we have been using in this course, it will be either a simple or complete induction. Where in this case, strong induction seems more suitable.

3.Carrying out the plan
So I argue P(n): if n = len(s), the precondition implies the post condition, I claim that \forall n \in N, P(n) always holds for true.

Here is the proof:
Assume n \in N, and assume P(0) and P(1) and ...... and P(n-1) is true, assume pre condition holds for any arbitrary string s.

Case 1: Assume s is a python string and n palindrome and a character itself is a palindrome too, which in both cases satisfying the post condition. Therefore P(0) and P(1) is true.

Following cases are all based on s is a python string, which satisfies the pre condition.

Case 2A: If n >= 2 and n is even, line 1 fails and line 4 gets executed. A sub string is taken from the second letter to the second last character. As such, the length of the newly created string would be a even number as well. After that, line 5 runs and it will evaluate s[0] == s[len(s) - 1], which is checking if the first and last character is the same, and this is exactly what we are heading for. Meanwhile, this line also generated a recursive call to evaluate the s_inner string to see if it is palindrome, the recursive call will follow the steps below, moving towards the post condition, therefore P(n)

Case 2B: If n >= 2 and n is odd, line 1 fails too, a substring is formed from the second character to the second last character and set this string to variable s_inner. However the length of this string is odd. Line 5 will evaluate s[0] == s[len(s) - 1] as well as CheckPal(s_inner). Differ from case 2A, this recursive call will sooner or later left with a string containing only one character, which is saying n = 1, at that time line 2 will executes, and if it is palindrome, the call stack will return true all the way to the main function call, otherwise it will return false, which in both cases satisfying the post condition.

So P(n).

4. Looking Back
This loop is not a very complicated one, and for some reason I do believe I can prove it with the simple induction, but the even or odd length will be tricky if I am with the simple induction. Proving the program's correctness is essential not only theoretically, but also in practice, if a function does not behaves what we like it to be, and we can have a pretty good idea of where it can be wrong if we were to prove it.

Week 12

In week 12, we started a topic called pumping lemma. It is meant to testify that "Not all languages are normal". It is defined by: x which is the string belongs to normal language L, a integer length p which limits the length of x to be at least as long as p(|x| >= p). Then we cut x into three pieces --- u, v and w. The length of the first two element u and v is limited to |uv| <= p. v can not be a empty string. So if we pump up v by k times, for all integer k we should still have u(v^k)w \in L. This theory fails sometime, so we that proves not all language are normal.

After that we started a quite interesting example that has something to do with the recipe, I never thought recipe could actually has relationship with the computer science! Through the process of "making an sandwich" we learnt what is context-free grammars. Like the FSAs we have whole bunch of symbols. V denotes a set of variables, \Sigma indicates a set of terminals which means it would be the end of the "recipe" no further extension is allowed. Like the FSAs it has the starting point which is S.

Recall Week 4 to Week 6

On week 4 we talked about the recursion, thought we've been using recursion functions in programming language courses, and I hated it since it is hard to follow what is going on compare to a loop. This chapter will helped me understood the recursion better for sure. The Fibonacci sequence is used for demonstrating the unwind steps. I actually found it was quite hard to convert a expression that is originally defined in the recursive way, to a one line mathematics equation. I did tried some related problems, and found they are all very useful, but I guess the core reason is that I do not feel safe with recursions, by this I mean it is harder for me to monitor each steps, unlike a for or while loop, though as a matter of fact other people may find it is neat to use a recursive call rather than a loop. After that we focused on the recursive binary search function. We followed through the steps and I find it's really useful to actually sit down and see what each variables and the return value can vary after the first time, the second time ... until it hits the stop point. The last part is the Time Complexity for a function. We actually did the similar topics in CSC165 and I still remember we used the big O to give a approximate timing for the worse situation that a program can happen. It become more precise here. Actually we do know the logN is the time complexity for binary search, but it is still cool to see we actually proved it.

In week five we went through closed form recursive functions, and in week six we were dealing with an instance of sort algorithm called merge sort. The merge sort is kind of nice; as it keeps dividing the huge thing into small pieces, until it reaches the size of 1, then combine them together. And this leads to the divide and conquer theory. Honestly speaking I am really not that familiar with these two chapters, but I will definitely take a close look when I begin to do the review work. Besides, we also did some unwinding stuff and proof. Unwinding seems pretty easy, but I found it looks easy, but when you actually sit down and do some problems you will find it takes some tricks to unwind, at least for me. It is not that straightforward as proof. I should work on more similar problems to make myself comfortable with this.

Week 11

We use to deal with the DFSA which stands for determined finite state automaton. In some cases the string doesn't always proceed into one state, as such we have the non-determined FSA concepts introduced in. The NFSA is defined in a similar way as DFSA, which still holds Q as a finite set of states, the \Sigma is a finite alphabet, and the \delta which was defined in a more weird way, it was Q * (\Sigma \union {\epsilon}) \implies P(Q). The rest are what we have in DFSA: s\in Q as the starting state, F \in Q as the accepting state. We can somehow transform a NFSA into a DFSA. So there is a "theory": every NFSA has a equivalent DFSA. For regular expressions, we got a NFSA to represent every regular expression as well.

After that we experienced the process of transferring a NFSA to a regular expression. We first add \epsilon state to it, and then begin to cut off any state as we please. Usually through this state you can travel to certain states via certain paths. Mark these path down and we have got the regular expression. For example if it takes a string 1 to go to another state and a string 0 to come back, we will have a string 10 as its path. After we cut off this state, all paths with destinations to itself will be derived to a self-loop of another state. The path we marked down earlier will become its self loop condition. As we repeat this process, we will eventually have two states left with a whole bunch of regular expression as the bridge between the two. One is the starting state and anther is the accepting state. By the end of the lecture we also realized that there is some kind of language that is hard to denote using our current method. Like the binary string with the same numbers of 1 and 0.

Week 10

We start today's lecture by introducing some regular expression tricks and rules. It would be helpful to simplify the regular expression, or to find out if two regular expressions are equivalent. After that, we realize that there are certain things that regular expressions are not capable or hard to achieve. Here we have Finite State Automata kicked in. It defines the language into certain paths and routes between the states. The states are denoted by a circle and the route is the condition that each character of the language or string has to go through. Ideally the language or string will begin at a certain state and if it ends at the designated state we will call this string or language is "accepted", or otherwise it ends up at somewhere else, we call it was rejected. We define a DFSA like defines a function. We let Q be a finite set of states, the \sigma is used to describe a transition function. The s \in Q is the start state while the F is the accepting state. So we simply say \sigma(s,x) ={certain states if something happens.}. I thought this algorithm will be extremely to solve the problems like defining a certain amount of letters appears in a string where in this case regular expression will be hard to denote.

Week 9

Language is introduced today with several methods associated with it. We start by defining strings. Though we have been using it quite frequently but we rarely really stick into it. Alphabet is introduced as well, this one is not the same one in English. Sigma, which used to denote summation, is used to denote Alphabet here. Just like the Alphabet in English, the Alphabet we are talking about also contains all the candidate that are waiting to be choosing and combining to form different strings. All the possible combination will be Sigma*. There are several manipulating options for strings as well, for example you can concatenate two strings into one, take the length of the string, make a reverse of a string, or take nth power of a string. Beyond a string we have another concept called language, and it's not a nature language we are talking about. The language is formed from sigma. So we can certainly make a union or interaction of two languages, make a copy of concatenation of the two, and the most important Kleene star. The Kleene star is all the possible concatenation of the two language. After that we talked about the regular expression. I have never ever heard regular expression before so it really took a while for me to become comfortable with it. I looked up it on the wiki, and figured out what "*" and "+" means. Since this is essential for CSC207 as well, I will definitely do more exercises with the regular expression.

Oct 30 - Week 8

Since I missed this Monday's lecture, I'd decide to go to the evening instead. Surprisingly, I found the evening lecture is much better than the morning sections. Perhaps it's because there are fewer people prefer to listen a lecture in the evening.

We went through the pow_revisited example, which contains one simply while loop. It was quite obvious and meant to show us the structure of proving a loop is correct. The "trickier termination" is indeed tricker. A girl came up with the question with what if value a become negative? I was wondering the same thing at that time either. Well fortunately a won't be decremented as long as b is not zero, and in that case this statement is assumed. This would be the trickiest part, as only every time b becomes zero, a will decrement by 1, and b's value will be back to 6 again. It's not that obvious to figure out what the loop is behaving at the first place. And this is not the worst, the last example is a selection sort function, which contains two for loops. The algorithm is not hard, but you will likely yo lose the track of in dices as you are writing the proof. As Professor Danny said, never use any letter that is a index in the program in your proof, since that will really drive us into trouble.

Besides, we also need to check if the loop is ever going to end. At this point I like for loop more, as most of the time it has a finite set of content to iterate. For while loop I have to check the statement which it moves the iteration forward. Luckily if there is more than one condition along with the while loop, it will generate cases.

Overall, I do believe I kind of get what I am supposed to do when I were to write a proof about a loop --- that is, to find out the pre and post condition (wonder if there is any chance that these two conditions are given in the questions?), find out an expression of what the loop does (not sure what officially that calls) and try to make sure the loop ends.