Nivel 2 · Tipos simples (λ→)

Las tres reglas de λ→

La página anterior fijó la forma del juicio $\Gamma \vdash M : \sigma$ (Definición 7.51). Para verificar si un $\lambda$ -término es tipable se introduce ahora un sistema de derivación: tres reglas, una por cada forma de término de la Definición 7.50. Un juicio es derivable si se obtiene aplicando estas reglas un número finito de veces. Todo el material sigue a Nederpelt y Geuvers (2014) .

Las reglas de derivación

(variable): una declaración $x : \sigma$ presente en el contexto $\Gamma$ es derivable en ese mismo contexto.

\Gamma \vdash x : \sigma \quad \text{si} \quad (x : \sigma) \in \Gamma.

(aplicación): si $M : \sigma \rightarrow \tau$ y $N : \sigma$ son válidos en el contexto $\Gamma$ , entonces $M N : \tau$ es derivable en el mismo contexto.

\frac{\Gamma \vdash M : \sigma \rightarrow \tau \qquad \Gamma \vdash N : \sigma} {\Gamma \vdash M N : \tau}.

(abstracción): si $M : \tau$ es derivable en el contexto extendido $\Gamma,\ x : \sigma$ , entonces $\lambda x : \sigma .\, M : \sigma \rightarrow \tau$ es derivable en $\Gamma$ .

\frac{\Gamma,\ x : \sigma \vdash M : \tau} {\Gamma \vdash \lambda x : \sigma .\, M : \sigma \rightarrow \tau}.

La notación de fracción se lee de arriba hacia abajo: los juicios sobre la línea son las premisas y el juicio bajo la línea es la conclusión. Vale la pena observar el movimiento de las declaraciones: la regla (aplicación) mantiene el contexto fijo, mientras que la regla (abstracción) retira la declaración $x : \sigma$ del contexto y la convierte en la parte izquierda de un tipo flecha. Las variables libres se pagan con declaraciones; las ligadas, con flechas.

Primera derivación: la función constante

Ejemplo 7.52 (Derivación simbólica de la función «constante»)

Demostrar el juicio:

\vdash \lambda x : \sigma .\, \lambda y : \tau .\, x \;:\; \sigma \rightarrow (\tau \rightarrow \sigma).

Demostración.

Sea $x : \sigma,\ y : \tau$ el contexto inicial.

El objetivo es demostrar el juicio $x : \sigma,\ y : \tau \vdash x : \sigma$ . Se aplica la regla (variable), ya que la declaración $(x : \sigma)$ es un miembro del contexto $\{x : \sigma,\ y : \tau\}$ . Esto establece el juicio inicial: $x : \sigma,\ y : \tau \vdash x : \sigma . \tag{1}$
El objetivo es demostrar $x : \sigma \vdash \lambda y : \tau .\, x : \tau \rightarrow \sigma$ . Usando el juicio (1) como premisa, se aplica la regla (abstracción): se abstrae la variable $y$ , se elimina $y : \tau$ del contexto y se construye un tipo flecha: $\frac{x : \sigma,\ y : \tau \vdash x : \sigma} {x : \sigma \vdash \lambda y : \tau .\, x : \tau \rightarrow \sigma}. \tag{2}$
El objetivo es demostrar el juicio final. Se aplica nuevamente la regla (abstracción), usando ahora el juicio (2) como premisa. Esta vez se abstrae la variable $x$ , eliminando $x : \sigma$ del contexto, que queda vacío: $\frac{x : \sigma \vdash \lambda y : \tau .\, x : \tau \rightarrow \sigma} {\varnothing \vdash \lambda x : \sigma .\, (\lambda y : \tau .\, x) : \sigma \rightarrow (\tau \rightarrow \sigma)}.$

La composición de los pasos (1), (2) y (3) forma el siguiente árbol de derivación, que representa la prueba completa en una única estructura formal:

(x{:}\sigma) \in \{x{:}\sigma,\ y{:}\tau\}

(variable)

x{:}\sigma,\ y{:}\tau \vdash x : \sigma

(abstracción)

x{:}\sigma \vdash \lambda y{:}\tau.\, x \;:\; \tau \to \sigma

(abstracción)

\vdash \lambda x{:}\sigma.\, \lambda y{:}\tau.\, x \;:\; \sigma \to (\tau \to \sigma)

Segunda derivación: las tres reglas juntas

El siguiente ejemplo, tomado de la tesis, ejercita las tres reglas, incluida (aplicación).

Ejemplo 7.53 (Derivación con las tres reglas)

Demostrar el juicio:

\vdash \lambda y : \alpha \rightarrow \beta .\, \lambda z : \alpha .\, y\, z \;:\; (\alpha \rightarrow \beta) \rightarrow (\alpha \rightarrow \beta).

Demostración.

Sea $\Gamma_1 = \{y : \alpha \rightarrow \beta,\ z : \alpha\}$ el contexto inicial.

Para derivar la aplicación $y\, z$ , primero se necesita el tipo de $y$ . En $\Gamma_1$ la declaración $y : \alpha \rightarrow \beta$ está presente, y la regla (variable) se aplica: $y : \alpha \rightarrow \beta,\ z : \alpha \vdash y : \alpha \rightarrow \beta . \tag{1}$
De manera similar se necesita el tipo de $z$ . En el mismo contexto $\Gamma_1$ la declaración $z : \alpha$ está presente, por lo que la regla (variable) se aplica de nuevo: $y : \alpha \rightarrow \beta,\ z : \alpha \vdash z : \alpha . \tag{2}$
Con los juicios (1) y (2) como premisas, la regla (aplicación) combina la función y su argumento para producir el resultado: $\frac{\Gamma_1 \vdash y : \alpha \rightarrow \beta \qquad \Gamma_1 \vdash z : \alpha} {\Gamma_1 \vdash y\, z : \beta}. \tag{3}$
El objetivo es demostrar $y : \alpha \rightarrow \beta \vdash \lambda z : \alpha .\, y\, z : \alpha \rightarrow \beta$ . Usando el juicio (3) como premisa, se aplica la regla (abstracción) para la variable $z$ , lo que elimina $z : \alpha$ del contexto: $\frac{y : \alpha \rightarrow \beta,\ z : \alpha \vdash y\, z : \beta} {y : \alpha \rightarrow \beta \vdash \lambda z : \alpha .\, y\, z : \alpha \rightarrow \beta}. \tag{4}$
Para demostrar el juicio original se aplica la regla (abstracción) por última vez, usando el juicio (4) como premisa para abstraer la variable $y$ . Esto elimina $y : \alpha \rightarrow \beta$ y deja el contexto vacío: $\frac{y : \alpha \rightarrow \beta \vdash \lambda z : \alpha .\, y\, z : \alpha \rightarrow \beta} {\varnothing \vdash \lambda y : \alpha \rightarrow \beta .\, (\lambda z : \alpha .\, y\, z) : (\alpha \rightarrow \beta) \rightarrow (\alpha \rightarrow \beta)}.$

Notación de banderas

Una alternativa para evitar la repetición de declaraciones en los contextos es la notación de banderas: las declaraciones se presentan en recuadros (las «banderas») y se asume que forman parte del contexto de todos los juicios escritos bajo ellas. El mismo ejemplo se reescribe, siguiendo el ejemplo 2.4.6 de Nederpelt y Geuvers (2014) , así:

(1)	$y : \alpha \to \beta$	introducción de y
(2)	$z : \alpha$	introducción de z
(3)	$y : \alpha \to \beta$	(variable) en (1)
(4)	$z : \alpha$	(variable) en (2)
(5)	$y\,z : \beta$	(aplicación) en (3) y (4)
(6)	$\lambda z{:}\alpha.\, y\,z \;:\; \alpha \to \beta$	(abstracción) en (5)
(7)	$\lambda y{:}\alpha{\to}\beta.\, \lambda z{:}\alpha.\, y\,z \;:\; (\alpha \to \beta) \to \alpha \to \beta$	(abstracción) en (6)

Este formato resulta más compacto y fácil de leer, especialmente para derivaciones complejas. En general, la notación de banderas equivale a la notación lineal y de árbol por medio de la siguiente relación: cada línea derivada dentro de las banderas es el juicio cuyo contexto son las banderas abiertas en ese punto,

\begin{array}{lll} (\text{Paso 1}) & \text{es equivalente a} & (1), (2) \vdash (3) \\ (\text{Paso 2}) & \text{es equivalente a} & (1), (2) \vdash (4) \\ (\text{Paso 3}) & \text{es equivalente a} & (1), (2) \vdash (5) \\ (\text{Paso 4}) & \text{es equivalente a} & (1) \vdash (6) \\ (\text{Paso 5}) & \text{es equivalente a} & \varnothing \vdash (7) \end{array}

donde «Paso $k$ » denota el $k$ -ésimo paso de derivación (las líneas (3) a (7)).

Explóralo tú mismo

El siguiente widget contiene exactamente la derivación del Ejemplo 7.53 y, como calentamiento, la de la función identidad. Cada juicio puede expandirse hacia arriba hasta sus premisas, y el botón de la esquina alterna entre la presentación de árbol y la de banderas: son la misma derivación.

Explorador de derivaciones de tipado (λ→)

Se parte de la conclusión; pulsa «+» para preguntar de dónde sale cada juicio (leyendo las reglas de abajo hacia arriba).

\vdash \lambda x{:}\sigma.\, x \;:\; \sigma \to \sigma

Pasa el cursor por el nombre de una regla para ver su esquema. Las dos vistas presentan la MISMA derivación.

Términos legales

Con el sistema de derivación disponible, la noción de «estar bien tipado» adquiere su forma definitiva.

Definición 7.54 (Término legal)

Un término pre-tipado $M$ en $\lambda\rightarrow$ se denomina legal si existen un contexto $\Gamma$ y un tipo $\rho$ tales que

\Gamma \vdash M : \rho .

El lema de variables libres

La primera propiedad general de $\lambda\rightarrow$ conecta la sintaxis pura (el conjunto $FV$ de la Definición 7.10) con el sistema de tipado (el dominio de un contexto, de la Definición 7.55).

Lema 7.57 (Variables libres)

Si $\Gamma \vdash L : \sigma$ , entonces el conjunto de variables libres de $L$ es un subconjunto del dominio de $\Gamma$ , es decir, $FV(L) \subseteq \operatorname{dom}(\Gamma)$ .

Esto garantiza que cada variable libre en un término legal tiene un tipo asignado explícitamente en el contexto de tipado.

Demostración.

A probar: $FV(L) \subseteq \operatorname{dom}(\Gamma)$ . La prueba se realiza por inducción estructural sobre la derivación de $\Gamma \vdash L : \sigma$ . Para cada caso se analiza la forma del término $L$ y la regla de tipado que lo justifica.

(Variable). El término es $L \equiv x$ $L \equiv x$ . La forma del juicio es $\Gamma \vdash x : \sigma$ $Γ ⊢ x : σ$ .
- Por regla de (variable): la validez de este juicio exige que la declaración $(x : \sigma)$ esté en el contexto $\Gamma$ .
- Por definición de dominio: si $(x : \sigma) \in \Gamma$ , se sigue que $x \in \operatorname{dom}(\Gamma)$ .
- Por la Definición 7.10, cláusula de variables: el conjunto de variables libres para una variable es $FV(x) = \{x\}$ .
- Por lo tanto, se concluye directamente que $FV(x) \subseteq \operatorname{dom}(\Gamma)$ .
(Aplicación). El término es $L \equiv M N$ $L \equiv M N$ . La forma del juicio es $\Gamma \vdash M N : \tau$ $Γ ⊢ M N : τ$ .
- Por regla de (aplicación): este juicio se deriva de dos premisas con el mismo contexto: $\Gamma \vdash M : \sigma \rightarrow \tau \quad \text{y} \quad \Gamma \vdash N : \sigma .$
- Hipótesis de inducción (H.I.): la propiedad se asume válida para las derivaciones de las premisas: $FV(M) \subseteq \operatorname{dom}(\Gamma) \quad \text{y} \quad FV(N) \subseteq \operatorname{dom}(\Gamma).$
- Por lo tanto, aplicando la cláusula de aplicación de la Definición 7.10 y la H.I.: $FV(M N) = FV(M) \cup FV(N) \subseteq \operatorname{dom}(\Gamma) \cup \operatorname{dom}(\Gamma) = \operatorname{dom}(\Gamma).$
(Abstracción). El término es $L \equiv \lambda x : \sigma .\, M$ $L \equiv λ x : σ . M$ . La forma del juicio es $\Gamma \vdash L : \sigma \rightarrow \tau$ $Γ ⊢ L : σ \to τ$ .
- Por regla de (abstracción): este juicio se deriva de la premisa $\Gamma,\ x : \sigma \vdash M : \tau$ .
- Hipótesis de inducción (H.I.): la propiedad se asume válida para la derivación de la premisa: $FV(M) \subseteq \operatorname{dom}(\Gamma,\ x : \sigma).$
- Por lo tanto, aplicando la cláusula de abstracción de la Definición 7.10 y el hecho de que $\operatorname{dom}(\Gamma,\ x : \sigma) = \operatorname{dom}(\Gamma) \cup \{x\}$ : $FV(\lambda x : \sigma .\, M) = FV(M) \setminus \{x\} \subseteq (\operatorname{dom}(\Gamma) \cup \{x\}) \setminus \{x\} = \operatorname{dom}(\Gamma).$

Por lo tanto, $FV(L) \subseteq \operatorname{dom}(\Gamma)$ .

Las derivaciones de esta página anotaron cada abstracción con su tipo, al estilo de Church. La página siguiente examina esa decisión de diseño y su alternativa, el estilo de Curry, en el que los tipos se infieren en lugar de declararse.