Programming Languages and Compilers CS 421 Elsa L Gunter 2112 SC UIUC http www cs uiuc edu class sp07 cs421 Based in part on slides by Mattox Beckman as updated by Vikram Adve and Gul Agha Where Are We First four weeks Functional Programming Intro to OCAML Recursion Higher Order Functions User defined datatypes Elsa L Gunter Where 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 Grammars Elsa L Gunter Where 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 Programming Language Semantics And some more Elsa L Gunter Lambda Calculus Motivation Aim is to capture the essence of functions function applications and evaluation calculus is a theory of computation The Lambda Calculus Its Syntax and Semantics H P Barendregt North Holland 1984 Elsa L Gunter Lambda 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 untyped Elsa L Gunter Untyped Calculus Only three kinds of expressions Variables x y z w Abstraction x e Function creation think fun x e Application e1 e2 Elsa L Gunter Untyped Calculus Grammar Formal BNF Grammar expression variable abstraction application expression abstraction variable expression application expression expression Elsa L Gunter Untyped 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 term Elsa L Gunter Example Label occurrences and scope x y y x x y x Elsa L Gunter Untyped 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 capture Elsa L Gunter How 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 sugar Elsa L Gunter Typed 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 Gunter Uses 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 exp let x e1 in e2 x e2 e1 Elsa L Gunter Conversion conversion x exp y exp y x Provided that 1 y is not free in exp 2 No free occurrence of x in exp becomes bound in exp when replaced by y Elsa L Gunter Conversion Non Examples 1 y is not free in exp x x y y y y 2 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 y And y y y y x y y x Elsa L Gunter Congruence 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 e2 Elsa L Gunter Equivalence equivalence is the smallest congruence containing conversion One usually treats equivalent terms as equal i e use equivalence classes of terms Elsa L Gunter Example Show 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 y Elsa 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 y Elsa L Gunter Substitution 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 N Elsa L Gunter Substitution 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 necessary Elsa L Gunter Example 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 Gunter Example 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 lambda calculus Usually defined on equivalence classes of terms Elsa L Gunter Example 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 x x x x x x x x x x Elsa L Gunter Equivalence equivalence is the smallest congruence containing equivalence and reduction A term is in normal form if no subterm is equivalent to a term that can be reduced Hard fact Church Rosser if e 1 and e2 are equivalent and both are normal forms then they are equivalent Elsa L Gunter Order of Evaluation Not all terms reduce to normal forms Not all reduction strategies will produce a normal form if one exists Elsa L Gunter Lazy evaluation Always reduce the left most application in a top most series of applications i e Do not perform reduction inside an abstraction Stop when left most application is not an application of an abstraction to a term Elsa L Gunter Example 1 z x x y y y y y y Lazy evaluation Reduce the left most application z x x y y y y y y x x …
View Full Document
Unlocking...