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 552.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 Curry￾Howard 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