From my last post, the answer of my unwinding was wrong., due to the complex of unwinding an equation that end up of having a summation from 1 to n. When having a summation from 1 to n, it has to be simplified to a certain form and replace with a certain formula. This is the most difficult step I found when unwinding.

It’s just been 2 days from term test 2 on Thursday. On the test, there was a question about proving the correctness and termination of the function. This topic was just taught last week. We didn’t really have a chance to practice on tutorial or assignment, so I was not familiar with the question and spent most of the time on it. Still, the question was a bit easier compare to what we have done in class. In test, Pow(x, y), the arguments are just numbers, but in class, the one of the arguments is usually a list. When given a list, we have to keep track of this indexes of the list, (ei, e, b, m), which can easily turned into a mess when proving the post condition, correctness and termination. Different from csc165, pre and postcondition, and loop invariant are not given, and we have to determine them by tracing the function. Although it has covered in class, it's a big mess with all this, e+1, m+1, b+1, e+1-b, e+1-m-1, b-1+1+e, etc. It was gone through quickly in class, but it required much more time to analyst them. We didn't have tutorial this week, and same next week. I find it hard to understand with the lack of practice. But I think now is a good time to do practice questions on past exams.

Closed Form by Unwinding

The main topic of this week is to find the close form and prove the upper bound of a given program. Proofing the upper bound I found is relatively easy, because we only have to proof the inequality. We can always make a bigger approximation of the given equation, which it doesn't have to be exact. However, when finding the closed form, we have to analyze the pattern carefully and find the exact equation that will cover the whole set. And the best way to understand the process is working through a problem.

In tutorial 4 question 2 is to find the closed form of T(n). Given n is a power of k; substitute 3^k into T(n). T(n) = 3T(3^(k-1)) + 3^2k, and substitute T(3^(k-1)) = 3T(3^(k-2)) + 3^(2k-1). So, T(n) = 3^2T(3^(k-1)) + 3^(2k-1)(1 + 3). And substitute repeatedly until T(3^(k-k)). The main goal in unwinding is to find the pattern, and I found that if this process repeated k times, the pattern of T(3^k) seems to be 3^k + 3^(k+1)(3^0 + 3^1 + ... + 3^(k-1)). This is the closest I can get to the closed form of T(n). However, calculating (3^0 + 3^1 + ... + 3^(k-1)) still takes a bit of time, so maybe there is a shorter closed form; which I have to confirm during the tutorial.

week 5 - First post

This week is the week of Term Test 1. Writing SLOG while reviewing for the test is probably a good idea, such that I can check if I really understand each different proof strategies. In Assignment 1, the questions had covered Mathematical Induction and Complete Induction. By struggling through the questions, I have now a better understanding of how to structure the problem into MI and CI differently. To me, MI seems to work well on mathematical equations, where we can use algebra to manipulate the equation into something already purposed in the inductive hypothesis. CI in contrast, the strategy of partitioning seems extremely important. We can break down the problem into smaller subsets so we can apply what we assumed in IH to solve the problem.

The real problem, however, is Proof by Well Ordering and Structural Induction, which we haven't had a chance to practice and get familiar with the thoughts and proof structures. In PWO, by simply assuming that every set has a smallest element can solve the problem seems to be confusing. In the 3 player cycle example, this seems to make sense, since we are able to show that 3 being the smallest possible case. But in general case, where we have only an arbitrary variable, PWO doesn't seem to get you anywhere. Lastly SI, which seems a lot similar to MI, thus the proving structure in MI should work with SI too. I should then focus on PWO such that I can prepare for the test.