CMSC 330: Organization of Programming Languages Lambda Calculus and Types CMSC 330 2 Introduction •! We’ve seen that several language conveniences aren’t strictly necessary –! Multi-argument functions (use currying or tuples) let fst (x,y) = x let fst x y = x let fst p = let fst x = match p with fun y -> x (x,y) -> x CMSC 330 3 Introduction –! Loops (use recursion) –! Side-effects r = 0; let rec sum i r = for (i = 0; i < n; i++) { if i >= n then r r += i; else sum (i+1) (r+i) } in sum 0 0 CMSC 330 4 IntroductionCMSC 330 5 Lambda Calculus Syntax •! A lambda calculus expression is defined as e ::= x variable | !x.e function | e e function application •! !x.e is like (fun x -> e) in OCaml •! That’s it! All there is is higher-order functions CMSC 330 6 Conventions •! The scope of ! extends as far to the right as possible !x. !y.x y is !x.(!y.(x y)) •! Function application is left-associative x y z is (x y) z –! Same rule as OCaml CMSC 330 7 Operational Semantics •! All we’ve got are functions, so all we can do is call them •! To evaluate (!x.e1) e2 –! Evaluate e1 with x bound to e2 •! e1[x/e2] is e1 where occurrences of x are replaced by e2 •! Slightly different than the environments we saw for Ocaml –! apply a substitution instead of carry an environment •! We allow reductions to occur anywhere in a term An interpreter in “math” CMSC 330 8 Examples •! (!x.x) z " •! (!x.y) z " •! (!x.x y) z " –! A function that applies its argument to y •! (!x.x y) (!z.z) " •! (!x.!y.x y) z " –! A curried function of two arguments that applies its first argument to its second •! (!x.!y.x y) (!z.zz) x " z y (!z.z) y " y zy !y.z y !y.((!z.zz)y)x " (!z.zz)x " xxCMSC 330 9 Syntactic sugar for local declarations let x = e1 in e2 can be written as (!x.e2) e1 CMSC 330 10 Static Scoping and Alpha Conversion •! Lambda calculus uses static scoping •! Consider the following –! (!x.x (!x.x)) z " ? •! The rightmost “x” refers to the second binding –! This is a function that takes its argument and applies it to the identity function •! This function is “the same” as (!x.x (!y.y)) –! Renaming bound variables consistently is allowed CMSC 330 11 Static Scoping (cont’d) •! How about the following? –! (!x.!y.x y) y " ? –! When we replace y inside, we don’t want it to be “captured” by the inner binding of y •! This function is “the same” as (!x.!z.x z) CMSC 330 12 Beta-Reduction, Again •! Whenever we do a step of beta reduction... –! (!x.e1) e2 " e1[x/e2] –! ...alpha-convert variables as necessary •! Examples: –! (!x.x (!x.x)) z = (!x.x (!y.y)) z " z (!y.y) –! (!x.!y.x y) y = (!x.!z.x z) y " !z.y zCMSC 330 13 Encodings •! It turns out that this language is Turing complete •! That means we can encode any computation we want in it –! ...if we’re sufficiently clever... CMSC 330 14 Booleans The lambda calculus was created by logician Alonzo Church in the 1930's to formulate a mathematical logical system true = !x.!y.x false = !x.!y.y if a then b else c = a b c (the ! expression) •! Examples: –! if true then b else c " (!x.!y.x) b c " (!y.b) c " b –! if false then b else c " (!x.!y.y) b c " (!y.y) c " c CMSC 330 15 Booleans (continued) Other Boolean operations: •! not = !x.((x false) true) •! not true " !x.((x false) true) true " ((true false) true) " false •! and = !x.!y.((xy) false) •! or = !x.!y.((x true) y) •! Show not, and and or have the desired properties, … •! Given these operations, can build up a logical inference system CMSC 330 16 Pairs (a,b) = !x.if x then a else b fst = !f.f true snd = !f.f false •! Examples: –! fst (a,b) = (!f.f true) (!x.if x then a else b) " (!x.if x then a else b) true " if true then a else b " a –! snd (a,b) = (!f.f false) (!x.if x then a else b) " (!x.if x then a else b) false " if false then a else b " bCMSC 330 17 Natural Numbers (Church*) 0 = !f.!y.y 1 = !f.!y.f y 2 = !f.!y.f (f y) 3 = !f.!y.f (f (f y)) i.e., n = !f.!y.<apply f n times to y> succ = !z.!f.!y.f (z f y) iszero = !g.g (!y.false) true –! Recall that this is equivalent to !g.((g (!y.false)) true) *(Named after Alonzo Church, developer of lambda calculus) CMSC 330 18 Natural Numbers (cont’d) •! Examples: succ 0 = (!z.!f.!y.f (z f y)) (!f.!y.y) " !f.!y.f ((!f.!y.y) f y) " !f.!y.f y = 1 iszero 0 = (!z.z (!y.false) true) (!f.!y.y) " (!f.!y.y) (!y.false) true " (!y.y) true " true CMSC 330 19 Arithmetic defined •! Addition, if M and N are integers (as ! expressions): M + N = !x.!y.(M x)((N x) y) Equivalently: + = !M.!N.!x.!y.(M x)((N x) y) •! Multiplication: M * N = !x.(M (N x)) •! Prove 1+1 = 2. 1+1 = !x.!y.(1 x)((1 x) y) " !x.!y.((!x.!y.x y) x)(((!x.!y.x y) x) y) " !x.!y.(!y.x y)(((!x.!y.x y) x) y) " !x.!y.(!y.x y)((!y.x y) y) " !x.!y.x ((!y.x y) y) " !x.!y.x (x y) = 2 •! With these definitions, can build a theory of integer arithmetic. What else? •! What about looping or recursion? let rec fact n = if n = 0 then 1 else n * fact (n-1) CMSC 330 20CMSC 330 21 Looping •! Define D = !x.x x •! Then –! D D = (!x.x x) (!x.x x) " (!x.x x) (!x.x x) = D D •! So D D is an infinite loop –! In general, self application is how we get looping CMSC 330 22 The “Paradoxical” Combinator Y = !f.(!x.f (x x)) (!x.f (x x)) •! Then Y F = (!f.(!x.f (x x)) (!x.f (x x))) F " (!x.F (x x)) (!x.F (x x)) " F ((!x.F (x x)) (!x.F (x x))) = F (Y F) •! Thus Y F = F (Y F) = F (F (Y F)) = ... CMSC 330 23 Example fact = !f. !n.if n = 0 then 1 else n * (f (n-1)) –! The second argument to fact is the integer –! The first argument is the function to call in the body •! We’ll use Y to make this recursively call fact (Y fact) 1 = (fact (Y fact)) 1 " if 1 = 0 then 1 else 1 * ((Y fact) 0) " 1 * ((Y fact) 0) " 1 * (fact (Y fact) 0) " 1 * (if 0 = 0 then 1 else 0 * ((Y fact) (-1)) " 1 * 1 " 1 CMSC 330 24 Discussion •! …
View Full Document
Unlocking...