2009-06-24

Post date: Jun 25, 2009 12:23:02 AM

In talking about the sample Final Exam, spent almost all the time on Question 7:

    • Lambda calculus primer, t ::= x | t t | λx.t
    • Use "canonical form" strategy to break down function type. If we want to construct a term t that type A → B, the term t has to have the form λx.t0 where x (the argument) has type A and t0 (the body) has type B (in ATS, it would be written as lam x => t0).
      • If A is a function type, that means x is a function given to us.
      • If B is a function type, then recursively break down B using the canonical form strategy.
      • If B is not a function type, then look at all the arguments we are given so far (some of them are functions), and see if there is any combination of the function call that will give us B.
    • Sometimes it may be useful to do function composition to obtain the required type, i.e. given f: A → B and g: B → C, if we want a function that has the type A → C, then we can write λx.g (f x).
    • Use the typing rules of lam and app to verify your result is correct.
    • Motivated why these typing rules are written the way they are.
      • Operational semantics t ⇒ t' means that t is reduced in one step to t'. Imagine your program is a very long expression which runs by reducing to smaller programs until it becomes a value, which is irreducible, representing the result of computation. The only rule we're interested here concerns function call: (λx.t0) t ⇒ t0[x := t], by substitution all occurrences of variable x inside the function body with the term passed in as the argument. This is called β reduction.
      • Call by value: evaluate argument t to a value first, then substitute for function call. Call by name: substitute t into the function body, and evaluate individual occurrences of t separately. If t is an expression that prints out a string, call by value only prints once prior to the function call, and call by name prints as many times as x occurs in the function.
      • Type preservation theorem: if ∅ ⊢ t : A and t ⇒ t', then ∅ ⊢ t' : A, i.e. the intermediate steps of evaluation doesn't change the type of your program.
      • Substitution lemma: if Γ, x : A ⊢ t0 : B and Γ ⊢ t : A, then Γ ⊢ t0[x := t] : B. This lemma describes what's the correct behavior for β reduction, which governs how lam and app rules can be written if we want the type system to be sound.
    • Will go over some dependent type examples tomorrow at 2pm.