Cálculo lambda simplemente tipado

Sean ${\displaystyle \sigma }$ y ${\displaystyle \tau }$ dos variables representando tipos arbitrarios. Informalmente, el tipo función ${\displaystyle \sigma \to \tau }$ es el tipo de las funciones que, dado un argumento de tipo ${\displaystyle \sigma }$, producen una salida de tipo ${\displaystyle \tau }$. Por convención, ${\displaystyle \to }$ es asociativo a derecha: leemos ${\displaystyle \sigma \to \tau \to \rho }$ como ${\displaystyle \sigma \to (\tau \to \rho )}$.

Para definir los tipos, empezamos fijando un conjunto de tipos base, ${\displaystyle B}$, en ocasiones llamados tipos atómicos o constantes de tipo. Una vez fijados, la sintaxis de los tipos viene dada por la siguiente BNF:

${\displaystyle \tau$ ::=\tau \to \tau \mid T\quad \mathrm {donde} \quad T\in B} .

La sintaxis de los términos del cálculo lambda simplemente tipado es esencialmente la misma que la del cálculo lambda. Escribimos ${\displaystyle x{:}\tau }$ para denotar que la variable ${\displaystyle x}$ es de tipo ${\displaystyle \tau }$. La sintaxis de los términos en BNF es entonces:

${\displaystyle e::=x\mid \lambda x{\mathbin {:}}\tau .e\mid e\,e\mid c}$

donde ${\displaystyle c}$ es una constante.

El cálculo lambda simplemente tipado (asumiendo ${\displaystyle \beta \eta }$-equivalencia) es el lenguaje interno de las categorías cartesianas cerradas, como fue observado por Joachim Lambek por primera vez. Dada cualquier categoría cartesiana cerrada específica, los tipos base de su correspondiente cálculo lambda son sus objetos, y los términos son los morfismos. En la otra dirección, cada cálculo lambda simplemente tipado genera una categoría cartesiana cerrada cuyos objetos son los tipos, y cuyos morfismos son clases de equivalencia sobre los términos.

• A. Church: A Formulation of the Simple Theory of Types, JSL 5, 1940
• W.W.Tait: Intensional Interpretations of Functionals of Finite Type I, JSL 32(2), 1967
• G.D. Plotkin: Lambda-definability and logical relations, Technical report, 1973
• G.P. Huet: The Undecidability of Unification in Third Order Logic Information and Control 22(3): 257-267 (1973)
• H. Friedman: Equality between functionals. LogicColl. '73, pages 22-37, LNM 453, 1975.
• H. Schwichtenberg: Functions definable in the simply-typed lambda calculus, Arch. Math Logik 17 (1976) 113-114.
• R. Statman: The Typed lambda-Calculus Is not Elementary Recursive FOCS 1977: 90-94
• W. D. Goldfarb: The undecidability of the 2nd order unification problem, TCS (1981), no. 13, 225- 230.
• R. Statman. ${\displaystyle \lambda }$-definable functionals and ${\displaystyle \beta \eta }$ conversion. Arch. Math. Logik, 23:21–26, 1983.
• J. Lambek: Cartesian Closed Categories and Typed Lambda-calculi. Combinators and Functional Programming Languages 1985: 136-175
• U. Berger, H. Schwichtenberg: An Inverse of the Evaluation Functional for Typed lambda-calculus LICS 1991: 203-211
• H. Mairson: A simple proof of a theorem of Statman, TCS 103(2):387-394, 1992.
• Jung, A.,Tiuryn, J.:A New Characterization of Lambda Definability, TLCA 1993
• R. Loader: The Undecidability of λ-definability, appeared in the Church Festschrift, 2001
• H. Barendregt, Lambda Calculi with Types, Handbook of Logic in Computer Science, Volume II, Oxford University Press, 1993. ISBN 0-19-853761-1.

• L. Baxter: The undecidability of the third order dyadic unification problem, Information and Control 38(2), 170-178 (1978)