Programming Languages andCompilers (CS 421)Elsa L Gunter2112 SC, UIUChttp://www.cs.uiuc.edu/class/fa05/cs421/current/Based in part on slides by Mattox Beckman, as updatedby Vikram Adve and Gul AghaElsa L. GunterWhere Are We?• First four weeks–Functional Programming• Intro to OCAML• Recursion• Higher-Order Functions• User defined datatypesElsa L. GunterWhere Are We?• Types and Type Systems– Unification– Type Derivation and Inference• Language Syntax and Parsing– DFAs and NDFAS, Lexing– Grammars– First and Follow Sets– LL Grammars– LR GrammarsElsa L. GunterWhere Are We Going?• Next three weeks– Lambda Calculus– Evaluation– Modeling Programs in Lambda Calculus(Denotational Semantics)• Later in course– Natural Semantics– Transition Semantics• Interpreters - Implementing ProgrammingLanguage Semantics• And some more …Elsa L. GunterLambda Calculus - Motivation• Aim is to capture the essence offunctions, function applications, andevaluation∀λ−calculus is a theory of computation• “The Lambda Calculus: Its Syntax andSemantics”. H. P. Barendregt. NorthHolland, 1984Elsa L. GunterLambda Calculus - Motivation• All sequential programs may be viewedas functions from input (initial state andinput values) to output (resulting stateand output values).∀λ-calculus is a mathematical formalismof functions and functional computations• Two flavors: typed and untypedElsa L. GunterUntyped λ-Calculus• Only three kinds of expressions:–Variables: x, y, z, w, …–Abstraction: λ x. e (Function creation, think fun x -> e)–Application: e1 e2Elsa L. GunterUntyped λ-Calculus Grammar• Formal BNF Grammar:– <expression> → <variable> | <abstraction> | <application> | (<expression>)– <abstraction> → λ <variable> .<expression>– <application> → <expression> <expression>Elsa L. GunterUntyped λ-CalculusTerminology• Occurrence: a location of a subterm in a term• Variable binding: λ x. e is a binding of x in e• Bound occurrence: all occurrences of x inλ x. e• Free occurrence: one that is not bound• Scope of binding: in λ x. e, all occurrences ine not in a subterm of the form λ x. e’ (samex)• Free variables: all variables having freeoccurrences in a termElsa L. GunterExample• Label occurrences and scope:(λ x. λ y. y (λ x. x y)) xElsa L. GunterUntyped λ-Calculus• How do you compute with the λ-calculus?• Roughly speaking, by substitution:• (λ x. e1) e2 ⇒* e1 [e2 / x]• * Modulo all kinds of subtleties to avoidfree variable captureElsa L. GunterHow Powerful is the Untypedλ-Calculus?• The untyped λ-calculus is TuringComplete– Can express any sequential computation• Problems:– How to express basic data: booleans,integers, etc?– How to express recursion?– Constants, if_then_else, etc, areconveniences; can be added as syntacticsugarElsa L. GunterTyped vs Untyped λ-Calculus• The pure λ-calculus has no notion oftype: (f f) is a legal expression• Types restrict which applications arevalid• Types are not syntactic sugar! Theydisallow some terms• Simply typed λ-calculus is less powerfulthan the untyped λ-Calculus: NOTTuring Complete (no recursion)Elsa L. GunterUses of λ-Calculus• Typed and untyped λ-calculus used fortheoretical study of sequentialprogramming languages• Sequential programming languages areessentially the λ-calculus, extended withpredefined constructs, constants, types,and syntactic sugar• Ocaml is close to the λ-Calculus: fun x -> exp --> λ x. explet x = e1 in e2 --> (λ x. e2)e1Elsa L. Gunterα Conversion• α-conversion:λ x. exp --α--> λ y. (exp [y/x])• Provided that1. y is not free in exp2. No free occurrence of x in expbecomes bound in exp whenreplaced by yElsa L. Gunterα Conversion Non-Examples1. y is not free in exp λ x. x y --α--> λ y. y y2. No free occurrence of x becomesbound when replaced by x λ x. λ y. x y --α--> λ y. λ y. y y exp exp[y/x]But λ x. (λ y. y) x --α--> λ y. (λ y. y) yAnd λ y. (λ y. y) y --α--> λ x. (λ y. y) xElsa L. GunterCongruence• Let ~ be a relation on lambda terms. ~is a congruence if• it is an equivalence relation• If e1 ~ e2 then– (e e1) ~ (e e2) and (e1e) ~ (e2 e)– λ x. e1 ~ λ x. e2Elsa L. Gunter α Equivalence• α equivalence is the smallestcongruence containing αconversion• One usually treats α-equivalentterms as equal - i.e. use αequivalence classes of termsElsa L. GunterExampleShow: λ x. (λ y. y x) x ~α~ λ y. (λ x. x y) y∀λ x. (λ y. y x) x --α--> λ z. (λ y. y z) z soλ x. (λ y. y x) x ~α~ λ z. (λ y. y z) z• (λ y. y z) --α--> (λ x. x z) soλ z. (λ y. y z) z ~α~ λ z. (λ x. x z) z∀λ z. (λ x. x z) z --α--> λ y. (λ x. x y) y soλ z. (λ x. x z) z ~α~ λ y. (λ x. x y) y∀λ x. (λ y. y x) x ~α~ λ y. (λ x. x y) yElsa L. Gunter η (Eta) Reduction• η Rule: λ x. f x --η--> f if x not free in f– Can be useful in each direction– Not valid in Ocaml• recall lambda-lifting and side effects– Not equivalent to (λ x. f) x --> f (inst of β)• Example: λ x. (λ y. y) x --η--> λ y. yElsa L. GunterSubstitution• Defined on α-equivalence classes ofterms• [N / x] P means replace every freeoccurrence of x in P by N• Provided that no variable free in Pbecomes bound in [N / x] P– Rename bound variables in P to avoidcapturing free variables of NElsa L. GunterSubstitution• [N / x] x = N• [N / x] y = y if y ≠ x• [N / x] (e1 e2) = (([N / x] e1) ([N / x] e2))• [N / x] (λ x. e) = (λ x. e)• [N / x] (λ y. e) = λ y. ([N / x] e)provided y ≠ x and y not free in N–Rename y if necessaryElsa L. GunterExample[(λ x. x y) / z] (λ y. y z) = ?• Problems?– z in redex in scope of y binding– y free in the residue• [(λ x. x y) / z] (λ y. y z) --α-->[(λ x. x y) / z] (λ w.w z) = λw. w (λ x. x y)Elsa L. GunterExample• Only replace free occurrences• [(λ x. x) / z] (λ y. y z (λ z. z)) =λ y. y (λ x. x) (λ z. z)Notλ y. y (λ x. x) (λ z. (λ x. x))Elsa L. Gunter β reduction• β Rule: (λ x. P) N --β--> [N /x] P• Essence of computation in the lambdacalculus• Usually defined on α-equivalenceclasses of termsElsa L. GunterExample• (λ z. (λ x. x y) z) (λ y. y z) --β--> (λ x. x y) (λ y. y z) --β--> (λ y. y z) y --β--> y z• (λ x. x x) (λ x. x x) --β--> (λ x. x
View Full Document