Simply typed lambda calculus

From Wikipedia, the free encyclopedia

The simply typed lambda calculus ( $\lambda^\to$ ) is a typed lambda calculus whose only connective is $\to$ (function type). This makes it the canonical, and in many ways simplest, example of a typed lambda calculus.

The word simple types is also used to refer to extensions of the simply typed lambda calculus such as products, coproducts or natural numbers (System T) or even full recursion (like PCF). In contrast, systems which introduce polymorphic types (like System F) or dependent types (like the Logical Framework) are not considered simply typed. The simply typed lambda calculus was originally introduced by Alonzo Church in 1940 as an attempt to avoid paradoxical uses of the untyped lambda calculus.

1 Types
2 Terms
3 Important results
4 References

[edit] Types

The types of the simply typed lambda calculus are constructed from base types (or type variables) $\alpha,\beta,\gamma,\dots$ and given types $σ,τ$ we can construct $\sigma \to\tau$ . Church used only two base types $o$ for the type of propositions and $ι$ for the type of individuals. Frequently the calculus with only one base type, usually $o$ , is considered.

$\to$ associates to the right: we read $\sigma\to\tau\to\rho$ as $\sigma\to(\tau\to\rho)$ . To each type $σ$ we assign a number $o (σ)$ , the order of $σ$ . For base types we set $o (α) = 0$ and for function types we define recursively $o(\sigma\to\tau)=\mbox{max}(o(\sigma)+1,o(\tau))$ .

[edit] Terms

To define the set of well typed lambda terms of a given type, we introduce typing contexts $\Gamma,\Delta,\dots$ which are sequences of typing assumptions of the form $x :σ$ where $x$ is a variable. We introduce the judgment $\Gamma\vdash t : \sigma$ which means that $t$ is a term of type $σ$ in context $Γ$ which is given by the following typing rules:

${}\over{x:\sigma \vdash x : \sigma }$ (1)	${\Gamma\vdash x:\sigma\quad x\not=y}\over{\Gamma.y:\tau \vdash x : \sigma}$ (2)
${\Gamma.x:\sigma\vdash t:\tau}\over{\Gamma\vdash \lambda x : \sigma.t : \sigma \to \tau}$ (3)	${\Gamma\vdash t:\sigma\to\tau\quad\Gamma\vdash u:\sigma}\over{\Gamma\vdash t\,u : \tau}$ (4)

In other words,

If x has type $σ$ , we know that x has type $σ$ .
If in a certain context x has type $σ$ and we have some y which isn't x, then the fact that y has type $τ$ , along with that same context, allows us to infer that x has type $σ$ . Even more clearly, adding a new value to a context doesn't change existing ones (provided that the new value isn't the same as one of the previous ones).
If, in a certain context, x has type $σ$ and t type $τ$ , then we can construct, in the same context, the lambda abstraction $λ x :σ. t$ which then has type $\sigma \to \tau$ .
If, in a certain context, t has type $\sigma \to \tau$ , and u has type $σ$ , then we can construct the expression $t\,u$ , which has type $τ$ . This captures the concept of function application.

Examples of closed terms, i.e. terms typable in the empty context, are:

$\lambda x:\alpha.x : \alpha\to\alpha$ (the I-combinator),
$\lambda x:\alpha.\lambda y:\beta.x:\alpha \to \beta \to \alpha$ (the K-combinator), and
$\lambda x:\alpha\to\beta\to\gamma.\lambda y:\alpha\to\beta.\lambda z:\alpha.x z (y z) : (\alpha\to\beta\to\gamma)\to(\alpha\to\beta)\to\alpha\to\gamma$ (the S-combinator).

These are the typed lambda calculus representations of the basic combinators of combinatory logic.

The simply typed lambda calculus is closely related to propositional intuitionistic logic using only implication ( $\to$ ) as a connective (minimal logic) via the Curry-Howard isomorphism: the types inhabited by closed terms are precisely the tautologies of minimal logic.

Terms of the same type are identified via $βη$ -equivalence, which is generated by the equations $(\lambda x:\sigma.t)\,u =_{\beta} t[x:=u]$ , where $t [x : = u]$ stands for $t$ with all free occurrences of $x$ replaced by $u$ , and $\lambda x:\sigma.t\,x =_\eta t$ , if $x$ does not appear free in $t$ . The simply typed lambda calculus (with $βη$ -equivalence) is the internal language of Cartesian Closed Categories (CCCs), this was first observed by Lambek.

[edit] Important results

Tait showed in 1967 that $β$ -reduction is strongly normalizing. As a corollary $βη$ -equivalence is decidable. Statman showed in 1977 that the normalisation problem is not elementary recursive. A purely semantic normalisation proof was given by Berger and Schwichtenberg (Normalisation by evaluation) in 1991.
The unification problem for $βη$ -equivalence is undecidable. Huet showed in 1973 that 3rd order unification is undecidable and this was improved upon by Goldfarb in 1981 by showing that 2nd order unification is already undecidable. Whether higher order matching (unification where only one term contains existential variables) is decidable is still open. [2006: Colin Stirling, Edinburgh, has published a proof showing that it is decidable]
We can encode natural numbers by terms of the type $(o\to o)\to(o \to o)$ (Church numerals). Schwichtenberg showed in 1976 that in $\lambda^\to$ exactly the extended polynomials are representable as functions over Church numerals; these are roughly the polynomials closed up under a conditional operator.
A full model of $\lambda^\to$ is given by interpreting base types as sets and function types by the set-theoretic function space. Friedman showed in 1975 that this interpretation is complete for $βη$ -equivalence, if the base types are interpreted by infinite sets. Statman showed in 1983 that $βη$ -equivalence is the maximal equivalence which is typically ambiguous,i.e. closed under type substitutions (Statman's Typical Ambiguity Theorem). A corollary of this is that the finite model property holds, i.e. finite sets are sufficient to distinguish terms which are not identified by $βη$ -equivalence.
Plotkin introduced logical relations in 1973 to characterize the elements of a model which are definable by lambda terms. In 1993 Jung and Tiuryn showed that a general form of logical relation (Kripke logical relations with varying arity) exactly characterizes lambda definability. Plotkin and Statman conjectured that it is decidable whether a given element of a model generated from finite sets is definable by a lambda term (Plotkin-Statman-conjecture). The conjecture was shown to be false by Loader in 1993.

[edit] References

A. Church: A Formulation of the Simple Theory of Types, JSL 5, 1940
W.W.Tait: Intensional Interpretations of Functionals of Finite Type I, JSL 32(2), 1967
G.D. Plotkin: Lambda-definability and logical relations, Technical report, 1973
G.P. Huet: The Undecidability of Unification in Third Order Logic Information and Control 22(3): 257-267 (1973)
H. Friedman: Equality between functionals. LogicColl. '73, pages 22-37, LNM 453, 1975.
H. Schwichtenberg: Functions definable in the simply-typed lambda calculus, Arch. Math Logik 17 (1976) 113-114.
R. Statman: The Typed lambda-Calculus Is not Elementary Recursive FOCS 1977: 90-94
W. D. Goldfarb: The undecidability of the 2nd order unification problem, TCS (1981), no. 13, 225- 230.
R. Statman. $λ$ -definable functionals and $βη$ conversion. Arch. Math. Logik, 23:21--26, 1983.
J. Lambek: Cartesian Closed Categories and Typed Lambda-calculi. Combinators and Functional Programming Languages 1985: 136-175
U. Berger, H. Schwichtenberg: An Inverse of the Evaluation Functional for Typed lambda-calculus LICS 1991: 203-211
Jung, A.,Tiuryn, J.:A New Characterization of Lambda Definability, TLCA 1993
R. Loader: The Undecidability of λ-definability, appeared in the Church Festschrift, 2001