Lambda calculus

Lambda terms¹

The lambda calculus has three basic components, or lambda terms: expressions, variables, and abstractions. The word expression refers to a superset of all those things: an expression can be a variable name, an abstraction, or a combination of those things. …

An abstraction is a function. It is a lambda term that has a head (a lambda) and a body and is applied to an argument. An argument is an input value.

Abstractions consist of two parts: the head and the body. The head of the function is a $\lambda$ (lambda) followed by a variable name. The body of the function is another expression. So, a simple function might look like this:

$\lambda x. x$

The variable named in the head is the parameter and binds all instances of that same variable in the body of the function. … The act of applying a lambda function to an argument is called application, and application is the lynchpin of the lambda calculus. … When we apply the abstraction to arguments, we replace the names with values, making it concrete.

Alpha equivalence¹

The variable $x$ in $\lambda x. x$ is not semantically meaningful except in its role in that single expression. Because of this, there’s a form of equivalence between lambda terms called alpha equivalence. This is a way of saying that the following expressions all mean the same thing:

$\lambda x. x$ $\lambda d. d$ $\lambda z. z$

Beta reduction¹

When we apply a function to an argument, we substitute the input expression for all instances of bound variables within the body of the abstraction. You also eliminate the head of the abstraction, since its only purpose is to bind a variable. This process is called beta reduction.

Let’s use the function we had above: $\lambda x.x$

… We apply the function above to 2, substitute 2 for each bound variable in the body of the function, and eliminate the head:

$\lambda x.x \space 2 \rightarrow 2$

The only bound variable is the single $x$ , so applying this function to 2 return 2. This function is the identity function. …

Beta reduction is this process of applying a lambda term to an argument, replacing the bound variables with the value of the argument, and eliminating the head. Eliminating the head tells you the function has been applied. …

Applications in the lambda calculus are left associative. Unless specific parentheses suggest otherwise, they associate, or group, to the left. So $(\lambda x.x)(\lambda y.y)z$ can be rewritten as: $((\lambda x.x)(\lambda y.y))z$

Free variables¹

… sometimes, the body expression has variables that are not named in the head. We call those variables free variables. In the expression $\lambda x.xy$, the $x$ in the body is a bound variable, because it is named in the head of the function, while the $y$ is a free variable, because it is not. …

Note that alpha equivalence does not apply to free variables. That is, $\lambda x.xz$ and $\lambda x.x.y$ are not equivalent, because $z$ and $y$ might be different things. However, $\lambda xy.yx$ and $\lambda ab.ba$ are equivalent due to alpha equivalence, as are $\lambda x.xz$ and $\lambda x.xy$, because the free variable is left alone.

Multiple arguments

Evaluation is simplification

Combinators

Divergence

Footnotes

1. Haskell programming from first principles ↩ ↩² ↩³ ↩⁴