= Simply typed lambda calculus
{title2=$\lambda^{\to}$}
{wiki}
In the <simply typed lambda calculus>, types are generated from base types by the arrow constructor $A\to B$. A context $\Gamma$ assigns types to variables. Its basic rules are
$$
\frac{x:A\in\Gamma}{\Gamma\vdash x:A},\qquad
\frac{\Gamma,x:A\vdash M:B}{\Gamma\vdash\lambda x.M:A\to B},\qquad
\frac{\Gamma\vdash M:A\to B\quad\Gamma\vdash N:A}{\Gamma\vdash MN:B}.
$$
Thus <lambda abstraction> creates a function type and <lambda application> consumes its input type. For example, $\lambda x.x$ has type $A\to A$, and $\lambda f.\lambda x.fx$ has type $(A\to B)\to A\to B$.
The untyped self-application $xx$ would require one finite type to satisfy $A=A\to B$, which is impossible in this type grammar. This excludes the familiar looping term $(\lambda x.xx)(\lambda x.xx)$; more generally the <Strong normalization theorem for simply typed lambda calculus> says that every reduction sequence from a well-typed term terminates. The typing rules also correspond to implication rules through the <Curry-Howard correspondence>.
Back to article page
