Preface ........................................................ ix
1 Elements of combinatory logic ................................ 1
1.1 Objects, combinators and terms .......................... 1
1.2 Various kinds of combinators ............................ 6
1.3 Reductions and combinatory bases ....................... 12
2 Main theorems ............................................... 29
2.1 Church-Rosser property ................................. 29
2.2 Normal forms and consistency ........................... 38
2.3 Fixed points ........................................... 44
2.4 Second fixed point theorem and undecidability .......... 52
3 Recursive functions and arithmetic .......................... 53
3.1 Primitive and partial recursive functions .............. 54
3.2 First modeling of partial recursive functions in CL .... 64
3.3 Second modeling of partial recursive functions in CL ... 81
3.4 Undecidability of weak equality ........................ 85
4 Connections to λ-calculi .................................... 93
4.1 λ-calculi: Λ .......................................... 93
4.2 Combinators in Λ ...................................... 106
4.3 Back and forth between CL and Λ ....................... 110
5 (In)equational combinatory logic ........................... 121
5.1 Inequational calculi .................................. 121
5.2 Equational calculi .................................... 128
6 Models ..................................................... 133
6.1 Term models ........................................... 134
6.2 Operational models .................................... 136
6.3 Encoding functions by numbers ......................... 148
6.4 Domains ............................................... 155
6.5 Models for typed CL ................................... 165
6.6 Relational models ..................................... 174
7 Dual and symmetric combinatory logics ...................... 179
7.1 Dual combinators ...................................... 179
7.2 Symmetric combinators ................................. 201
7.3 Structurally free logics .............................. 210
8 Applied combinatory logic .................................. 221
8.1 Illative combinatory logic ............................ 221
8.2 Elimination of bound variables ........................ 227
9 Typed combinatory logic .................................... 237
9.1 Simply typed combinatory logic ........................ 237
9.2 Intersection types for combinators .................... 268
Appendix ...................................................... 275
A.l Elements of combinatory logic ......................... 275
A.2 Main theorems ......................................... 284
A.3 Recursive functions and arithmetic .................... 288
A.4 Connections to λ-calculi .............................. 292
A.5 (In)equational combinatory logic ...................... 294
A.6 Models ................................................ 296
A.7 Dual and symmetric combinatory logic .................. 302
A.8 Applied combinatory logic ............................. 308
A.9 Typed combinatory logic ............................... 312
Bibliography .................................................. 321
List of Symbols ............................................... 331
Index ......................................................... 335
|
