Showing posts with label proofs. Show all posts
Showing posts with label proofs. Show all posts

Sunday, 31 March 2013

Halt Right There!

I'm going to be brutally honest here. I haven't had time to review course notes recently and so I was really really lost during the lectures involving reduction and halting functions. I had almost no idea what was going on and I was really confused.

Halts? Halting? Naval_gaze? Infinite loop? Halt cannot exist? What?!?

I felt horrified that I didn't have the slightest clue what was going on especially since Assignment #3's deadline was closing in, which involved using halts. So I did some strenuous reviewing of the lecture notes along with the course notes.

After reviewing, I still felt dazed and confused about what a function halts was all about. It was only when I was semi-explaining (I had a vague idea of what halts was but didn't really understand it) the course notes/lecture notes to a fellow CSC165 classmate that I had an epiphany and almost fully understood what halts is all about.

Halts is a function that would take a function and an input as a parameters and return True if and only if the given function halted on the given parameter.

Halts has proven to not be computable (i.e. impossible to write in code) because there exists a contradiction. The proof is in the course notes on page 70. With this knowledge in mind, we can reduce the halting function to another function that is similar and show that a contradiction exists to prove that this other function can not be computed as well.

For example, let's consider this function (I made this example and I'm assuming this function is not computable so let me know if I'm mistaken):

def prints_something(f, x):
    ''' (function, object) -> bool
    Return whether the given function prints anything on the given input x.
    '''
    # Here exists valid Python code that scans the functions codes and
    # returns True if and only if the given function prints anything on
    # the given input x

Now, let's assume this function is computable and reduce the uncomputable function halts to this function:

Assume prints_something is computable

def halts(F, i):
    ''' (function, object) -> bool
    Return True if and onlf if function F halts on input i.
    '''

    def prints_something(f, x):
        ''' (function, object) -> bool
        Return whether the given function prints
        anything on the given input x.
        '''
        # Here exists valid Python code that scans the functions codes and
        # returns True if and only if the given function prints anything on
        # the given input x

        pass
   
    pass


So far this doesn't tell us anything. Now let's create an arbitrary function that function prints_something will analyze:

def f_naught(g):
    ''' (str) -> NoneType
    After calling F(i), the function and input that was passed
    to halts as arguments, print g.
    '''
    F(i)
    print(g)

Considering the function f_naught, we can see that if F(i) (a function and input that was passed to halts) halts, f_naught will print something thus prints_something will return True. If F(i) does not halt, f_naught will never print something and prints_something will return False.

So now let's put all these functions together. Obviously, f_naught must go into halts since it uses F(i) from halts:


Assume prints_something is computable with valid Python code

def halts(F, i):
    ''' (function, object) -> bool
    Return True if and onlf if function F halts on input i.
    '''

    def prints_something(f, x):
        ''' (function, object) -> bool
        Return whether the given function prints
        anything on the given input x.
        '''
        # Here exists valid Python code that scans the functions codes and
        # returns True if and only if the given function prints anything on
        # the given input x

     def f_naught(g):
        ''' (str) -> NoneType
        After calling F(i), the function and input that was passed
        to halts as arguments, print g.
        '''
        F(i)
        print(g)
   
    return prints_something(f_naught, '')

If F(i) halts, prints_something(f_naught,'') will return True because the "F(i)" line in f_naught will stop running, thus allowing print(g) to print something.Thus halts(F, i) will consequently return True as well.

If F(i) doesn't halt, prints_something(f_naught, '') will return False because the "F(i)" line in f_naught will never stop running, thus never allowing print(g) to print anything. Thus halts(F, i) will consequently return False as well.

Thus halts(F, i) returns True when F(i) halts, and it returns False when F(i) doesn't halt.

Now, the problem should be pretty clear. We've somehow successfully created a halting function!

The meaning of reducing one function to another is if this inner function can be made, the outter function can be made. Thus:

prints_something is computable implies halts is computable.

But there exists a contradiction; halts was previously proven to not be computable

Also, if we take the contrapositive of the statement:

"prints_something is computable implies halts is computable"

 We get:

"halts is not computable implies prints_something is not computable"

Thus, since halts was previously proven to not be computable, this implies prints_something is also not computable!

I hope this helps someone better understanding the halting function and related information!

Sunday, 24 March 2013

Understanding Big-Oh (upperbounds) with the help of 1i

The concept of Big-Oh can be quite terrifying if you don't really understand it at first. However, after more rigorous overview of course notes and reading students' slogs about Big-Oh, I felt much more comfortable with this concept and now I know why it is such an important concept for computer science students.

Refer to 1i's March 21st, 2013 slog post : http://oneicsc165.blogspot.ca/

In this course, we've been dealing with proofs for a while now and it is fairly easy to just focus on the the structure of the proof, the symbolic statement of the proof, and the math involved in linking the antecedent to the consequent. However, because it is fairly easy to do this now and it almost becomes an automatic thought process, it becomes fairly easy to forget about what each line actually means outside of all the math and steps.

This is why I liked 1i's approach at understanding exactly what Big-Oh means by going through and understanding each step of a proof. If you understand what each of the relevant lines of the proof mean instead of just performing the steps to finish the proof, you'll have a better understanding of Big-Oh.

Through each step, 1i continuously reminds us that we are making our function f(n) that is bounded by our function g(n), bigger and bigger and eventually it is shown that a constant multipled by function g(n) is still bigger in the end. This is what it means to have an upper bound and this is what Big-Oh means. Through the proof, which I initially thought was just some mathematical equations, operations, inequalities, etc that would not give us a bigger/real world picture, and through 1i's slog post, I now have a better understanding of what Big-Oh actually means.

Thanks 1i for your post!

Wednesday, 27 February 2013

Proofs: Simple Structures, Complicated Content

I just wanted to slog about how to generally start a proof and set it up/structure it. There is nothing more really to say about writing up proofs beyond that because each proof is unique and the meatiest part of the proof, finding the connections, is vastly different with each different proof.

The example I will be using (even though this example is covered in lecture, I want to go more in-depth, step-by-step):

"For every natural number n, n² odd implies that n is odd"

1. Decide whether you want to prove the statement or disprove the statement. Do this by using intuition or scribbling some cases you think will make the statement wrong. Basically look for some counter-examples.

Since I can't think of any odd numbers` that has an even root, I'm going to attempt to prove this.



2. Now you're ready to begin. Always start with the symbolic representation of the original statement of what you're trying to prove or disprove. After figuring out the symbolic representation of the statement, if you decided you want to disprove it, NEGATE the statement before proceeding with the next steps.

  • What does an odd natural number mean symbolically??? We'll have to refer to the symbolic definition of what it means to be an odd number by either looking it up on the internet, or finding it in the Course Notes.
  • We see that for a natural number to be odd, it means there exists a natural number where 2 multiplied by that natural number, plus one, equals to our odd number. Thus the symbolic statement would be:
∀n∋N, (∃ k∋N, n² = 2k + 1) ⇒ (∃ k₀∋N, n² = 2(k₀) + 1)
  • Since we want to prove this, then we don't need to negate it.

3. Now it's time to set up the structure for the proof, while leaving out the meat of it. While setting up the structure for a proof, you want to follow these guide lines:
  • Start from left to right of the symbolic statement
  • Whenever you have have a Universal Quantifier (∀), you want to assume there is a generic number of this set, and then proceed with the proof with everything below with one indent. After completing the structure and/or proof for all the proceeding elements after the universal quantifier, the whole statement after the universal quantifier, including the universal quantifier should be restated in conclusion form, aligned vertically with the original assumption line of this universal quantifier. 
    • Assume x∋Y     # x is a generic to introduce ∀ 
      • proceeding lines start here vertically (without a bullet obviously)
      •  
      • # ***Lines connecting the antecedent to the consequent ***
      •  

    • Then x∋Y................  # conclude for all x in Y
    • For our example:
      • Assume ∀n∋N     # n is a generic natural number to introduce ∀
        •  
        •  
        •  
      • Then  conclude ∀n∋N, (∃ k∋N, n² = 2k + 1) ⇒ (∃ k₀∋N, n² = 2(k₀) + 1)  # for all n in N
  • Whenever you have an Existential Quantifier (∃), you want to "pick" or "let" that number equal to something that you haven't decided yet, unless the existential is a part of your antecedent for a direct proof. So you want to have either:
    • pick x = _____ then x∋Y
    • or let x = _____ then x∋Y
    • For our example, since our existential is part of our antecedent for a direct proof, we don't pick until we get the the consequent part of our proof
  •  Whenever you get to an antecedent of an implication, you want to assume the antecedent is true and the lines proceeding the proof should be indented by one. The proceeding lines should be the meat of your proof where you show a connection from the antecedent to the consequent. Then, after these lines, the consequent should be stated. Then on the next line afterwards, the whole implication should be stated without the indent, thus lined back up with the antecedent vertically.
    • Assume x = y   # x = y is an example antecedent
      • proceeding lines start here vertically (without the bullet obviously)
      •  
      •  
      • then consequent 
    • Then x=y ⇒consequent
    • For our example:
      • Then ∃ k∋N, n² = 2k + 1
        •  
        •  
        •  
        • Then ∃ k₀∋N, n² = 2(k₀) + 1
      • Then (∃ k∋N, n² = 2k + 1) ⇒ (∃ k₀∋N, n² = 2(k₀) + 1)
  • Keep in mind that the meatiest part of the proof, the fruit of the proof, the most meaningful part of the proof, the hardest part of the proof, are the ***Lines connecting the antecedent to the consequent ***, from the antecedent assumption. Thus you can have this structure set up while leaving space for these lines.
4. If you suspect that your antecedent implies a conjunction, you may want to have different cases set up in your proof that follow the same structure guidelines.

5. Now that you have enough information to start, setup, and structure a proof, all you need is to figure out the hard part of connecting any antecedent to the consequent. In the case of just showing if a conjunction or disjunction is true, the same structure can be followed.
  • For our example:
    • Then ∃ k∋N, n² = 2k + 1
    • Then n² - 1 = 2k
    • Then (n + 1)(n - 1) = 2k
    • Then n = 2(k/(n+1)) + 1
    • Then let k₀ = (k/(n+1))
    • Then∃ k₀∋N, n² = 2(k₀) + 1

6. When concluding a disprove, state that the original statement is incorrect because you showed the negation to be true.

7. This is just a simple guide, there are many other things you may need to think of while proving such as should you take the contrapositive of the statement? Should you perform a direct proof? Should you perform an indirect proof? Should you prove by contradiction? Etc.

So he final product for our proof of ∀n∋N, (∃ k∋N, n² = 2k + 1) ⇒ (∃ k₀∋N, n² = 2(k₀) + 1)
is:

  • Assume ∀n∋N     # n is a generic natural number to introduce ∀
    • Then ∃ k∋N, n² = 2k + 1
      • Then n² - 1 = 2k
      • Then (n + 1)(n - 1) = 2k
      • Then n = 2(k/(n+1)) + 1
      • Then let k₀ = (k/(n+1))
      • Then∃ k₀∋N, n² = 2(k₀) + 1
      • Then ∃ k₀∋N, n² = 2(k₀) + 1
    • Then (∃ k∋N, n² = 2k + 1) ⇒ (∃ k₀∋N, n² = 2(k₀) + 1)
  • Then  conclude ∀n∋N, (∃ k∋N, n² = 2k + 1) ⇒ (∃ k₀∋N, n² = 2(k₀) + 1)  # for all n in N

So this would be a proper proof with proper structure (minus the bullet points on each line).

Hope someone finds this helpful!