Càlcul lambda simplement tipado

El càlcul lambda simplement tipado (${\lambda }^{\to }$) és una teoria de tipos basada en el càlcul de lambda en un únic constructor de tipos, $\to$, que construïx tipos funció. És l'eixemple canònic i més senzill d'un càlcul lambda tipado. El càlcul lambda simplement tipado va ser originalment introduït per Alonzo Church en el 1940 com un intent d'evitar l'aparició de paradoxes en el càlcul lambda sense tipos.

El terme simplement tipado és també utilisat per a referir-se a extensions del càlcul lambda simplement tipado en productes, coproductos, número natural (Sistema T) o inclús recursión (com en el llenguage PCF). En contrast, els sistemes que introduïxen tipos polimòrfics (com Sistema F) o tipos depenents (com el Logical Framework) no es consideren simplement tipados. Els primers, llevat aquells que implementen recursión arbitrària, es consideren encara simplement tipados perque la codificació de Church d'estes estructures pot fer-se utilisant solament $\to$ i variables de tipo, mentres que el polimorfisme i la dependència no poden expressar-se d'esta forma.

Sintaxis

Sean $\sigma$ i $\tau$ dos variables representant tipos arbitraris. Informalment, el tipo funció $\sigma \to \tau$ és el tipo de les funcions que, donat un argument de tipo $\sigma$, produïxen una eixida de tipo $\tau$. Per convenció, $\to$ és associatiu a dreta: llegim $\sigma \to \tau \to \rho$ com $\sigma \to (\tau \to \rho )$.

Per a definir els tipos, vàrem escomençar fixant un conjunt de tipos base, $B$, en ocasions cridats tipos atòmics o constants de tipo. Una volta fixats, la sintaxis dels tipos ve donada per la següent BNF:

$\tau ::=\tau \to \tau \mid T\mathrm{d}\mathrm{o}\mathrm{n}\mathrm{d}\mathrm{e}T\in B$.

La sintaxis dels térmens del càlcul lambda simplement tipado és essencialment la mateixa que la del càlcul lambda. Escrivim $x:\tau$ per a denotar que la variable $x$ és de tipo $\tau$. La sintaxis dels térmens en BNF és llavors:

$e::=x\mid \lambda x:\tau .e\mid ee\mid c$

a on $c$ és una constant.

Semàntica categòrica

El càlcul lambda simplement tipado (assumint $\beta \eta$-equivalència) és el llenguage intern de les categories cartesianas tancades, com va ser observat per Joachim Lambek per primera volta. Donada qualsevol categoria cartesiana tancada específica, els tipos base del seu corresponent càlcul lambda són les seues objectes, i els térmens són els morfismos. En l'atra direcció, cada càlcul lambda simplement tipado genera una categoria cartesiana tancada els objectes de la qual són els tipos, i que els seus morfismos són classes d'equivalència sobre els térmens.

Referències

• 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. $\lambda$-definable functionals and $\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, ^{[enllaç trencat]}, Handbook of Logic in Computer Science, Volume II, Oxford University Press, 1993. ISBN 0-19-853761-1.

Isbn

1

0-19-853761-1

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