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