The simply typed lambda calculus ( λ → {\displaystyle \lambda ^{\to }} ), a form of type theory, is a typed interpretation of the lambda calculus with only one type constructor ( → {\displaystyle \to } ) that builds function types. It is the canonical and simplest example of a typed lambda calculus. The simply typed lambda calculus was originally introduced by Alonzo Church in 1940 as an attempt to avoid paradoxical use of the untyped lambda calculus. 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 contrast, systems that introduce polymorphic types (like System F) or dependent types (like the Logical Framework) are not considered simply typed. The simple types, except for full recursion, are still considered simple because the Church encodings of such structures can be done using only → {\displaystyle \to } and suitable type variables, while polymorphism and dependency cannot.
Syntax In the 1930s Alonzo Church sought to use the logistic method: his lambda calculus, as a formal language based on symbolic expressions, consisted of a denumerably infinite series of axioms and variables, but also a finite set of primitive symbols, denoting abstraction and scope, as well as four constants: negation, disjunction, universal quantification, and selection respectively; and also, a finite set of rules I to VI. This finite set of rules included rule V modus ponens as well as IV and VI for substitution and generalization respectively. Rules I to III are known as alpha, beta, and eta conversion in the lambda calculus. Church sought to use English only as a syntax language (that is, a metamathematical language) for describing symbolic expressions with no interpretations. In 1940 Church settled on a subscript notation for denoting the type in a symbolic expression. In his presentation, Church used only two base types: o {\displaystyle o} for "the type of propositions" and ι {\displaystyle \iota } for "the type of individuals". The type o {\displaystyle o} has no term constants, whereas ι {\displaystyle \iota } has one term constant. Frequently the calculus with only one base type, usually o {\displaystyle o} , is considered. The Greek letter subscripts α {\displaystyle \alpha } , β {\displaystyle \beta } , etc. denote type variables; the parenthesized subscripted ( α β ) {\displaystyle (\alpha \beta )} denotes the function type β → α {\displaystyle \beta \to \alpha } . Church 1940 p.58 used 'arrow or → {\displaystyle \to } ' to denote stands for, or is an abbreviation for. By the 1970s stand-alone arrow notation was in use; for example in this article non-subscripted symbols σ {\displaystyle \sigma } and τ {\displaystyle \tau } can range over types. The infinite number of axioms were then seen to be a consequence of applying rules I to VI to the types (see Peano axioms). Informally, the function type σ → τ {\displaystyle \sigma \to \tau } refers to the type of functions that, given an input of type σ {\displaystyle \sigma } , produce an output of type τ {\displaystyle \tau } . By convention, → {\displaystyle \to } associates to the right: σ → τ → ρ {\displaystyle \sigma \to \tau \to \rho } is read as σ → ( τ → ρ ) {\displaystyle \sigma \to (\tau \to \rho )} . To define the types, a set of base types, B {\displaystyle B} , must first be defined. These are sometimes called atomic types or type constants. With this fixed, the syntax of types is:
τ : := τ → τ ∣ T w h e r e T ∈ B . {\displaystyle \tau \;{{:}{:=}}\;\tau \to \tau \mid T\quad \mathrm {where} \quad T\in B.}
… excerpt ends here. Continue reading the full article.
