---
tag: HD5KCKVPS8
kind: definition
name: Lambda calculus
msc: [03B40, 68N18]
defines: BD756KR8FM
sources:
  - url: https://en.wikipedia.org/wiki/Lambda_calculus
---

## Definition

Fix a countably infinite set $V$ of variables.
The *lambda terms* are the strings defined by these rules:

1. every variable $x \in V$ is a term;
2. if $M$ is a term and $x \in V$, then $(\lambda x.\, M)$ is a term, called an *abstraction*;
3. if $M$ and $N$ are terms, then $(M\, N)$ is a term, called an *application*.

In $\lambda x.\, M$ the variable $x$ is bound in $M$.
Terms that differ only in the names of bound variables are identified ($\alpha$-equivalence).
Let $M[x := N]$ be the term obtained from $M$ by replacing the free occurrences of $x$ by $N$.
Before the replacement, bound variables of $M$ are renamed so that no free variable of $N$ gets bound.
The *untyped lambda calculus* is the set of terms together with *$\beta$-reduction*.
This is the relation generated by the rule
$$(\lambda x.\, M)\, N \to_\beta M[x := N],$$
applied to any subterm of a term.

## Remarks

Example: $(\lambda x.\, x\, x)(\lambda y.\, y)$ is a term by rules 1 to 3, and
$$(\lambda x.\, x\, x)(\lambda y.\, y) \to_\beta (\lambda y.\, y)(\lambda y.\, y) \to_\beta \lambda y.\, y.$$
The last term has no further reduction, so it is a *normal form*.

Non-example: the string $\lambda x$ alone is not a term, since rule 2 requires a body $M$ after the dot.

The term $\Omega = (\lambda x.\, x\, x)(\lambda x.\, x\, x)$ reduces only to itself, so it has no normal form.
By the Church–Rosser theorem, a term has at most one normal form up to $\alpha$-equivalence.