In 1936, the mathematician Alonzo Church published a paper called “An unsolvable problem of number theory”. In it he set out a way to decide which functions of whole numbers could ever be worked out by a fixed, effective procedure. He called a function “λ-definable” if it could be built inside his own notation, a system now known as the lambda calculus. Alan Turing’s work of the same period reached the same result on a related problem.
more
Church’s tool was a formalism, written entirely in symbols. Within it, a programmer can carry out both arithmetic and logic. A lambda calculus function has no name and cannot refer to itself, yet the system can still define recursion, the trick of a function calling on its own result. In his paper, Church tied the notation to the recursive functions of number theory: “Every λ-definable function of positive integers is recursive.”
Two routes to the same idea
Church built the lambda calculus to study the mathematical properties of effectively computable functions. What “effectively calculable” means sat behind the decision problem posed by the mathematician David Hilbert. Church’s 1936 paper, alongside Turing’s work, showed that Hilbert’s decision problem has no general solution.
One later paper argues that Church’s and Turing’s models can each simulate the other. It also argues that they are not equivalent when they work on symbols rather than numbers. The paper notes that Church’s own definitions were all stated in terms of numbers. It traces the name “Church-Turing Thesis” to Stephen Kleene’s book Introduction to Metamathematics, which never actually states it.
Where it ended up
The lambda calculus did not stay a historical curiosity. It became the theoretical foundation underneath an entire family of programming languages, the functional ones. Lambda models still underpin the theory of higher-order programming languages.
