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 Typing rules
3 Important results
4 References
5 See also
6 External links

[edit] Types

The types of the simply typed lambda calculus are constructed from base types (or type variables) $α$ , $β$ , $γ$ , ..., and given types $σ$ , $τ$ we can construct $\sigma \to\tau$ which denotes the type of functions taking an argument of type $σ$ and returning a result of type $τ$ .

The function-type symbol $\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] Typing rules

There are basically two presentations of simply typed lambda calculus. In the first presentation, simply typed lambda calculus is thought of as a subset of lambda calculus and the types come as constraints on the way lambda terms are formed. This is referred to as Curry-style presentation or typing à la Curry and it connects to polymorphic type inference and type assignment systems.

In the second variant, the lambda terms are not pure terms of lambda calculus, but lambda terms carrying information about their type. This is referred to as typing à la Church.

[edit] Church-style typing

In the Church presentation of simply typed lambda calculus, a type-annotated lambda term is either

a variable x
a typed lambda abstraction $λ x :σ. t$
an application $t\;u$

Thus a type-annotated lambda term is like a pure lambda term except that the variables are typed in the abstractions (in the same way as the formal parameters of a function have a type assigned in a language like C).

To define the set of well typed lambda terms of a given type, we introduce typing contexts $\Gamma,\Delta,\dots$ which are sets 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 $Γ$ and 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.

In the original presentation, 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.

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] Curry-style typing

In Curry-style typing, lambda abstractions carry no type information. As a consequence, terms can have more than one type. One of these types is more general than the others and it is called the principal type. The type variables of a principal type are implicitly universally quantified and all possible types of a term are indeed instances of its principal type.

For example, consider again the combinator $K = λ a .λ b . a$ . Suppose that $a$ has type $α$ and $b$ has type $β$ . Then $λ b . a$ has type $\beta \to \alpha$ , and $λ a .λ b . a$ has principal type $\alpha \to \beta \to \alpha$ . In other words, the combinator $K$ takes an argument of arbitrary type $σ$ and returns a function, which, given an argument of type $τ$ , returns a value of type $σ$ .

Similarly, consider the combinator $B = λ a .λ b .λ c . a (b c)$ . Suppose that $c$ has type $γ$ . Then $b$ must have some type of the form $\gamma \to \beta$ , and the expression $b c$ has the type $β$ . $a$ must have some type of the form $\beta \to \alpha$ , and the expression $a (b c)$ has the type $α$ . Then $λ c . a (b c)$ has the type $\gamma \to \alpha$ ; $λ b .λ c . a (b c)$ has the type $(\gamma \to \beta) \to \gamma \to \alpha$ , and $λ a .λ b .λ c . a (b c)$ has the principal type $(\beta \to \alpha) \to (\gamma \to \beta) \to \gamma \to \alpha$ . One can interpret this as meaning that when the combinator $B$ receives an argument of type $(\tau \to \sigma)$ and an argument of type $(\rho \to \tau)$ , it returns a function, which, given an argument of type $ρ$ , returns a result of type $σ$ .

[edit] General observations

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.

[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 (see normalisation by evaluation) was given by Berger and Schwichtenberg 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 Baxter in 1978 then 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-sketch in which he claims that the problem is decidable; however, the complete version of the proof is still unpublished]
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
H. Barendregt, Lambda Calculi with Types, Handbook of Logic in Computer Science, Volume II, Oxford University Press, 1993. ISBN 0198537611.
L. Baxter: The undecidability of the third order dyadic unification problem, Information and Control 38(2), 170-178 (1978)