Combinatory logic and lambda-calculus, originally devised in the 1920's, have since developed into linguistic tools, especially useful in programming languages. The authors' previous book served as the main reference for introductory courses on lambda-calculus for over 20 years: this long-awaited new version is thoroughly revised and offers a fully up-to-date account of the subject, with the same authoritative exposition. The grammar and basic properties of both combinatory logic and lambda-calculus are discussed, followed by an introduction to type-theory. Typed and untyped versions of the systems, and their differences, are covered. Lambda-calculus models, which lie behind much of the semantics of programming languages, are also explained in depth. The treatment is as non-technical as possible, with the main ideas emphasized and illustrated by examples. Many exercises are included, from routine to advanced, with solutions to most at the end of the book.
Author(s): J. Roger Hindley, Jonathan P. Seldin
Edition: 2
Publisher: Cambridge University Press
Year: 2008
Language: English
Pages: 359
Cover......Page 1
Half-title......Page 3
Title......Page 5
Copyright......Page 6
Contents......Page 8
Preface......Page 11
1A Introduction......Page 15
1B Term-structure and substitution......Page 19
1C beta-reduction......Page 25
1D beta-equality......Page 30
Further reading......Page 33
2A Introduction to CL......Page 35
2B Weak reduction......Page 38
2C Abstraction in CL......Page 40
2D Weak equality......Page 43
Further reading......Page 46
3A Introduction......Page 47
3B The fixed-point theorem......Page 48
3C Bohm’s theorem......Page 50
3D The quasi-leftmost-reduction theorem......Page 54
3E History and interpretation......Page 57
4A Introduction......Page 61
4B Primitive recursive functions......Page 64
4C Recursive functions......Page 70
4D Abstract numerals and Z......Page 75
5 The undecidability theorem......Page 77
6A The definitions of the theories......Page 83
6B First-order theories......Page 86
6C Equivalence of theories......Page 87
7A Extensional equality......Page 90
7B lambdaeta-reduction in lambda-calculus......Page 93
8A Extensional equality......Page 96
8B Axioms for extensionality in CL......Page 99
8C Strong reduction......Page 103
9A Introduction......Page 106
9B The extensional equalities......Page 109
9C New abstraction algorithms in CL......Page 114
9D Combinatory beta-equality......Page 116
10A Simple types......Page 121
10B Typed lambda-calculus......Page 123
10C Typed CL......Page 129
11A Introduction......Page 133
11B The system TA→C......Page 136
11C Subject-construction......Page 140
11D Abstraction......Page 141
11E Subject-reduction......Page 144
11F Typable CL-terms......Page 148
11G Link with Church’s approach......Page 151
11H Principal types......Page 152
11I Adding new axioms......Page 157
11J Propositions-as-types and normalization......Page 161
12A The system TA→lambda......Page 173
12B Basic properties of TA→lambda......Page 179
12C Typable lambda-terms......Page 184
12D Propositions-as-types and normalization......Page 187
12E The equality-rule Eq......Page 190
Further reading......Page 192
13A Introduction......Page 194
13B Dependent function types, introduction......Page 195
13C Basic generalized typing, Curry-style in lambda......Page 197
13D Deductive rules to define types......Page 201
13E Church-style typing in lambda......Page 205
13F Normalization in PTSs......Page 216
13G Propositions-as-types......Page 223
13H PTSs with equality......Page 231
14A Applicative structures......Page 234
14B Combinatory algebras......Page 237
15A The definition of lambda-model......Page 243
15B Syntax-free definitions......Page 250
15C General properties of lambda-models......Page 256
16A Introduction: complete partial orders......Page 261
16B Continuous functions......Page 266
16C The construction of D∞......Page 270
16E D∞ is a lambda-model......Page 281
16F Some other models......Page 285
Further reading......Page 289
Appendix A1 Bound variables and alpha-conversion......Page 290
A2A Confluence of beta-reduction......Page 296
A2B Confluence of other reductions......Page 303
Appendix A3 Strong normalization proofs......Page 307
A3A Simply typed lambda-calculus......Page 308
A3B Simply typed CL......Page 311
A3C Arithmetical system......Page 313
Appendix A4 Care of your pet combinator......Page 319
Appendix A5 Answers to starred exercises......Page 321
References......Page 337
List of symbols......Page 348
Index......Page 351
