Cálculo lambda simplemente tipado
# Cálculo lambda simplemente tipado

El cálculo lambda simplemente tipado ($\lambda ^{\to }$) es una teoría de tipos basada en el cálculo de lambda con un único constructor de tipos, $\to$, que construye tipos función. Es el ejemplo canónico y más sencillo de un cálculo lambda tipado. El cálculo lambda simplemente tipado fue originalmente introducido por Alonzo Church en el 1940 como un intento de evitar la aparición de paradojas en el cálculo lambda sin tipos.

El término simplemente tipado es también utilizado para referirse a extensiones del cálculo lambda simplemente tipado con productos, coproductos, números naturales (Sistema T) o incluso recursión (como en el lenguaje PCF). En contraste, los sistemas que introducen tipos polimórficos (como Sistema F) o tipos dependientes (como el Logical Framework) no se consideran simplemente tipados. Los primeros, excepto aquellos que implementan recursión arbitraria, se consideran todavía simplemente tipados porque la codificación de Church de estas estructuras puede hacerse utilizando solamente $\to$ y variables de tipo, mientras que el polimorfismo y la dependencia no pueden expresarse de esta forma.

## Sintaxis

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

Para definir los tipos, empezamos fijando un conjunto de tipos base, $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:

    $\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 $x{:}\tau$ para denotar que la variable $x$ es de tipo $\tau$. La sintaxis de los términos en BNF es entonces:

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

donde $c$ es una constante.

## Semántica categórica

El cálculo lambda simplemente tipado (asumiendo $\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.

