= Lambda calculus
{title2=$\lambda$-calculus}
{wiki}
A <lambda term> is a variable $x$, a <lambda application> $(MN)$, or a <lambda abstraction> $\lambda x.M$. The <lambda abstraction> binds $x$ in $M$ and represents a function whose argument will be substituted for $x$. Computation uses <beta reduction>:
$$
(\lambda x.M)N\longrightarrow_\beta M[x:=N],
$$
where the substitution is <capture-avoiding substitution>. For example, $(\lambda x.x)N$ reduces to $N$, while substituting a free $y$ into $\lambda y.x$ first requires renaming its bound variable, giving $\lambda z.y$ rather than $\lambda y.y$.
The untyped <lambda calculus> allows self-application. If $D=\lambda x.xx$, then $DD$ reduces to itself and has no terminating reduction. Conversely, <Church numerals> encode natural numbers as repeated application: $\lambda f.\lambda x.f(fx)$ represents two. This small syntax supports general computation while making binding, substitution and termination visible. The <simply typed lambda calculus> restricts the allowed <lambda applications> through types.
Back to article page
