First published Wed Dec 12, 2012; substantive revision Tue Jul 25, 2023
The \(\lambda\)-calculus is, at heart, a simple notation for functions and application. The main ideas are applying a function to an argument and forming functions by abstraction. The syntax of basic \(\lambda\)-calculus is quite sparse, making it an elegant, focused notation for representing functions. Functions and arguments are on a par with one another. The result is a non-extensional theory of functions as rules of computation, contrasting with an extensional theory of functions as sets of ordered pairs. Despite its sparse syntax, the expressiveness and flexibility of the \(\lambda\)-calculus make it a cornucopia of logic and mathematics. This entry develops some of the central highlights of the field and prepares the reader for further study of the subject and its applications in philosophy, linguistics, computer science, and logic.
The \(\lambda\)-calculus is an elegant notation for working with applications of functions to arguments. To take a mathematical example, suppose we are given a simple polynomial such as \(x^2 -2\cdot x+5\). What is the value of this expression when \(x = 2\)? We compute this by ‘plugging in’ 2 for \(x\) in the expression: we get \(2^2 -2\cdot 2+5\), which we can further reduce to get the answer 5. To use the \(\lambda\)-calculus to represent the situation, we start with the \(\lambda\)-term
\[ \lambda x[x^2 -2\cdot x+5]. \]
The \(\lambda\) operators allows us to abstract over \(x\). One can intuitively read ‘\(\lambda x[x^2 -2\cdot x+5]\)’ as an expression that is waiting for a value \(a\) for the variable \(x\). When given such a value \(a\) (such as the number 2), the value of the expression is \(a^2 -2\cdot a+5\). The ‘\(\lambda\)’ on its own has no significance; it merely binds the variable \(x\), guarding it, as it were, from outside interference. The terminology in \(\lambda\)-calculus is that we want to apply this expression to an argument, and get a value. We write ‘\(Ma\)’ to denote the application of the function \(M\) to the argument \(a\). Continuing with the example, we get:
\[\begin{align} (\lambda x[x^2 -2\cdot x+5])2 \rhd 2^2& -2\cdot 2+5 &\langle \text{Substitute 2 for } x\rangle \\ &= 4-4+5 &\langle\text{Arithmetic}\rangle \\ &= 5 &\langle\text{Arithmetic}\rangle \end{align}\]
The first step of this calculation, plugging in ‘2’ for occurrences of \(x\) in the expression ‘\(x^2 - 2\cdot x + 5\)’, is the passage from an abstraction term to another term by the operation of substitution. The remaining equalities are justified by computing with natural numbers.
This example suggests the central principle of the \(\lambda\)-calculus, called \(\beta\)-reduction, which is also sometimes called \(\beta\)-conversion:
\[ \tag{\(\beta\)} (\lambda x[M])N \rhd M[x := N] \]
The understanding is that we can reduce or contract \((\rhd)\) an application \((\lambda xM)N\) of an abstraction term (the left-hand side, \(\lambda xM)\) to something (the right-hand side, \(N)\) by simply plugging in \(N\) for the occurrences of \(x\) inside \(M\) (that’s what the notation ‘\(M[x := N]\)’ expresses). \(\beta\)-reduction, or \(\beta\)-conversion, is the heart of the \(\lambda\)-calculus. When one actually applies \(\beta\)-reduction to reduce a term, there is an important proviso that has to be observed. But this will be described in Section 2.1, when we discuss bound and free variables.
... continue reading