OutlineCourse PreviewObjectivesλ-CalculusComputational ModelData RepresentationCS421 Lecture 8: λ-Calculus1Mark [email protected] of Illinois at Urbana-ChampaignJune 15, 20061Based on slides by Mattox Beckman, as updated by Vikram Adve, GulAgha, and Elsa GunterMark Hills CS421 Lecture 8: λ-CalculusOutlineCourse PreviewObjectivesλ-CalculusComputational ModelData RepresentationCourse PreviewObjectivesλ-CalculusComputational ModelData RepresentationMark Hills CS421 Lecture 8: λ-CalculusOutlineCourse PreviewObjectivesλ-CalculusComputational ModelData RepresentationA Preview of Where We Are Going - 1 of 3◮Functional Programming◮Intro to OCaml◮Recursion◮Higher-Order Functions◮Foundations of Programming Languages◮Types and Type Systems◮Lambda Calculus◮Natural Semantics◮Transition Semantics and the Church-Rosser TheoremMark Hills CS421 Lecture 8: λ-CalculusOutlineCourse PreviewObjectivesλ-CalculusComputational ModelData RepresentationPreview - 2 of 3◮Language Syntax and Parsing◮DFAs and NFAs◮Grammars◮First and Follow Sets◮LL Grammars◮LR Grammars◮Interpreters – Implementing Programming Language SemanticsMark Hills CS421 Lecture 8: λ-CalculusOutlineCourse PreviewObjectivesλ-CalculusComputational ModelData RepresentationPreview - 3 of 3◮Language Features for Organizing Data◮Variables and Binding◮Language Support for Data Abstraction◮Object-Oriented Programming◮Language Features for Organizing Control◮Logic Programming◮Control Flow Basics: Structured, Unstructured, and Exceptions◮Concurrency◮Continuations and Continuation-Passing Style (CPS)◮Function Calls and Parameter PassingMark Hills CS421 Lecture 8: λ-CalculusOutlineCourse PreviewObjectivesλ-CalculusComputational ModelData RepresentationObjectivesSubtitle: “Everything is Really a Function”This lecture introduces λ-calculus, and uses it to show howfunctions can represent arbitrary computations and data structures.After this lecture you should . . .◮Know the three constructs of λ-calculus.◮Know the terminology: free vs. bound variables, scopes,α-reduction, β-reduction◮Know how to use λ terms to represent arbitrary typ es.◮numbers, booleans, pairs, etcMark Hills CS421 Lecture 8: λ-CalculusOutlineCourse PreviewObjectivesλ-CalculusComputational ModelData RepresentationMotivationSyntax of λ-CalculusTerminologyFeatures and FactsThe λ-Calculus: MotivationAll sequential programs may be viewed as functions from input(initial state and input values) to output (resulting state andoutput values).◮The λ-calculus is a mathematical formalism of functions andfunctional computations◮Provides a simple, flexible model to represent programminglanguages◮Heavily used in languages research, and highly influential infunctional programmingMark Hills CS421 Lecture 8: λ-CalculusOutlineCourse PreviewObjectivesλ-CalculusComputational ModelData RepresentationMotivationSyntax of λ-CalculusTerminologyFeatures and FactsThe λ-Calculusλ-calculus : A language with only three ki nds of expressions(called terms):Variables: e → xAbstraction: e → λx.e1i.e., Function creationApplication: e → (e1e2)Mark Hills CS421 Lecture 8: λ-CalculusOutlineCourse PreviewObjectivesλ-CalculusComputational ModelData RepresentationMotivationSyntax of λ-CalculusTerminologyFeatures and FactsTerminologyOccurrence : A l ocation of a subterm in a termBound variable : Variable x is said to be bound in λx.e.Scope : The scope of this binding is all of e exce pt anyterms within e that are of the form λx.e1.Bound occurrence : An occurrence of x in e is a bound occurrenceif it is within the scope of some binding for x.Free occurrence : Otherwise, an occurrence is said to be a freeoccurrence (aka free variable)Mark Hills CS421 Lecture 8: λ-CalculusOutlineCourse PreviewObjectivesλ-CalculusComputational ModelData RepresentationMotivationSyntax of λ-CalculusTerminologyFeatures and FactsHow powerful is the λ-Calculus?Computing Power: .◮The language is Turing Complete – we canexpress any sequential computation◮“We don’t need no stinking integers!” – how dowe represent basic data?◮How do we represent recursion?◮Constants, if-expressions, etc. are conveniencesto make programming easier.a.k.a., “syntactic sugar”Mark Hills CS421 Lecture 8: λ-CalculusOutlineCourse PreviewObjectivesλ-CalculusComputational ModelData RepresentationMotivationSyntax of λ-CalculusTerminologyFeatures and FactsHow powerful is the λ-Calculus?Typed vs. Untyped Lambda Calculus .◮Lambda Calculus has no notion of type.E.g., (ff ) is a legal expression for any f !◮Types restrict what functions can be applied towhat arguments◮Types are not just syntactic sugar: some termsare illegal in the typed calculus◮The simply typed λ-calculus is less powerfulthan the untyped λ-calculus – it is NOT Turingcomplete, since it lacks recursionMark Hills CS421 Lecture 8: λ-CalculusOutlineCourse PreviewObjectivesλ-CalculusComputational ModelData RepresentationMotivationSyntax of λ-CalculusTerminologyFeatures and Factsλ-Calculus in the Real World◮The typed and untyped λ-Calculi enable the theoretical studyof sequential programming languages.◮A functional language is essentially the λ-Calculus extendedwith predefined constants, syntactic constructs, and types.E.g., Lisp, Scheme, functional subsets of ML and OCAML◮We can (mostly) express the λ-Calculus in OCaml:λx.x = fun x -> xMark Hills CS421 Lecture 8: λ-CalculusOutlineCourse PreviewObjectivesλ-CalculusComputational ModelData RepresentationTerminologyCongruenceα Conversionα Equivalenceη ReductionSubstitutionβ Reductionα β EquivalenceEvaluation OrderComputing with the λ-CalculusHow do we “execute” programs in the λ-calculus? We need somemethod to systematically process λ terms to get some kind of“result”. This requires reduction, or evaluation, methods. We alsoneed some way to tell when terms are equivalent. Finally, we needsome notion of terms that are “answers”, so we know when to stopcomputing.Mark Hills CS421 Lecture 8: λ-CalculusOutlineCourse PreviewObjectivesλ-CalculusComputational ModelData RepresentationTerminologyCongruenceα Conversionα Equivalenceη ReductionSubstitutionβ Reductionα β EquivalenceEvaluation OrderCongruenceLet ∼ be a relation on lambda terms. ∼ is a congruence if◮it is an equivalence relation◮e1∼ e2implies that (e e1) ∼ (e e2) and (e1e) ∼ (e2e) andλx.e1∼ λx.e2Mark
View Full Document
Unlocking...