Synthese Library

1. The Theory of Combinators and the ?-Calculus.- 1. Introduction.- 2. Informal theory of combinators.- 2.1. Combinators and combinations.- 2.2. The combinators I, B, W, C, ?, ?.- 2.3. Extensionality.- 2.4. Alternative primitive combinators.- 2.5. Composite products, powers and deferred combinators.- 2.6. Truth-functions.- 3. Equality and reduction.- 3.2. Combinatory terms.- 3.3. ?-equality.- 3.4. Functional abstraction.- 3.5. Substitution.- 3.6. Weak reduction.- 3.7. Equality.- 3.8. Strong reduction.- 4. The ?-calculus.- 4.1. ?-terms.- 4.2. Substitution.- 4.3. Equality.- 4.4. Reduction.- 4.5. ?-reduction.- 4.6. Historical remarks.- 5. Equivalence of the ?-calculus and the theory of combinators.- 6. Set-theoretical interpretations of combinators.- 6.1. Introduction.- 6.2. Scott's models.- 6.3. Combinatorial completeness.- 6.4. A representation result.- 6.5. Limit spaces.- 7. Illative combinatory logic and the paradoxes.- 2. The Church-Rosser Property.- 1. Introduction.- 2. R-reductions.- 3. One-step reduction.- 4. Proof of main result.- 5. Generalization.- 6. Generalized weak reduction.- 3. Combinatory Arithmetic.- 1. Introduction.- 2. Combinatory definability.- 3. Fixed-points and numeral sequences.- 4. Undecidability results.- 4. Computable Functionals of Finite Type.- 1. Introduction.- 2. Finite types and terms of finite types.- 3. The equation calculus.- 4. The role of the induction rule.- 5. Soundness of the axioms.- 6. Defining axioms and uniqueness rules.- 7. Reduction rules.- 8. Computability and normal form.- 9. Interpretation of types and terms.- 5. Proofs in the Theory of Species.- 1. Introduction.- 2. Formulas, terms and types.- 3. A-terms and deductions.- 4. The equation calculus.- 5. Reduction and normal form.- 6. The strong normalization theorem.- 7. Interpretation of types and terms.- Index of Names.- Index of Subjects.