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 and 2013. Topics covered in these notes include the un-
                                                                    typed lambda calculus, the Church-Rosser theorem, combinatory algebras,
                                                                    the simply-typed lambda calculus, the Curry-Howard isomorphism, weak
                                                                    and strong normalization, polymorphism, type inference, denotational se-
                                                                    mantics, complete partial orders, and the language PCF.
                                                          Contents
                                                          1     Introduction                                                                                                               6
                                                                1.1       Extensional vs. intensional view of functions                               . . . . . . . . . . .                6
                                                                1.2       Thelambdacalculus . . . . . . . . . . . . . . . . . . . . . . . .                                                7
                                                                1.3       Untypedvs. typed lambda-calculi                          . . . . . . . . . . . . . . . . .                       8
                                                                1.4       Lambdacalculusandcomputability . . . . . . . . . . . . . . . .                                                   9
                                                                1.5       Connectionsto computerscience . . . . . . . . . . . . . . . . . .                                              10
                                                                1.6       Connectionsto logic                 .  . . . . . . . . . . . . . . . . . . . . . . .                           10
                                                                1.7       Connectionsto mathematics . . . . . . . . . . . . . . . . . . . .                                              11
                                                          2     Theuntypedlambdacalculus                                                                                                 11
                                                                2.1       Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .                                         11
                                                                                                                          1
                                            2.2   Free and bound variables, α-equivalence . . . . . . . . . . . . . .         13
                                            2.3   Substitution . . . . . . . . . . . . . . . . . . . . . . . . . . . . .      15
                                            2.4   Introduction to β-reduction . . . . . . . . . . . . . . . . . . . . .       17
                                            2.5   Formaldefinitionsof β-reductionand β-equivalence . . . . . . .               18
                                        3   Programmingintheuntypedlambdacalculus                                             19
                                            3.1   Booleans     . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .    19
                                            3.2   Natural numbers . . . . . . . . . . . . . . . . . . . . . . . . . . .       20
                                            3.3   Fixed points and recursive functions . . . . . . . . . . . . . . . .        22
                                            3.4   Other data types: pairs, tuples, lists, trees, etc. . . . . . . . . . . .   24
                                        4   TheChurch-RosserTheorem                                                           26
                                            4.1   Extensionality, η-equivalence, and η-reduction . . . . . . . . . . .        26
                                            4.2   Statement of the Church-Rosser Theorem, and some consequences               28
                                            4.3   Preliminary remarks on the proof of the Church-Rosser Theorem .             30
                                            4.4   Proof of the Church-Rosser Theorem . . . . . . . . . . . . . . . .          32
                                            4.5   Exercises    . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .    37
                                        5   Combinatoryalgebras                                                               38
                                            5.1   Applicative structures . . . . . . . . . . . . . . . . . . . . . . . .      39
                                            5.2   Combinatorycompleteness . . . . . . . . . . . . . . . . . . . . .           40
                                            5.3   Combinatoryalgebras . . . . . . . . . . . . . . . . . . . . . . . .         42
                                            5.4   Thefailure of soundness for combinatory algebras . . . . . . . . .          43
                                            5.5   Lambdaalgebras . . . . . . . . . . . . . . . . . . . . . . . . . .          45
                                            5.6   Extensional combinatory algebras . . . . . . . . . . . . . . . . .          49
                                        6   Simply-typed lambda calculus, propositional logic, and the Curry-
                                            Howardisomorphism                                                                 51
                                            6.1   Simple types and simply-typed terms . . . . . . . . . . . . . . . .         51
                                            6.2   Connectionsto propositional logic . . . . . . . . . . . . . . . . .         54
                                            6.3   Propositional intuitionistic logic    . . . . . . . . . . . . . . . . . .   56
                                                                                    2
                                           6.4   Analternative presentation of natural deduction . . . . . . . . . .       58
                                           6.5   TheCurry-HowardIsomorphism . . . . . . . . . . . . . . . . . .            60
                                           6.6   Reductions in the simply-typed lambda calculus . . . . . . . . . .        62
                                           6.7   AwordonChurch-Rosser . . . . . . . . . . . . . . . . . . . . .            63
                                           6.8   Reduction as proof simplification . . . . . . . . . . . . . . . . . .      64
                                           6.9   Getting mileage out of the Curry-Howardisomorphism . . . . . .            65
                                           6.10 Disjunction and sum types . . . . . . . . . . . . . . . . . . . . .        66
                                           6.11 Classical logic vs. intuitionistic logic . . . . . . . . . . . . . . . .   68
                                           6.12 Classical logic and the Curry-Howardisomorphism . . . . . . . .            70
                                       7   Weakandstrongnormalization                                                      71
                                           7.1   Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .    71
                                           7.2   Weakandstrongnormalizationin typed lambdacalculus . . . . .               72
                                       8   Polymorphism                                                                    73
                                           8.1   Syntax of System F . . . . . . . . . . . . . . . . . . . . . . . . .      73
                                           8.2   Reduction rules . . . . . . . . . . . . . . . . . . . . . . . . . . .     74
                                           8.3   Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .      75
                                                 8.3.1    Booleans . . . . . . . . . . . . . . . . . . . . . . . . . .     75
                                                 8.3.2    Natural numbers . . . . . . . . . . . . . . . . . . . . . .      76
                                                 8.3.3    Pairs . . . . . . . . . . . . . . . . . . . . . . . . . . . . .  77
                                           8.4   Church-Rosser property and strong normalization . . . . . . . . .         77
                                           8.5   TheCurry-Howardisomorphism . . . . . . . . . . . . . . . . . .            78
                                           8.6   Supplying the missing logical connectives . . . . . . . . . . . . .       79
                                           8.7   Normalformsandlongnormalforms . . . . . . . . . . . . . . .               80
                                           8.8   Thestructure of closed normal forms . . . . . . . . . . . . . . . .       82
                                           8.9   Application: representation of arbitrary data in System F . . . . .       84
                                       9   Typeinference                                                                   86
                                           9.1   Principal types    . . . . . . . . . . . . . . . . . . . . . . . . . . .  87
                                                                                  3
                                            9.2   Typetemplates and type substitutions       . . . . . . . . . . . . . . .   87
                                            9.3   Unifiers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .      89
                                            9.4   Theunification algorithm . . . . . . . . . . . . . . . . . . . . . .        90
                                            9.5   Thetypeinferencealgorithm . . . . . . . . . . . . . . . . . . . .          92
                                        10 Denotationalsemantics                                                             93
                                            10.1 Set-theoretic interpretation . . . . . . . . . . . . . . . . . . . . .      94
                                            10.2 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .       96
                                            10.3 Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . .        98
                                        11 ThelanguagePCF                                                                    98
                                            11.1 Syntax and typing rules . . . . . . . . . . . . . . . . . . . . . . .       99
                                            11.2 Axiomatic equivalence . . . . . . . . . . . . . . . . . . . . . . . 100
                                            11.3 Operational semantics . . . . . . . . . . . . . . . . . . . . . . . . 101
                                            11.4 Big-step semantics . . . . . . . . . . . . . . . . . . . . . . . . . 103
                                            11.5 Operational equivalence . . . . . . . . . . . . . . . . . . . . . . . 105
                                            11.6 Operational approximation . . . . . . . . . . . . . . . . . . . . . 106
                                            11.7 Discussion of operational equivalence . . . . . . . . . . . . . . . 106
                                            11.8 Operational equivalence and parallel or       . . . . . . . . . . . . . . 107
                                        12 Completepartialorders                                                           109
                                            12.1 Whyaresets notenough,in general? . . . . . . . . . . . . . . . . 109
                                            12.2 Complete partial orders . . . . . . . . . . . . . . . . . . . . . . . 109
                                            12.3 Properties of limits . . . . . . . . . . . . . . . . . . . . . . . . . 111
                                            12.4 Continuousfunctions . . . . . . . . . . . . . . . . . . . . . . . . 111
                                            12.5 Pointed cpo’s and strict functions . . . . . . . . . . . . . . . . . . 112
                                            12.6 Products and function spaces . . . . . . . . . . . . . . . . . . . . 112
                                            12.7 The interpretation of the simply-typed lambda calculus in com-
                                                  plete partial orders   . . . . . . . . . . . . . . . . . . . . . . . . . 114
                                            12.8 Cpo’s and fixed points       . . . . . . . . . . . . . . . . . . . . . . . 114
                                                                                   4