Programming Languages and Compilers (CS 421)Where Are We?Where Are We?After MidtermLambda Calculus - MotivationSlide 6Untyped -CalculusUntyped -Calculus GrammarUntyped -Calculus TerminologyExampleSlide 11How Powerful is the Untyped -Calculus?Typed vs Untyped -CalculusUses of -Calculus Conversion Conversion Non-ExamplesCongruence EquivalenceSlide 19 (Eta) ReductionSubstitutionSlide 22Slide 23Slide 24 reductionSlide 26 EquivalenceOrder of EvaluationLazy evaluation:Example 1Eager evaluationSlide 32Example 2Slide 34Slide 35Slide 36Slide 37Slide 38Slide 39Slide 40Slide 41Slide 42Slide 43Slide 44Slide 45Programming Languages and Compilers (CS 421)Elsa L Gunter2112 SC, UIUChttp://www.cs.uiuc.edu/class/fa06/cs421/Presented by Baris Aktemur and Chris OsbornBased in part on slides by Mattox Beckman, as updated by Vikram Adve and Gul Agha, and on slides by Grigore RosuElsa L. GunterWhere Are We? •First four weeks–Functional Programming•Intro to OCAML•Recursion•Higher-Order Functions•User defined datatypesElsa L. GunterWhere Are We?•Next three weeks–Foundations of Programming•Types and Type Systems•Lambda Calculus•Later in course•Natural Semantics•Transition SemanticsElsa L. GunterAfter Midterm•Language Syntax and Parsing–DFAs and NDFAS–Grammars–First and Follow Sets–LL Grammars–LR Grammars•Interpreters - Implementing Programming Language Semantics•And some more …Elsa L. GunterLambda Calculus - Motivation•Aim is to capture the essence of functions and function applications•calculus is a theory of computation•“The Lambda Calculus: Its Syntax and Semantics”. H. P. Barendregt. North Holland, 1984Elsa L. GunterLambda Calculus - Motivation•All sequential programs may be viewed as functions from input (initial state and input values) to output (resulting state and output values).•-calculus is a mathematical formalism of 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 -Calculus Terminology•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 in e not in a subterm of the form x. e’ (same x)•Free variables: all variables having free occurrences 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 avoid free variable captureElsa L. GunterHow Powerful is the Untyped -Calculus?•The untyped -calculus is Turing Complete–Can express any sequential computation•Problems: –How to express basic data: booleans, integers, etc?–How to express recursion?–Constants, if_then_else, etc, are conveniences; can be added as syntactic sugarElsa L. GunterTyped vs Untyped -Calculus•The pure -calculus has no notion of type: (f f) is a legal expression•Types restrict which applications are valid•Types are not syntactic sugar! They disallow some terms•Simply typed -calculus is less powerful than the untyped -Calculus: NOT Turing Complete (no recursion)Elsa L. GunterUses of -Calculus•Typed and untyped -calculus used for theoretical study of sequential programming languages•Sequential programming languages are essentially the -calculus, extended with predefined 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 exp becomes bound in exp when replaced by yElsa L. Gunter Conversion Non-Examples1. y is not free in exp x. x y ----> y. y y2. No free occurrence of x becomes bound 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 smallest congruence containing conversion•One usually treats -equivalent terms 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 of terms•[N / x] P means replace every free occurrence of x in P by N•Provided that no variable free in P becomes bound in [N / x] P–Rename bound variables in P to avoid capturing 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
View Full Document
Unlocking...