Untyped lambda calculus

The untyped lambda calculus forms terms from variables, abstraction, and application without assigning types.

Beta reduction performs capture-avoiding substitution:

Capture-avoiding substitution $M[x:=N]$ replaces the free occurrences of $x$ in $M$ by $N$, renaming bound variables when necessary so that free variables of $N$ do not become bound.

Beta equivalence is the smallest equivalence relation containing beta reduction; equivalently, $M{\equiv }_{\beta }N$ when a finite sequence of beta reductions and reversed beta reductions connects $M$ and $N$.

A beta-redex is a subterm of the form $(\lambda x.M)N$, to which beta reduction can be applied.

A lambda term is in beta-normal form when it contains no beta-redex.

A combinator is a lambda term with no free variables.

The omega combinator is the divergent untyped lambda calculus termwhose only beta reduction reproduces $\Omega$.

An untyped lambda term $Y$ is a fixed-point combinator when $Yf{\equiv }_{\beta }f(Yf)$ for every term $f$.

Every lambda term $F$ has a fixed point: the termsatisfies $X{\equiv }_{\beta }F(X)$. Equivalently, a fixed-point combinator such assatisfies $YF{\equiv }_{\beta }F(YF)$ for every $F$.

The set of fixed-point combinators is recursively enumerable. Enumerate closed lambda terms and finite proofs of beta equivalence, and output $Y$ whenever a proof of $Yf{\equiv }_{\beta }f(Yf)$ appears for a fresh variable $f$.