DOC PREVIEW
U of I CS 421 - Lecture notes

This preview shows page 1-2-3 out of 8 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 8 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 8 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 8 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 8 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

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

U of I CS 421 - Lecture notes

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 Lecture notes
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 Lecture notes 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 Lecture notes 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?