**Part I: Tail Recursion**

Consider the following definitions:

type nat = int 

let rec fact (n:nat) : nat =
  if n <= 0 then 1
  else fact (n-1) * n   

let rec fib (n:nat) : nat =
  match n with
  | 0 -> 0
  | 1 -> 1
  | n -> fib (n-1) + fib (n-2)

let rec len (xs:nat list) : nat =
  match xs with
  | [] -> 0
  | hd::tl -> 1 + len tl

type cont = nat -> nat

(1a)
Write the following tail-recursive functions using continuation passing style:
fact_cont : nat -> cont -> nat
fib_cont : nat -> cont -> nat
len_cont : nat list -> cont -> nat

(1b)
Write another set of tail-recursive equivalents using accumulating parameter style:
  




(1c)
Prove that your continuation-passing function fact_cont is equivalent
to the original version of fact presented above.  In other words,
prove the following lemma and then the theorem:

Lemma: For all natural numbers n, 
         for all k:cont, fact_cont n k == k (fact n)

Theorem: For all natural numbers n, 
           fact_cont n (fun m -> m) == fact n

You could do the same for the other functions. 

**Part II: Closure Conversion**

Closure-convert the following code.  In other words, rewrite the
functions apply and sum (call them apply_code and sum_code) so that
they contain no free variables.  Ensure the resulting code type
checks.

let c = 5
let d = 6

let apply (f : int -> int) : int = f (c*d) 

let sum (y : int) : int = y + c + d

let result = apply sum


**Part III: Induction: Trees**

type tree = Leaf | Node of int * tree * tree

let rec inc (t:tree) (a:int) : tree =
  match t with
    Leaf -> Leaf
  | Node(i,left,right) -> Node(i+a, inc left a, inc right a)

Prove the following theorem:

Theorem: for all t:tree, inc (inc t a) b == inc t (a+b)