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.

Oct 28 - Week 8

Last week we did a proof about the binary search. I begin to doubt is it always the case that we use strong induction to prove the program correctness? At least for now I assume so. The proof structure is not quite complexed. Just as normal strong induction, we will assume P(1) up to P(n-1). As the programming code come into play now, we have to analyze what does these code do at the same time. Binary search has got a basic case, which is the input first index and last index is the same. It means we go through the entire list, so the if the index position indeed contains the element we want, then we are done. Otherwise we can not find anything, since we assumed the entire list has been gone through. This satisfies both precondition as well as postcondition. After finished the base case, we will play with the rest of the program for a well. The key part is how the program divide the list into two parts. That generate the proof into two separate branches. First is the list from the first to the m index, the other one runs from m+1 to the last. By comparing the element to the value of m, it will make the list smaller and smaller. We can not forget to check whether the precondition still holds at the same time.
The greatest common divisor example seems ambiguous to me. I sort of understanding how the proof is made, but have some problems understanding how does the program works.

I missed Monday's lecture, and did not have a chance to hand in the problem set 4 which was printed two days ago. I believe I will go to Thursday evening's lecture.

Oct 20 - Week 7

Professor Danny was missing today, but that doesn't mean we didn't have a passionate class. Instructor Nick starts the class with a statement "No programs will never crush.". Quite interesting, eh? He then lead us go through the Binary Search algorithm. By that he introduced us "Precondition" and "Postcondition". The postcondition is guaranteed to happen provided the correct precondition is given.

Sept 29th - Week 3

On today's lecture we begin to touch some aspects of the recursion and its proof.
We started by proving a recursive f(n) which f(n) = 0 if n =0, otherwise f(n) = f(n-1) + 3n^2.
Then we get into the Fibonacci sequences by a rabbit example. We tried a few base cases and figured out some patterns between the summation of the entire sequences and F(n).

Sept 24th - Week 2

On Monday we have discovered "Principal of well ordering".

Today we have gone back to some simple induction proofs.