The λ-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 x2−2⋅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 22−2⋅2+5, which we can further reduce to get the answer 5. To use the λ-calculus to represent the situation, we start with the λ-term
The λ operators allows us to abstract over x. One can intuitively read ‘λx[x2−2⋅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 a2−2⋅a+5. The ‘λ’ on its own has no significance; it merely binds the variable xx, guarding it, as it were, from outside interference. The terminology in λ-calculus is that we want to apply this expression to an argument, and get a value. We write ‘MaMa’ to denote the application of the function MM to the argument aa. Continuing with the example, we get:
=4−4+5〈Arithmetic〉
=5〈Arithmetic〉
The first step of this calculation, plugging in ‘2’ for occurrences of x in the expression ‘x2−2⋅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 λλ-calculus, called β-reduction, which is also sometimes called β-conversion:
The understanding is that we can reduce or contract (⊳)an application (λxM)N of an abstraction term (the left-hand side, λ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). β-reduction, or β-conversion, is the heart of the λ-calculus.
