Definition
The simply-typed lambda calculus (often denoted ) is the fragment of lambda calculus in which every term is assigned a type and function abstraction must specify the type of its argument. It is the basic typed calculus built from variables, application, abstraction, and function types.
Unlike the untyped lambda calculus, not every term is permitted. The typing rules exclude self-application terms such as , and with the usual function types alone the system has no general recursion.
Judgments
Let be a discrete set of base types. The simply-typed lambda calculus can be presented by judgments for type formation, context formation, and typing.
The type formation judgments are
\qquad \dfrac{A \in \mathbf{B}}{A \; \mathrm{type}}$$ Contexts are formed by the rules $$\dfrac{}{\varnothing \; \mathrm{ctx}} \qquad \dfrac{\Gamma \; \mathrm{ctx} \qquad A \; \mathrm{type}}{\Gamma, x:A \; \mathrm{ctx}}$$ Terms are then introduced only through typing judgments of the form $\Gamma \vdash t : A$. ## Typing rules Typing judgments have the form $\Gamma \vdash t : A$, where $\Gamma$ is a context assigning types to free variables. The basic rules are: $$\dfrac{x:A \in \Gamma}{\Gamma \vdash x : A}$$ $$\dfrac{\Gamma, x:A \vdash t : B}{\Gamma \vdash \lambda x:A.\; t : A \to B}$$ $$\dfrac{\Gamma \vdash t : A \to B \qquad \Gamma \vdash u : A}{\Gamma \vdash t\,u : B}$$ These rules express that abstraction introduces a function type and application eliminates one. ## Example The identity function is typable as $$\vdash \lambda x:A.\; x : A \to A.$$ Similarly, function composition can be typed as $$\vdash \lambda f:B \to C.\; \lambda g:A \to B.\; \lambda x:A.\; f\,(g\,x) : (B \to C) \to (A \to B) \to A \to C.$$ ## Properties The simply-typed lambda calculus has several fundamental metatheoretic properties. - *Preservation*: if $\Gamma \vdash t : A$ and $t \to t'$, then $\Gamma \vdash t' : A$. - *Progress*: a closed well-typed term is either a value or can take a reduction step. - *Strong normalization*: every well-typed term reduces in finitely many steps to a normal form. Because of strong normalization, the pure simply-typed lambda calculus does not define arbitrary recursive functions. ## Curry-Howard Under the [[Curry-Howard Correspondence]], the simply-typed lambda calculus corresponds to the implicational fragment of [[Propositional Logic#intuitionistic-fragment|intuitionistic propositional logic]]. Types correspond to propositions and terms correspond to proofs. ## Related Concepts - [[Lambda Calculus]] - [[Type Theory]] - [[Function Type]] - [[Curry-Howard Correspondence]] - [[barendregt1992-typed-lambda-calculus]]