Book contents
- Frontmatter
- Contents
- Preface
- 1 The λ-calculus
- 2 Combinatory logic
- 3 The power of λ and combinators
- 4 Representing the computable functions
- 5 The undecidability theorem
- 6 The formal theories λβ and CLw
- 7 Extensionality in λ-calculus
- 8 Extensionality in combinatory logic
- 9 Correspondence between λ and CL
- 10 Simple typing, Church-style
- 11 Simple typing, Curry-style in CL
- 12 Simple typing, Curry-style in λ
- 13 Generalizations of typing
- 14 Models of CL
- 15 Models of λ-calculus
- 16 Scott's D∞ and other models
- Appendix A1 Bound variables and α-conversion
- Appendix A2 Confluence proofs
- Appendix A3 Strong normalization proofs
- Appendix A4 Care of your pet combinator
- Appendix A5 Answers to starred exercises
- References
- List of symbols
- Index
6 - The formal theories λβ and CLw
Published online by Cambridge University Press: 05 June 2012
- Frontmatter
- Contents
- Preface
- 1 The λ-calculus
- 2 Combinatory logic
- 3 The power of λ and combinators
- 4 Representing the computable functions
- 5 The undecidability theorem
- 6 The formal theories λβ and CLw
- 7 Extensionality in λ-calculus
- 8 Extensionality in combinatory logic
- 9 Correspondence between λ and CL
- 10 Simple typing, Church-style
- 11 Simple typing, Curry-style in CL
- 12 Simple typing, Curry-style in λ
- 13 Generalizations of typing
- 14 Models of CL
- 15 Models of λ-calculus
- 16 Scott's D∞ and other models
- Appendix A1 Bound variables and α-conversion
- Appendix A2 Confluence proofs
- Appendix A3 Strong normalization proofs
- Appendix A4 Care of your pet combinator
- Appendix A5 Answers to starred exercises
- References
- List of symbols
- Index
Summary
The definitions of the theories
The relations of reducibility and convertibility were defined in Chapters 1 and 2 via contractions of redexes. The present chapter gives alternative definitions, via formal theories with axioms and rules of inference.
These theories will be used later in describing the correspondence between λ and CL precisely, and will help to make the distinction between syntax and semantics clearer in the chapters on models to come. They will also give a more direct meaning to such phrases as ‘add the equation M = N as a new axiom to the definition of = β … ’ (Corollary 3.11.1).
In books on logic, formal theories come in two kinds (at least): Hilbert-style and Gentzen-style. The theories in this chapter will be the former.
Notation 6.1 (Hilbert-style formal theories) A (Hilbert-style) formal theory T consists of three sets: formulas, axioms and rules (of inference). Each rule has one or more premises and one conclusion, and we shall write its premises above a horizontal line and its conclusion under this line; for examples, see the rules in Definition 6.2 below.
If г is a set of formulas, a deduction of a formula B from г is a tree of formulas, with those at the tops of branches being axioms or members of г, the others being deduced from those immediately above them by a rule, and the bottom one being B.
- Type
- Chapter
- Information
- Lambda-Calculus and CombinatorsAn Introduction, pp. 69 - 75Publisher: Cambridge University PressPrint publication year: 2008