The simply typed lambda calculus (lambda^ o) is a typed lambda calculus whose only connective is o (function type), thus it is 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 cartesian 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.

= Types =

The types of the simply typed lambda calculus are constructed from base types (or type variables) alpha,eta,gamma,dots and given types sigma, au we can construct sigma o au. Church used only two base types o for the type of propositions and iota for the type of individuals. Frequently the calculus with only one base type, usually o, is considered.

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

= 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:sigma where x is a variable. We introduce the judgment Gammavdash t : sigma which means that t is a term of type sigma in context Gamma which is given by the following typing rules:

{}over{x:sigma vdash x : sigma} {Gammavdash x:sigmaquad x ot=y}over{Gamma.y: au vdash x : sigma} {Gamma.x:sigmavdash t: au}over{Gammavdash lambda x : sigma.t : sigma o au} {Gammavdash t:sigma o auquadGammavdash u:sigma}over{Gammavdash t,u : au}

Examples for closed terms are lambda x:alpha.x : alpha oalpha (I), lambda x:alpha.lambda y:eta.x:alpha o eta o alpha (K) and lambda x:alpha oeta ogamma.lambda y:alpha oeta.lambda z:alpha.x z (y z) : (alpha oeta ogamma) o(alpha oeta) ogamma (S) - 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 ( o) 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 etaeta-equivalence, which is generated by the equations (lambda x:sigma.t),u =_{eta} 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 etaeta-equivalence) is the internal language of Cartesian Closed Categories (CCCs), this was first observed by Joachim Lambek.

= Important results =

= References =