--------------------------------------------------
LOGISTICS:

* David Liben-Nowell
  dln at theory.lcs.mit 
  32-G694

* Office Hours:  R10-12.

* 1.5 handouts:
    -- my survey.
    -- PS1 is posted.

* Some points about recitation:

    -- we will cover new material!

    -- so section is as mandatory as lecture is, except more (since
       there are no videos).

    -- I am responsible for assigning grades for you.

    -- I expect this to be the kind of situation where:
         1) you feel comfortable asking anything.
         2) you participate actively.

    -- my annoying habit #1:  I demand feedback as we go.


--------------------------------------------------
ADVICE ON HOMEWORKS:

* Read the problems and let them percolate in the back of your brain
  for as long as possible.  Even if you don't start writing up your
  solutions until the day before the PS is due, you'll make your life
  infinitely easier if you read them a week before.

* For the first few problem sets, give a completely rigorous proof of
  correctness.  As the term goes on, "sketches" will become okay.

* Go for correctness first, then for performance.  It's easier to make
  a slow algorithm fast than a buggy algorithm correct.

--------------------------------------------------
Lectures this week:

  * Monday:  Labor Day.
  * Wednesday:  insertion sort, merge sort, asymptotic analysis.
    --> don't be scared about Theta-notation; it'll be covered in
        lecture on Monday.
--------------------------------------------------

PROOFS OF CORRECTNESS:

* How do we rigorously prove correctness?

  [OMIT THE SPEC.]
  // INPUT:  a sorted array A[1..n], and a number key.
  // OUTPUT: true iff key is in A (exists i in {1...n}  A[i] = key).
  linear-search(A,key) 
  i <- 1
  A[0]   <- -Infinity
  A[n+1] <- Infinity  <--- leave this out the first time!

  WHILE (key > A[i])
    i <- i+1
  IF key == A[i]
    THEN RETURN true
    ELSE RETURN false


  Is this correct?
  What does "this is correct" even mean?  [now add the spec.]
  Why is this correct?                    [now add A[n+1]<-infty.]

* From lecture, we need:
    1) it always terminates.
    2) when it terminates, it produces the right answer.

* Major tool for proving correctness:  mathematical induction.  
  (Of course.)

  How do we prove correctness for this algorithm?

  LOOP INVARIANTS: 

  a _loop invariant_ is a relationship among the variables in the
  algorithm.

  there are *many* such relationships; the hard part is finding one
  that allows you to prove correctness.

  (1) come up with a useful loop invariant.
  (2) prove that the loop invariant is truly invariant.
  (3) prove that the loop terminates.
  (4) prove that the algorithm is correct (given termination and the
      loop invariant).

  What does i measure in the linear-search loop?
    key > A[i-1].

  Here's a more detailed outline of the above:
  (1) Define a _precondition_ PRE that is true upon entering the loop.
  (2) Define a _postcondition_ POST that is true upon exiting the loop.
      POST == "what we want the loop to do" (=> correctness of algorithm)
  (3) Define a loop invariant L.
  (4) Prove by induction that L holds after every iteration of the loop.
  (5) Prove that (L AND "the loop terminates") => S.
  (6) Prove that the loop terminates.


  // PRE:  i=1, A[0] = -infty, A[n+1] = infty.
  WHILE (key > A[i])
    i <- i+1
    // L:  A[i-1] < key
  // POST: A[i-1] < key <= A[i]


  Prove that L holds:  well, we check it every time before we increment i!

  Prove that L + termination => S.
    -- obvious.  Termination:  key <= A[i].
		 L:            A[i-1] < key.

       so we have A[i-1] < key <= A[i].

  Termination:
    -- if we ever reach i=n+1, then the test will fail.
    -- i increases in every iteration.
    -- so we eventually terminate.


  Thus the algorithm is correct!

  (What's the running time?  O(n).)
------------------------------

  binary-search(A[1..n],key)

  A[0] <- -infty
  A[n+1] <- infty
  left <- 0
  right <- n+1

  WHILE (left != right)
    mid <- ceiling( (left+right)/2 )
    IF key < A[mid]
      THEN right <- mid - 1
      ELSE left  <- mid
  IF key == A[left]
    THEN RETURN true
    ELSE RETURN false.


  * What are PRE, L, POST?

    PRE:  left = 0, right = n+1, A[n+1]=infty, A[0]=-infty.
    L:    A[left] <= key < A[right+1]
    POST: A[left] <= key < A[left+1]

    Prove that L holds by induction on the number of iterations of the loop.

      Base case (0 iterations): 
	   immediate by precondition.

      Inductive case (k+1 iterations):
	   let left', right' be the values at the start of (k+1)st iteration
	   and left,  right  be the values at the start of (k)th   iteration.

	   By the IH, we had A[left] <= key < A[right + 1].

	   For the case in which (key < A[mid]):
	       we set right <- mid - 1.
	       So A[left'] = A[left] <= key < A[mid] = A[right'+1].

	   The other case is similar.


	   Done!

  * Why does this terminate?

    (right - left) is always decreasing.
    we terminate when right=left.

  * What's the running time?

    T(n) = T(n/2) + Theta(1)
    T(n) = log(n).
------------------------------

HORNER'S ALGORITHM:

Here's another problem:

Given a polynomial f(x) = a_0 + a_1 x + a_2 x^2 + ... + a_d x^d
How do we evaluate f(x) for a given value x?

INPUT:  array A[0..d], x.
OUTPUT: A[0] + A[1] x + A[2] x^2 + ... A[d] x^d.

Naively:  calculate each term, and add it up.
How many operations?  \sum{i=0}^d d = Theta(d^2).

Instead, think of f(x) as
	 a_0 + x(a_1 + x(a_2 + x( ... + x(a_d)))).

Horner(A[0..d],x)
  val <- 0
  FOR i <- d DOWNTO 0
     val <- A[i] + (x * val)
  RETURN val


PRE:  val = 0.
POST: val = sum_{j=0}^{d} A[j]x^j
L:    val = sum_{j=i+1}^{d} A[j]x^{j-(j+1)}