It is the canonical and simplest example of a typed lambda calculus.
[1] The term simple type is also used to refer to extensions of the simply typed lambda calculus with constructs such as products, coproducts or natural numbers (System T) or even full recursion (like PCF).
In the 1930s Alonzo Church sought to use the logistic method:[a] his lambda calculus, as a formal language based on symbolic expressions, consisted of a denumerably infinite series of axioms and variables,[b] but also a finite set of primitive symbols,[c] denoting abstraction and scope, as well as four constants: negation, disjunction, universal quantification, and selection respectively;[d][e] and also, a finite set of rules I to VI.
[d] Rules I to III are known as alpha, beta, and eta conversion in the lambda calculus.
[f] In 1940 Church settled on a subscript notation for denoting the type in a symbolic expression.
[g] By the 1970s stand-alone arrow notation was in use; for example in this article non-subscripted symbols
For example, it might be assumed that one of the base types is nat, and its term constants could be the natural numbers.
The term syntax, in Backus–Naur form, is variable reference, abstractions, application, or constant: where
Simply typed lambda calculus uses these rules:[h] In words, Examples of closed terms, i.e. terms typable in the empty context, are: These are the typed lambda calculus representations of the basic combinators of combinatory logic.
That is, the order of a type measures the depth of the most left-nested arrow.
Hence: Broadly speaking, there are two different ways of assigning meaning to the simply typed lambda calculus, as to typed languages more generally, variously called intrinsic vs. extrinsic, ontological vs. semantical, or Church-style vs.
In contrast, an extrinsic semantics assigns meaning to terms regardless of typing, as they would be interpreted in an untyped language.
The distinction between intrinsic and extrinsic semantics is sometimes associated with the presence or absence of annotations on lambda abstractions, but strictly speaking this usage is imprecise.
The essential difference between intrinsic and extrinsic approaches is just whether the typing rules are viewed as defining the language, or as a formalism for verifying properties of a more primitive underlying language.
Most of the different semantic interpretations discussed below can be seen through either an intrinsic or extrinsic perspective.
The simply typed lambda calculus (STLC) has the same equational theory of βη-equivalence as untyped lambda calculus, but subject to type restrictions.
The advantage of typed lambda calculus is that STLC allows potentially nonterminating computations to be cut short (that is, reduced).
[9] Likewise, the operational semantics of simply typed lambda calculus can be fixed as for the untyped lambda calculus, using call by name, call by value, or other evaluation strategies.
Additionally, the strong normalization property described below implies that any evaluation strategy will terminate on all simply typed terms.
-equivalence) is the internal language of Cartesian closed categories (CCCs), as was first observed by Joachim Lambek.
[11] Given any CCC, the basic types of the corresponding lambda calculus are the objects, and the terms are the morphisms.
The equational theory is extended likewise, so that one has This last is read as "if t has type 1, then it reduces to nil".
Part of this correspondence can be extended to closed symmetric monoidal categories by using a linear type system.
The simply typed lambda calculus is closely related to the implicational fragment of propositional intuitionistic logic, i.e., the implicational propositional calculus, via the Curry–Howard isomorphism: terms correspond precisely to proofs in natural deduction, and inhabited types are exactly the tautologies of this logic.
Henkin 1996 p. 146 described how Church's logistic method could seek to provide a foundation for mathematics (Peano arithmetic and real analysis),[4] via model theory.
The presentation given above is not the only way of defining the syntax of the simply typed lambda calculus.
The type system is divided into two judgments, representing both checking and synthesis, written
Finally, we explain rules [5] and [6] as follows: Because of these last two rules coercing between synthesis and checking, it is easy to see that any well-typed but unannotated term can be checked in the bidirectional system, so long as we insert "enough" type annotations.
Given the standard semantics, the simply typed lambda calculus is strongly normalizing: every sequence of reductions eventually terminates.
or adding general recursive types, though both eliminate strong normalization.