I. why study the theory of programming languages? A. arguments for the study of theory 1. need to abstract and generalize 2. programming is langauge design 3. formal semantic description techniques are a standard design notation a. deep understanding of elements of existing languages b. one key to future implementation techniques and optimizations c. tools for comparing languages d. tools for judging your design ideas e. help you to be an expert at design (architect) 4. formal description can be used as a prototype 5. techniques themselves useful in programming and reasoning B. broader intellectual context 1. self-reproduction 2. Hilbert's program 3. Want to be able to explain and classify programming language features II. Introduction to the Lambda Calculus A. The problem: What is a function? B. Basic notion: reduction (rewriting) C. Relation to standard math notations: --------------------------- NOTATIONS FOR FUNCTIONS Mathematical notation: f(y) = 1 + y or: f operates by y |-> 1+y Church's lambda notation: (\y . (+ 1 y)) ---------------------------- D. Relation to other programming languages ------------------ Haskell: (\y -> (1 + y)) Scheme: (lambda (y) (+ 1 y)) SML: (fn y => 1 + y) Lambda Prolog: y \ (1 + y) Smalltalk: [:y | 1 + y] ------------------ 1. Names of formals just placeholders (alpha conversion) ------------- FORMALS ARE MERE PLACEHOLDERS (\ x -> (g 1 x)) == (\ y -> (g 1 y)) (\ x -> (\ x -> x)) == (\ y -> (\ x -> x)) ------------- 2. Computation by substitution, call by name III. The simply typed lambda calculus A. syntax --------------- TYPED LANGUAGE CONCRETE SYNTAX t,s in Type-Expr e in Expr x in Identifier t ::= o | t -> t | (t) e ::= x | \ x : t . e | e e | (e) --------------- -------------------- ABSTRACT SYNTAX t,s in Type-Expr e in Expr x in Identifier t ::= o | (t -> t) e ::= x | (\ x : t . e) | (e e) -------------------- 1. parsing rules ------------- PARSING RULES \x:o. e e' == (\x:o. (e e')) x y z == ((x y) z) o -> o -> o == (o -> (o -> o)) ------------- B. substitution 1. free occurrences -------------- FREE AND BOUND VARIABLES def: x occurs free in (i) x, (ii) (U V) if x occurs free in U or V, (iii) (\y:t.U) if x =/= y, and x occurs free in U. ------------- 2. free variables, Fv ---------- Fv: Expr -> (Set of Identifier) Fv(x) = {x} Fv(\x:t.e) = Fv(e) - {x} Fv(e e') = Fv(e) union Fv(e') ---------- 3. bound variables ------------- def: x is bound in (i) \x:t.U, if x in Fv(U) (ii) (\y:t.U), if x is not y and if x is bound in U (iii) (U V), if x is bound in U or in V ------------- 4. syntactic substitution ------------ SYNTACTIC SUBSTITUTION [e/x]x == e [e/x]y == y if not(y == x) [e/x](e1 e2) == ([e/x]e1) ([e/x]e2) [e/x](\x:t.e') == (\x:t.e') [e/x](\y:t.e') == (\y:t . [e/x]e') where not(y == x), and not(y in Fv(e)) ------------ C. typing rules 1. examples ---------- TYPING RULE EXAMPLES what is the type of: (\x:o . x) (\x: o -> o . x) (\y:o.y) z (\x:o . z) ---------- -------------------------- THE TYPE CHECKING PROBLEM & NOTATION H[x:->s] |- e:t [-> Intro] -------------------- H |- (\x:s.e) : s->t --------------------------- 2. type environments (contexts) what if E involves x? What if E involves some y? ------------------------ TYPE ENVIRONMENTS H \in TypeEnv = Identifier -> Type-Expr empty-type-env : TypeEnv bind : Identifier * Type-Expr -> TypeEnv overlay : TypeEnv * TypeEnv -> TypeEnv find : TypeEnv * Identifier -> Type-Expr [ :-> ] : TypeEnv * Identifier * Type-Expr -> TypeEnv empty-type-env = { } bind(I,T) = { I :-> T } find(H, I) = H(I) find(overlay(H1, H2), I) = if I in dom(H1) then H1(I) else H2(I) dom(empty-type-env) = {} dom(bind(I,T)) = {I} dom(overlay(H1, H2) = dom(H1) \union dom(H2) H[I :-> T] = overlay(bind(I,T), H) Thus find(bind(x, t), x) = t find(H[x :-> t], x) = t find(H[x :-> t], y) = find(H, y), if not(x == y) ------------------------ so what is find(overlay(bind(i,int), bind(i:real)), i)? so how do we formalize the notation for the rule above? 3. type judgements, has type relation ------------------------------------------ TYPE CHECKING AXIOMS AND RULES [var] H |- x : t if find(H,x) = t H |- e:t [add hyp] --------------- if x not in H[x:->s] |- e:t dom(H) H[x:->s] |- e:t [-> Intro] -------------------- H |- (\x:s.e) : s->t H |- e:(s->t), H |- e':s [-> Elim] ------------------------ H |- (e e') : t ------------------------------------------ D. models (can skip) 1. full type frame ---------------------- FULL TYPE FRAME MODEL meaning of a type: [[.]]: Type-Expr -> Value [[o]] = Nat [[(s -> t)]] = { f: [[s]] -> [[t]] } H-environments: (H a type context) eta in Env(H) = Identifier -> Value such that if x:t in dom(H) then eta(x:t) in [[t]] Meaning of an expression: [[.|>.:.]] : (H:TypeEnv) * Expr * Type-Expr -> Env(H) -> Value such that if H |> e:t then [[H |> e : t]](eta) in [[t]] [[H |> x : t]]eta = eta(x:t) [[H |> (e e') : t]]eta = ([[H |> e:s->t]]eta) ([[H |> e':s]]eta) [[H |> (\x:s.e) : s->t]]eta = f where f(y) = [[H[x:->s] |> e:t ]]eta' and eta' = overlay(bind(x,y), eta) -------------------- IV. quiz on the typed lambda calculus ---------------------------------- 1. Give fully parenthesized forms for the following lambda-terms. (Note that the backslash (\) is meant to represent lambda: (a) \x: o -> o -> o . x y z (b) x y \x : o -> o. x y (c) x y (z w) 2. What are the free variables of the following terms? (a) \f:o -> o.(f y) (b) (f (\f:(o->o).f y)) \z:o.z 3. What is the result of the following substitutions? (a) [w/x]((\y:o.x) w) (b) [z/y](\f:o->o.f y) (c) [z/f](\f:o->o.f y) 4. Prove the following type judgements. (a) y:o, z:o |- y:o (b) |- (\x:o.x) : o -> o (c) |- (\f:o->o . \y:o . f(f(y)) : (o->o)->o -------------------------------------- V. Untyped lambda calculus A. The language (syntax) ------------------------ UNTYPED LAMBDA CALCULUS CONCRETE SYNTAX e in Expr x in Identifier e ::= x | \x . e | e e | (e) ABSTRACT SYNTAX e in Expr x in Identifier e ::= x | (\x . e) | (e e) --------------------------- B. substitution and equational rules same as typed language C. What's different? ------------------ CHURCH'S THESIS All computable functions are definable in the (untyped) lambda calculus. ------------------- VI. quiz on the untyped lambda calculus ---------------------------------- 1. Give fully parenthesized forms for the following lambda-terms. (Note that the backslash (\) is meant to represent lambda: (a) \x.x y z (b) x y \x. x y (c) x y (z w) 2. What are the free variables of the following terms? (a) \x.(x y) (b) (x (\x.x y)) \z.z 3. What is the result of the following substitutions? (a) [z/x](\x.x y) (b) [z/y](\x.x y) (c) [w/x]((\y.x) w) -------------------------------------- VII. Equational theory of the (simply typed) lambda calculus A. equational rules for the simply typed lambda calculus ------------------- EQUATIONAL THEORY OF THE LAMBDA CALCULUS CONVERSION RULES (alpha) H |> (\x:s.U) = (\y:s.[y/x]U) : t if y not in Fv(U) and y is not bound in U (beta) H |> ((\x:s.e) e') = [e'/x]e : t (eta) H |> \x:s.e(x) = e : s->t if x not in Fv(e) ------------------- ------------------- EQUIVALENCE RULES (refl) H |> x = x : s H |> e = e' : s (sym) ------------------ H |> e' = e : s H |> e = e' : s, H |> e' = e'' : s (trans) ------------------ H |> e = e'' : s CONGRUENCE RULES H[x:->s] |> e = e' : t (xi) ------------------------------- H |> (\x:s.e) = (\x:s.e') : (s -> t) H |> e0 = e0' : (s -> t), H |> e1 = e1' : s (mu) ------------------------------ H |> (e0 e1) = (e0' e1') : t ----------------------- B. conversion rules 1. alpha, change of bound variables --------------- SYNTACTIC IDENTITY (Congruence) (\x:t.x) == (\y:t.y) def: e is congruent to e' iff they are alpha convertable. ----------------- 2. beta, application --------------------- EXAMPLES OF CONVERSION (\x.add(square(x),1)) 3 = add(square(3),1) (\x.y) z = y --------------------- 3. eta, function abstraction, extensionality --------------------- (\x.inc x) = inc --------------------- 4. convertability relation denoted =, cnv, or <=> C. equational theory 1. proofs ------------------------ PROOFS OF EQUATIONS (refl) H[x:->o] |> x = x : o (xi) ------------------------------------- H |> (\x:o . x) = (\x:o . x) : (o -> o) ------------------------ -------------------------- (lemma 2) H |> (\f:o -> o . \y:o . z f y) = z : (o -> o) -> o -> o (lemma 1) H |> (\x:o . x) = (\x:o . x) : o -> o (mu) ------------------------------------ H |> (\f:o -> o . \y:o . z f y) (\x:o . x) = z (\x:o . x) : o -> o where the proof of lemma 1 is: (refl) H[x:->o] |> x = x : o (xi) --------------------------------- H |> (\x:o . x) = (\x:o . x) : o -> o and the proof of lemma 2 is: (eta) H[f:->(o->o)] |> \y:o . z f y = z f : o->o (xi) ------------------------------------ H |> (\f:o -> o \y:o . z f y) = \f:o -> o. z f : (o -> o) -> o -> o, (eta) H |> \f: o -> o . z f = z (trans) --------------------------------- H |> (\f:o -> o . \y:o . z f y) = z : (o -> o) -> o -> o --------------------------- 2. complexity VIII. Reductions A. Operational semantics (rewrite rules) --------------- LAMBDA CALCULUS: REDUCTION def: reduction, denoted --> (or red), relates the lhs to rhs of equational rules beta and eta. Examples: (\x.y) z --> y (\x.inc x) --> inc def: a redex is a subexpression where a beta or eta-reduction can take place def: the relation -->* is the reflexive, transitive closure of --> ----------------- B. Normal form ---------------- NORMAL FORM def: a term is in (beta,eta) normal form if does not contain beta or eta redexes e.g., x, \x.x but not: (\x.y) z or (\x.y x) ------------------------- 1. Not every term has a normal form in the untyped langauge ------------------ (\x.x x) (\x.x x) ------------------ 2. Normal-order reduction strategy ----------------- REDUCTION STRATEGIES def: normal-order evaluation strategy is to always reduce the leftmost, outermost redex example: ((\b.c)((\x.x x)(\x.x x))) --> c ----------------- 3. Applicative-order reduction strategy ------------------ def: applicative-order evaluation strategy is to always reduce both operator and operand of leftmost, outermost beta redex before reducing term example: ((\b.c)((\x.x x)(\x.x x))) --> (\b.c)((\x.x x)(\x.x x)) --> ... ------------------- C. Church-rosser theorems: ------------------------- CHURCH ROSSER THEOREMS 1. If X <--> Y, then there is some Z such that X -->* Z and Y -->* Z (this property is called *confluence*) ------------------------- ------------------------- 2. If X has a normal form Y, there is a normal order reduction from X to Y. corollary: if want to find normal form, use normal order eval. ------------------------- D. Normalization, comparison of simply typed and untyped calculus ------------------------- NORMALIZATION def: a system is * weakly normalizing (or church-rosser, confluent): if only one normal form for a term * strong normalizing (terminating): if every term has a normal form -------------------------