CMSC 330: Organization of Programming Languages Lambda Calculus CMSC 330 - Spring 2011 1CMSC 330 - Spring 2011 2 Programming Language Features ! Many features exist simply for convenience • Multi-argument functions foo ( a, b, c ) Use currying or tuples • Loops while (a < b) … Use recursion • Side effects a := 1 Use functional programming ! So what language features are really needed?CMSC 330 - Spring 2011 3 Turing Completeness ! Computational system that can • Simulate a Turing machine • Compute every Turing-computable function ! A programming language is Turing complete if • It can map every Turing machine to a program • A program can be written to emulate a Turing machine • It is a superset of a known Turing-complete language ! Most powerful programming language possible • Since Turing machine is most powerful automatonCMSC 330 - Spring 2011 4 Programming Language Theory ! Come up with a “core” language • Thatʼs as small as possible • But still Turing complete ! Helps illustrate important • Language features • Algorithms ! One solution • Lambda calculusCMSC 330 - Spring 2011 5 Lambda Calculus (λ-calculus) ! Proposed in 1930s by • Alonzo Church (born in Washingon DC!) ! Formal system • Designed to investigate functions & recursion • For exploration of foundations of mathematics ! Now used as • Tool for investigating computability • Basis of functional programming languages Lisp, Scheme, ML, OCaml, Haskell…CMSC 330 - Spring 2011 6 Lambda Expressions ! 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! Nothing but higher-order functionsCMSC 330 - Spring 2011 7 Three Conveniences ! Syntactic sugar for local declarations • let x = e1 in e2 is short for (λx.e2) e1 ! Scope of λ extends as far right as possible • Subject to scope delimited by parentheses • λx. λy.x y is same as λx.(λy.(x y)) ! Function application is left-associative • x y z is (x y) z • Same rule as OCamlCMSC 330 - Spring 2011 8 Lambda Calculus Semantics ! All weʼve got are functions • So all we can do is call them ! To evaluate (λx.e1) e2 • Evaluate e1 with x replaced by e2 ! This application is called beta-reduction • (λx.e1) e2 → e1[x:=e2] e1[x:=e2] is e1 with occurrences of x replaced by e2 This operation is called substitution Slightly different than the environments we saw for Ocaml • Do syntactic substitutions to replace formals with actuals • Instead of using environment to map formals to actuals • We allow reductions to occur anywhere in a termCMSC 330 - Spring 2011 9 Beta Reduction Example ! (λx.λz.x z) y → (λx.(λz.(x z))) y // since λ extends to right → (λx.(λz.(x z))) y // apply (λx.e1) e2 → e1[x:=e2] // where e1 = λz.(x z), e2 = y → λz.(y z) // final result ! Equivalent OCaml code • (fun x -> (fun z -> (x z))) y → fun z -> (y z) Parameters • Formal • ActualCMSC 330 - Spring 2011 10 Lambda Calculus Examples ! (λx.x) z → ! (λx.y) z → ! (λx.x y) z → • A function that applies its argument to y z y z yCMSC 330 - Spring 2011 11 Lambda Calculus Examples (cont.) ! (λx.x y) (λz.z) → ! (λx.λy.x y) z → • A curried function of two arguments • Applies its first argument to its second ! (λx.λy.x y) (λz.zz) x → (λz.z) y → y λy.z y (λy.(λz.zz)y)x → (λz.zz)x → xxDefining Substitution ! Use recursion on structure of terms! • x[x:=e]= e // Replace x by e • y[x:=e]= y // y is different than x, so no effect • (e1 e2)[x:=e]= (e1[x:=e])(e2[x:=e]) // Substitute both parts of application • (λx.eʼ)[x:=e]=λx.eʼ Inλx.eʼ,thexisaparameter,andthusalocalvariablethatisdifferentfromotherxʼs. Sothesubstitutionhasnoeffectinthiscase,sincethexbeingsubstitutedforisdifferentfromtheparameterxthatisineʼ!• (λy.eʼ)[x:=e]=? Theparameterydoesnotsharethesamenameasx,thevariablebeingsubstitutedfor Isλy.(eʼ[x:=e])correct?CMSC 330 - Spring 2011 12CMSC 330 - Spring 2011 13 Static Scoping & 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 • Ex. λx.x = λy.y = λz.z λy.λx.y = λz.λx.zCMSC 330 - Spring 2011 14 Static Scoping (cont.) ! 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, as this violates static scoping • I.e., (λx.λy.x y) y ≠ λy.y y ! Solution • (λx.λy.x y) is “the same” as (λx.λz.x z) Due to alpha conversion • So change (λx.λy.x y) y to (λx.λz.x z) y first Now (λx.λz.x z) y → λz.y zCompleting the Definition of Substitution ! Recall: we need to define (λy.eʼ)[x:=e] • We want to avoid capturing (free) occurrences of y in e • Solution: alpha-conversion! Change y to a variable w that does not appear in eʼ or e. (Such a w is called fresh.) Replace all occurrences of y in eʼ by w. Then replace all occurrences of x in eʼ by e! ! Formally: (λy.eʼ)[x:=e] = λw.((eʼ[y:=w])[x:=e])(wisfresh) CMSC 330 - Spring 2011 15CMSC 330 - Spring 2011 16 Beta-Reduction, Again ! Whenever we do a step of beta reduction • (λx.e1) e2 → e1[x:=e2] • We must alpha-convert variables as necessary • Usually performed implicitly (w/o showing conversion) ! Examples • (λx.λy.x y) y = (λx.λz.x z) y → λz.y z // y → z • (λx.x (λx.x)) z = (λy.y (λx.x)) z
View Full Document
Unlocking...