6 - Lambda Calculus, or an Attempt to Reinstate Computation in the Realm of Mathematics

Summary

the theory of computability, which provided a negative answer to Hilbert's decision problem, went hand in hand with an attempt to reinstate computation in mathematics. Although this attempt failed, it is significant and worthy of attention. In many ways, it foreshadowed future developments in the history of mathematics. This attempt rests on a language that is considered to be Church's greatest achievement, namely lambda calculus.

Lambda calculus started out as a simple functional notation system. A function can be represented by a table of values, or by a curve, but also, in some cases, by a functional expression. For example, the function that, to a number, assigns the square of that number can be represented by the expression x × x.

This notation, however, is somewhat clumsy, because it doesn't distinguish between the function and the value assumed by that function at a specific point. Thus, when you say that “if x is odd, then x × x is odd,” you are talking about the number x × x or, in other words, about the value taken by the function at x. On the other hand, when you say that “x × x is increasing,” you are talking about the function itself. In order to avoid this confusion, we will denote the function by x ↦ x × x rather than x × x.

This new notation is believed to have been introduced around 1930 by Nicolas Bourbaki, the pseudonym used by a group of mathematicians who wrote an important treatise, published in a series of installments over many years, that compiled the mathematical knowledge at the time. Around the same time, Church introduced a similar notation: λx(x × x), where the arrow ↦ was replaced by the Greek letter lambda. This notation is reminiscent of a previous convention, used by Russell and Whitehead in the early 1900s: x(x × x).