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
4 - Representing the computable functions
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
Introduction
In this chapter, a sequence of pure terms will be chosen to represent the natural numbers. It is then reasonable to expect that some of the other terms will represent functions of natural numbers, in some sense. This sense will be defined precisely below. The functions so representable will turn out to be exactly those computable by Turing machines.
In the 1930s, three concepts of computability arose independently: ‘Turing-computable function’, ‘recursive function’ and ‘λ-definable function’. The inventors of these three concepts soon discovered that all three gave the same set of functions. Most logicians took this as strong evidence that the informal notion of ‘computable function’ had been captured exactly by these three formally-defined concepts.
Here we shall look at the recursive functions, and prove that all these functions can be represented in λ and CL. (We shall not work with the Turing-computable functions because their representability-proof is longer.)
An outline definition of the recursive functions will be given here; more details and background can be found in many textbooks on computability or textbooks on logic which include computability, for example [Coh87], [Men97] or the old but thorough [Kle52].
Notation 4.1 This chapter is written in the same neutral notation as the last one, and its results will hold for both λ and CL unless explicitly stated otherwise.
- Type
- Chapter
- Information
- Lambda-Calculus and CombinatorsAn Introduction, pp. 47 - 62Publisher: Cambridge University PressPrint publication year: 2008