1CMSC 330: Organization of Programming LanguagesLambda Calculus IntroductionCMSC 330 2Introduction• We’ve seen that several language conveniences aren’t strictly necessary– Multi-argument functions: use currying or tuples– Loops: use recursion– Side-effects: we don't need them either• Goal: come up with a “core” language that’s as small as possible and still Turing complete– This will give a way of illustrating important language features and algorithms2CMSC 330 3Revised Rule for Application• To apply something to an argument:– Evaluate it to produce a closure– Evaluate the argument (call-by-value)– Evaluate the body of the closure, in• The current environment, extended with the closure’s environment, extended with the binding for the parameterA; (E1E2) A; E1 (A', x.E)A, A', x:v; E v'A; E2 vv'CMSC 330 4Example•; (fun x = (fun y = + x y)) 3 •; (fun x = (fun y = + x y)) (x:3, y.(+ x y))•; 3 3(•, x.(fun y = + x y))x:3; (fun y = + x y) (x:3, y.(+ x y))3CMSC 330 5Lambda Calculus• A lambda calculus expression is defined ase ::= x variable| x.e function| e e function application• x.e is like (fun x -> e) in OCaml• That’s it! Only higher-order functionsCMSC 330 6Intuitive Understanding• Before we work more with the mathematical notation of lambda calculus, we’re going to play a puzzle game!• From: http://worrydream.com/AlligatorEggs/4CMSC 330 7Puzzle Pieces• Hungry alligators: eat and guard family• Old alligators: guard family• Eggs: hatch into new familyCMSC 330 8Example Families• Families are shown in columns• Alligators guard families below them5CMSC 330 9Puzzle Rule 1: The Eating Rule• If families are side-by-side the top left alligator eats the entire family to her right• The top left alligator dies• Any eggs she was guarding of the same color hatch into what she just ateCMSC 330 10Eating Rule Practice• What happens to these alligators?Puzzle 1: Puzzle 2:Answer 1: Answer 2:6CMSC 330 11Puzzle Rule 2: The Color Rule• If an alligator is about to eat a family and a color appears in both families then we need to change that color in one of the families.• If a color appears in both families, but only as an egg, no color change is made.CMSC 330 12Puzzle Rule 3: The Old Alligator Rule• When an old alligator is only guarding one family it dies.7CMSC 330 13Challenging Puzzles!• Try to reduce these groups of alligators as much as possible using the three puzzle rules:• Challenge your neighbors with puzzles of your own.CMSC 330 14More Puzzles• When Family Not eats Family True it becomes Family False and when Not eats False it becomes True… what color should the white eggs be?• What do the AND and OR families look like?8CMSC 330 15Lambda Calculus• A lambda calculus expression is defined ase ::= x variable (e: egg)| x.e function (x: alligator)| e e function application(adjacency of families)• x.e is like (fun x -> e) in OCaml• That’s it! Only higher-order functionsCMSC 330 16Three Conveniences• Syntactic sugar for local declarations– let x = e1 in e2 is short for (x.e2) e1• 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 zis (x y) z– Same rule as OCaml9CMSC 330 17Operational 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• This application is called “beta-reduction”–(x.e1) e2 e1[x/e2] (the eating rule)• e1[x/e2] is e1 where occurrences of x are replaced by e2• Slightly different than the environments we saw for Ocaml– Do substitutions to replace formals with actuals, instead of carrying around environment that maps formals to actuals– We allow reductions to occur anywhere in a termCMSC 330 18Examples (try with alligators too)•(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 zy(z.z) y yzyy.z yy.((z.zz)y)x (z.zz)x xx10CMSC 330 19Static 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• This is called alpha-renaming or alpha conversion (color rule)–Ex. x.x = y.y = z.z y.x.y = z.x.zCMSC 330 20Static 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
View Full Document
Unlocking...