Simply typed lambda calculus: Encyclopedia II - Simply typed lambda calculus - Terms

Simply typed lambda calculus - Terms

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

Examples of closed terms are:

• (I),
• (K), and
• (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 () 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 , where t[x: = u] stands for t with all free occurrences of x replaced by u, and , 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.

Adapted from the Wikipedia article "Terms", under the G.N U Free Docmentation License. Please also see http://en.wikipedia.org/wiki