Lecture Notes on the Lambda Calculus Peter Selinger DDaihouremde Abstract Topics de the lambda caleulutheCurry-Howrd isomorism. Contents 1 Introduction 4 1.1 Extensional vs.intensional view of functions 1.2 The lambda calculus 6 1.3 Untyped vs.typed lambda-calculi 7 1.4 Lambda calculus and computability............. 1.5 Connections to computer science..................9 1.6 Connections to logic 9 1.7 Connections to mathematics....................10 2 The untyped lambda calculus 2.1 Syntax
Lecture Notes on the Lambda Calculus Peter Selinger Department of Mathematics and Statistics Dalhousie University, Halifax, Canada Abstract This is a set of lecture notes that developed out of courses on the lambda calculus that I taught at the University of Ottawa in 2001 and at Dalhousie University in 2007. Topics covered in these notes include the untyped lambda calculus, the Church-Rosser theorem, combinatory algebras, the simply-typed lambda calculus, the Curry-Howard isomorphism, weak and strong normalization, type inference, denotational semantics, complete partial orders, and the language PCF. Contents 1 Introduction 4 1.1 Extensional vs. intensional view of functions . . . . . . . . . . . 4 1.2 The lambda calculus . . . . . . . . . . . . . . . . . . . . . . . . 6 1.3 Untyped vs. typed lambda-calculi . . . . . . . . . . . . . . . . . 7 1.4 Lambda calculus and computability . . . . . . . . . . . . . . . . 8 1.5 Connections to computer science . . . . . . . . . . . . . . . . . . 9 1.6 Connections to logic . . . . . . . . . . . . . . . . . . . . . . . . 9 1.7 Connections to mathematics . . . . . . . . . . . . . . . . . . . . 10 2 The untyped lambda calculus 10 2.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 1
2.2 Free and bound variables,a-equivalence.............. 12 2.3 Substitution. 14 2.4 Introduction to B-reduction. 16 2.5 Formal definitions of B-reduction and B-equivalence.......17 3 Programming in the untyped lambda calculus 18 3.1 Booleans 18 3.2 Natural numbers......,.,.,.,............., 19 3.3 Fixpoints and recursive functions 3.4 Other datatypes:pairs,tuples,lists,trees,etc. 23 4 The Church-Rosser Theorem 25 4.1 Extensionality,equivalence,and nreduction 25 4.2 Statement of the Church-Rosser Theorem,and some consequences 27 4.3 Preliminary remarks on the proof of the Church-Rosser Theorem.29 4.4 Proof of the Church-Rosser Theorem 31 4.5 Exercises 36 5 Combinatory algebras 37 5.1 Applicative structures. 38 5.2 Combinatory completeness 39 5.3 Combinatory algebras. 1 5.4 The failure of soundness for combinatory algebras 42 55 Lambda algebras..... 5.6 Extensional combinatory algebras 48 6 Simply-typed lambda calculus,propositional logic,and the Curry- Howard isomorphism 50 6.1 Simple types and simply-typed terms ..50 6.Connections to propositional logi 53 6.3 Propositional intuitionistic logic 55
2.2 Free and bound variables, α-equivalence . . . . . . . . . . . . . . 12 2.3 Substitution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.4 Introduction to β-reduction . . . . . . . . . . . . . . . . . . . . . 16 2.5 Formal definitions of β-reduction and β-equivalence . . . . . . . 17 3 Programming in the untyped lambda calculus 18 3.1 Booleans . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 3.2 Natural numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 3.3 Fixpoints and recursive functions . . . . . . . . . . . . . . . . . . 21 3.4 Other datatypes: pairs, tuples, lists, trees, etc. . . . . . . . . . . . 23 4 The Church-Rosser Theorem 25 4.1 Extensionality, η-equivalence, and η-reduction . . . . . . . . . . . 25 4.2 Statement of the Church-Rosser Theorem, and some consequences 27 4.3 Preliminary remarks on the proof of the Church-Rosser Theorem . 29 4.4 Proof of the Church-Rosser Theorem . . . . . . . . . . . . . . . . 31 4.5 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 5 Combinatory algebras 37 5.1 Applicative structures . . . . . . . . . . . . . . . . . . . . . . . . 38 5.2 Combinatory completeness . . . . . . . . . . . . . . . . . . . . . 39 5.3 Combinatory algebras . . . . . . . . . . . . . . . . . . . . . . . . 41 5.4 The failure of soundness for combinatory algebras . . . . . . . . . 42 5.5 Lambda algebras . . . . . . . . . . . . . . . . . . . . . . . . . . 44 5.6 Extensional combinatory algebras . . . . . . . . . . . . . . . . . 48 6 Simply-typed lambda calculus, propositional logic, and the CurryHoward isomorphism 50 6.1 Simple types and simply-typed terms . . . . . . . . . . . . . . . . 50 6.2 Connections to propositional logic . . . . . . . . . . . . . . . . . 53 6.3 Propositional intuitionistic logic . . . . . . . . . . . . . . . . . . 55 2
6.4 An altemative presentation of natural deduction 57 6.5 The Curry-Howard Isomorphism.... 5 6.Reductions in the simply-typed lambda calculus 6.7 A word on Church-Rosser .................... 62 68 Reduction as proof simplification 6 Getting mileage out of the Curry-Howard isomorphism 6.10 Disjunction and sum types.. 65 6.11 Classical logic vs.intuitionistic logic......... 6.12 Classical logic and the Curry-Howard isomorphism........ 69 7 Polymorphism 70 8 Weak and strong normalization 8.1 Definitions 70 8 Weak and strong normalization in typed lambdacalculus 71 9 Type inference 72 9.1 Principal types 73 92 Type templates and type substitutions 74 9.3 Unifiers 75 9.4 The unification algorithm. 76 9.5 The type inference algorithm 78 10 Denotational semantics 9 10.1 Set-theoretic interpretation 102 Soundness 82 10.3 Completeness 84 11 The language PCF 85 11.1 Syntax and typing rules 85 11.2 Axiomatic equivalence 86
6.4 An alternative presentation of natural deduction . . . . . . . . . . 57 6.5 The Curry-Howard Isomorphism . . . . . . . . . . . . . . . . . . 59 6.6 Reductions in the simply-typed lambda calculus . . . . . . . . . . 61 6.7 A word on Church-Rosser . . . . . . . . . . . . . . . . . . . . . 62 6.8 Reduction as proof simplification . . . . . . . . . . . . . . . . . . 63 6.9 Getting mileage out of the Curry-Howard isomorphism . . . . . . 64 6.10 Disjunction and sum types . . . . . . . . . . . . . . . . . . . . . 65 6.11 Classical logic vs. intuitionistic logic . . . . . . . . . . . . . . . . 67 6.12 Classical logic and the Curry-Howard isomorphism . . . . . . . . 69 7 Polymorphism 70 8 Weak and strong normalization 70 8.1 Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 8.2 Weak and strong normalization in typed lambda calculus . . . . . 71 9 Type inference 72 9.1 Principal types . . . . . . . . . . . . . . . . . . . . . . . . . . . 73 9.2 Type templates and type substitutions . . . . . . . . . . . . . . . 74 9.3 Unifiers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75 9.4 The unification algorithm . . . . . . . . . . . . . . . . . . . . . . 76 9.5 The type inference algorithm . . . . . . . . . . . . . . . . . . . . 78 10 Denotational semantics 79 10.1 Set-theoretic interpretation . . . . . . . . . . . . . . . . . . . . . 80 10.2 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82 10.3 Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84 11 The language PCF 85 11.1 Syntax and typing rules . . . . . . . . . . . . . . . . . . . . . . . 85 11.2 Axiomatic equivalence . . . . . . . . . . . . . . . . . . . . . . . 86 3
11.3 Operational semantics 。。。 11.4 Big-step semantics 90 11.5 Operational equivalence. 91 11.6 Operational approximation 2 11.7 Discussion of operational equivalence 11.8 Operational equivalence and parallel or 93 12 Complete partialorders 95 12.1 Why are sets not enough.in general? 95 12.2 Complete partial orders....................... 96 12.3 Properties of limits. 9 12.4 Continuous functions 12.5 Pointed cpo's and strict functions 98 126 Productsand function spaces 98 12.7The of the simply-typed lambda caculus in com- plete partia rder 12.8 Cpo's and fixpoints 101 12.9 Example:Streams 102 13 Denotational semantics of PCF 102 13.1 Soundness and adequacy 102 13.2 Full abstraction 104 14 Bibliography 气 1 Introduction 1.1 Extensional vs.intensional view of functions What is a function?In modern mathematics the prevalent notion is that of"func tions as graphs":each function f has a fixed domain X and codomain Y,and a
11.3 Operational semantics . . . . . . . . . . . . . . . . . . . . . . . . 87 11.4 Big-step semantics . . . . . . . . . . . . . . . . . . . . . . . . . 90 11.5 Operational equivalence . . . . . . . . . . . . . . . . . . . . . . . 91 11.6 Operational approximation . . . . . . . . . . . . . . . . . . . . . 92 11.7 Discussion of operational equivalence . . . . . . . . . . . . . . . 92 11.8 Operational equivalence and parallel or . . . . . . . . . . . . . . 93 12 Complete partial orders 95 12.1 Why are sets not enough, in general? . . . . . . . . . . . . . . . . 95 12.2 Complete partial orders . . . . . . . . . . . . . . . . . . . . . . . 96 12.3 Properties of limits . . . . . . . . . . . . . . . . . . . . . . . . . 97 12.4 Continuous functions . . . . . . . . . . . . . . . . . . . . . . . . 98 12.5 Pointed cpo’s and strict functions . . . . . . . . . . . . . . . . . . 98 12.6 Products and function spaces . . . . . . . . . . . . . . . . . . . . 98 12.7 The interpretation of the simply-typed lambda calculus in complete partial orders . . . . . . . . . . . . . . . . . . . . . . . . . 100 12.8 Cpo’s and fixpoints . . . . . . . . . . . . . . . . . . . . . . . . . 101 12.9 Example: Streams . . . . . . . . . . . . . . . . . . . . . . . . . . 102 13 Denotational semantics of PCF 102 13.1 Soundness and adequacy . . . . . . . . . . . . . . . . . . . . . . 102 13.2 Full abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . . 104 14 Bibliography 106 1 Introduction 1.1 Extensional vs. intensional view of functions What is a function? In modern mathematics, the prevalent notion is that of “functions as graphs”: each function f has a fixed domain X and codomain Y , and a 4
functionf:Y isaset of pairsf considered equal if they vield the same output on each input.i(=)for allX.This is called the extensional view of functions,because it specifies that the only thing observable about a function is how it maps inputs to outputs. However.before the 20th century.functions were rarely looked at in this wav An older notion of functions as that of"functions as rules" In this view,to give on means to give a ru for how the function s t .O 2 o(=sin(e)from calculus.As before.two functions are extensionally equal if they have the same input-output behavior,but now we can also speak of another notion of equality:two functions are intensionally equal if they are given by (essentially)the same formula When we think of functions as given by formulas,it is not always necessary to fof course.the identity function.We may regard it as a function ider for instance the function In most of mathematics,the"fu nctions as graphs"parad digm is the most s that a Thus.when we prove a mathematical statement such as"any differentiable func tion is continuou s",we really mean this is true all functions(in the mathematical sense).not just those functions for which a rule can be given On the other hand,in computer science,the "functions as rules"paradigm is often more appropriate.Think of a computer program as defining a function that maps progra rs (and puts).but also about the output is calculated:How much time does it take? How much memory and disk space is used in the process?How much communi cation bandwidth usd？ se are in nal questions having to do with the Note that this word is intentionally spelled Tntensionally
function f : X → Y is a set of pairs f ⊆ X × Y such that for each x ∈ X, there exists exactly one y ∈ Y such that (x, y) ∈ f. Two functions f, g : X → Y are considered equal if they yield the same output on each input, i.e., f(x) = g(x) for all x ∈ X. This is called the extensional view of functions, because it specifies that the only thing observable about a function is how it maps inputs to outputs. However, before the 20th century, functions were rarely looked at in this way. An older notion of functions as that of “functions as rules”. In this view, to give a function means to give a rule for how the function is to be calculated. Often, such a rule can be given by a formula, for instance, the familiar f(x) = x 2 or g(x) = sin(e x ) from calculus. As before, two functions are extensionally equal if they have the same input-output behavior; but now we can also speak of another notion of equality: two functions are intensionally1 equal if they are given by (essentially) the same formula. When we think of functions as given by formulas, it is not always necessary to know the domain and codomain of a function. Consider for instance the function f(x) = x. This is, of course, the identity function. We may regard it as a function f : X → X for any set X. In most of mathematics, the “functions as graphs” paradigm is the most elegant and appropriate way of dealing with functions. Graphs define a more general class of functions, because it includes functions that are not necessarily given by a rule. Thus, when we prove a mathematical statement such as “any differentiable function is continuous”, we really mean this is true all functions (in the mathematical sense), not just those functions for which a rule can be given. On the other hand, in computer science, the “functions as rules” paradigm is often more appropriate. Think of a computer program as defining a function that maps input to output. Most computer programmers (and users) do not only care about the extensional behavior of a program (which inputs are mapped to which outputs), but also about how the output is calculated: How much time does it take? How much memory and disk space is used in the process? How much communication bandwidth is used? These are intensional questions having to do with the particular way in which a function was defined. 1Note that this word is intentionally spelled “intensionally”. 5