DOC PREVIEW
U of I CS 421 - Programming Languages and Compilers

This preview shows page 1-2-3-21-22-23-43-44-45 out of 45 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 45 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 45 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 45 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 45 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 45 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 45 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 45 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 45 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 45 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 45 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

Programming 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 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 lambda calculus•Usually defined on α-equivalence classes 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 x) (λ x. x x) --β--> (λ x. x x) (λ x. x x) --β--> ….Elsa L. Gunter α β


View Full Document

U of I CS 421 - Programming Languages and Compilers

Documents in this Course
Lecture 2

Lecture 2

12 pages

Exams

Exams

20 pages

Lecture

Lecture

32 pages

Lecture

Lecture

21 pages

Lecture

Lecture

15 pages

Lecture

Lecture

4 pages

Lecture

Lecture

68 pages

Lecture

Lecture

68 pages

Lecture

Lecture

84 pages

s

s

32 pages

Parsing

Parsing

52 pages

Lecture 2

Lecture 2

45 pages

Midterm

Midterm

13 pages

LECTURE

LECTURE

10 pages

Lecture

Lecture

5 pages

Lecture

Lecture

39 pages

Load more
Download Programming Languages and Compilers
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Programming Languages and Compilers and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Programming Languages and Compilers 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?