Simply typed lambda calculus
From Wikipedia, the free encyclopedia
|
The simply typed lambda calculus (Failed to parse (Missing texvc executable; please see math/README to configure.): \lambda^\to ) is a typed lambda calculus whose only connective is Failed to parse (Missing texvc executable; please see math/README to configure.): \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.
TypesThe types of the simply typed lambda calculus are constructed from base types (or type variables) Failed to parse (Missing texvc executable; please see math/README to configure.): \alpha,\beta,\gamma,\dots , and given types Failed to parse (Missing texvc executable; please see math/README to configure.): \sigma,\tau we can construct Failed to parse (Missing texvc executable; please see math/README to configure.): \sigma \to\tau which denotes the type of functions taking an argument of type Failed to parse (Missing texvc executable; please see math/README to configure.): \sigma and returning a result of type Failed to parse (Missing texvc executable; please see math/README to configure.): \tau . The function-type symbol Failed to parse (Missing texvc executable; please see math/README to configure.): \to associates to the right: we read Failed to parse (Missing texvc executable; please see math/README to configure.): \sigma\to\tau\to\rho as Failed to parse (Missing texvc executable; please see math/README to configure.): \sigma\to(\tau\to\rho) . To each type Failed to parse (Missing texvc executable; please see math/README to configure.): \sigma we assign a number Failed to parse (Missing texvc executable; please see math/README to configure.): o(\sigma) , the order of Failed to parse (Missing texvc executable; please see math/README to configure.): \sigma . For base types we set Failed to parse (Missing texvc executable; please see math/README to configure.): o(\alpha)=0
and for function types we define recursively Failed to parse (Missing texvc executable; please see math/README to configure.): o(\sigma\to\tau)=\mbox{max}(o(\sigma)+1,o(\tau))
. Typing rulesThere are basically two presentations of simply typed lambda calculus. In the first presentation, simply typed lambda calculus is thought 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 informations about their type. This is referred to as typing à la Church. Church-style typingIn the Church presentation of simply typed lambda calculus, a type-annotated lambda term is either
Otherwise said, a typed-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 Failed to parse (Missing texvc executable; please see math/README to configure.): \Gamma,\Delta,\dots which are sets of typing assumptions of the form Failed to parse (Missing texvc executable; please see math/README to configure.): x:\sigma where Failed to parse (Missing texvc executable; please see math/README to configure.): x is a variable. We introduce the judgment Failed to parse (Missing texvc executable; please see math/README to configure.): \Gamma\vdash t : \sigma which means that Failed to parse (Missing texvc executable; please see math/README to configure.): t is a term of type Failed to parse (Missing texvc executable; please see math/README to configure.): \sigma in context Failed to parse (Missing texvc executable; please see math/README to configure.): \Gamma and which is given by the following typing rules :
In other words,
, we know that x has type Failed to parse (Missing texvc executable; please see math/README to configure.): \sigma .
and we have some y which isn't x, then the fact that y has type Failed to parse (Missing texvc executable; please see math/README to configure.): \tau , along with that same context, allows us to infer that x has type Failed to parse (Missing texvc executable; please see math/README to configure.): \sigma . 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).
and t type Failed to parse (Missing texvc executable; please see math/README to configure.): \tau , then we can construct, in the same context, the lambda abstraction Failed to parse (Missing texvc executable; please see math/README to configure.): \lambda x : \sigma. t which then has type Failed to parse (Missing texvc executable; please see math/README to configure.): \sigma \to \tau .
, and u has type Failed to parse (Missing texvc executable; please see math/README to configure.): \sigma , then we can construct the expression Failed to parse (Missing texvc executable; please see math/README to configure.): t\,u , which has type Failed to parse (Missing texvc executable; please see math/README to configure.): \tau . This captures the concept of function application. Examples of closed terms, i.e. terms typable in the empty context, are:
(the I-combinator),
(the K-combinator), and
(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 Failed to parse (Missing texvc executable; please see math/README to configure.): o for the type of propositions and Failed to parse (Missing texvc executable; please see math/README to configure.): \iota for the type of individuals. Frequently the calculus with only one base type, usually Failed to parse (Missing texvc executable; please see math/README to configure.): o , is considered. Terms of the same type are identified via Failed to parse (Missing texvc executable; please see math/README to configure.): \beta\eta -equivalence, which is generated by the equations Failed to parse (Missing texvc executable; please see math/README to configure.): (\lambda x:\sigma.t)\,u =_{\beta} t[x:=u] , where Failed to parse (Missing texvc executable; please see math/README to configure.): t[x:=u] stands for Failed to parse (Missing texvc executable; please see math/README to configure.): t with all free occurrences of Failed to parse (Missing texvc executable; please see math/README to configure.): x replaced by Failed to parse (Missing texvc executable; please see math/README to configure.): u , and Failed to parse (Missing texvc executable; please see math/README to configure.): \lambda x:\sigma.t\,x =_\eta t , if Failed to parse (Missing texvc executable; please see math/README to configure.): x does not appear free in Failed to parse (Missing texvc executable; please see math/README to configure.): t . The simply typed lambda calculus (with Failed to parse (Missing texvc executable; please see math/README to configure.): \beta\eta -equivalence) is the internal language of Cartesian Closed Categories (CCCs), this was first observed by Lambek. Curry-style typingIn Curry-style typing, lambda abstractions carry no type information. As a consequence, terms can have more than one type. One of these type 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 β → α, and λa.λb.a has principal type α → β → α. Otherwise said, 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(bc). Suppose that c has type γ. Then b must have some type of the form γ → β, and the expression bc has the type β. a must have some type of the form β → α, and the expression a(bc) has the type α. Then λc.a(bc) has the type γ → α; λb.λc.a(bc) has the type (γ → β) → γ → α, and λa.λb.λc.a(bc) has the principal type (β → α) → (γ → β) → γ → α. One can interpret this as meaning that when the combinator B receives an argument of type (τ → σ) and an argument of type (ρ → τ), it returns a function, which, given an argument of type ρ, returns a result of type σ. General observationsThe simply typed lambda calculus is closely related to propositional intuitionistic logic using only implication (Failed to parse (Missing texvc executable; please see math/README to configure.): \to ) as a connective (minimal logic) via the Curry-Howard isomorphism: the types inhabited by closed terms are precisely the tautologies of minimal logic. Important results
-reduction is strongly normalizing. As a corollary Failed to parse (Missing texvc executable; please see math/README to configure.): \beta\eta -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.
-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]
(Church numerals). Schwichtenberg showed in 1976 that in Failed to parse (Missing texvc executable; please see math/README to configure.): \lambda^\to exactly the extended polynomials are representable as functions over Church numerals; these are roughly the polynomials closed up under a conditional operator.
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 Failed to parse (Missing texvc executable; please see math/README to configure.): \beta\eta -equivalence, if the base types are interpreted by infinite sets. Statman showed in 1983 that Failed to parse (Missing texvc executable; please see math/README to configure.): \beta\eta -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 Failed to parse (Missing texvc executable; please see math/README to configure.): \beta\eta -equivalence.
References
-definable functionals and Failed to parse (Missing texvc executable; please see math/README to configure.): \beta\eta conversion. Arch. Math. Logik, 23:21--26, 1983.
See alsoExternal links
|
