Nivel 2 · Tipos simples (λ→)

Juicios y contextos

El módulo anterior cerró con un anticipo del cálculo lambda simplemente tipado $\lambda\rightarrow$ : los tipos simples (Definición 7.45), los términos tipables (Definición 7.48), los términos pre-tipados (Definición 7.50) y la forma del juicio de tipado (Definición 7.51). Este módulo desarrolla $\lambda\rightarrow$ en detalle, siguiendo a Nederpelt y Geuvers (2014) . La pregunta que lo organiza es doble: qué significa exactamente la afirmación «el término $M$ tiene el tipo $\sigma$ », y cómo se demuestra. Esta página fija el lenguaje de las afirmaciones; la siguiente presenta las reglas que las derivan.

Los tipos, de un vistazo

El conjunto $\mathbb{T}$ de tipos simples de la

Definición 7.45

se escribe en forma compacta (estilo BNF) como

\sigma, \tau ::= \alpha \mid (\sigma \rightarrow \tau),

donde $\alpha$ recorre el conjunto infinito $\mathbb{V}$ de variables de tipo. Las letras griegas $\alpha, \beta, \gamma, \ldots$ denotan variables de tipo; los símbolos $\sigma, \tau, \ldots$ denotan tipos simples arbitrarios; los paréntesis externos se omiten y la flecha agrupa por la derecha: $\alpha \rightarrow \beta \rightarrow \gamma$ abrevia $\alpha \rightarrow (\beta \rightarrow \gamma)$ . La interpretación es la esperada:

las variables de tipo ( $\alpha, \beta, \ldots$ ) representan tipos básicos, como $\mathtt{nat}$ para los números naturales o $\mathtt{list}$ para las listas;
los tipos flecha ( $\sigma \rightarrow \tau$ ) representan funciones, como $\mathtt{nat} \rightarrow \mathtt{real}$ , el conjunto de funciones de naturales a reales.

Nota 7.47 (Lectura del símbolo «:»)

El símbolo « $:$ » se utiliza para denotar que un término tiene un tipo específico. Por ejemplo:

$M : \sigma$ significa que el término $M$ es de tipo $\sigma$ ;
$x : \sigma$ significa que $x$ es una variable de tipo $\sigma$ ;
$\lambda x .\, M : \sigma \rightarrow \tau$ significa que la función $\lambda x .\, M$ toma un argumento de tipo $\sigma$ y devuelve un resultado de tipo $\tau$ ;
$M N : \tau$ significa que la aplicación de $M$ a $N$ produce un resultado de tipo $\tau$ .

De los enunciados a los juicios

Las cuatro nociones que estructuran todo el sistema ya fueron definidas en la Definición 7.51; conviene repasarlas con calma, porque el resto del módulo las usa sin pausa.

Un enunciado tiene la forma $M : \sigma$ , con $M \in \Lambda_{\mathbb{T}}$ un término pre-tipado y $\sigma \in \mathbb{T}$ un tipo simple; $M$ es el sujeto y $\sigma$ el tipo. Por ejemplo, $\lambda x : \alpha .\, x : \alpha \rightarrow \alpha$ es un enunciado.
Una declaración es un enunciado cuyo sujeto es una variable, como $x : \sigma$ .
Un contexto $\Gamma$ es una lista de declaraciones con sujetos distintos: $\Gamma \equiv x_1 : \sigma_1,\ x_2 : \sigma_2,\ \ldots,\ x_n : \sigma_n .$ El contexto vacío se denota $\varnothing$ .
Un juicio tiene la forma $\Gamma \vdash M : \sigma$ , con $\Gamma$ un contexto y $M : \sigma$ un enunciado.

El juicio $\Gamma \vdash M : \sigma$ se lee en voz alta así: «asumiendo las declaraciones del contexto $\Gamma$ , el término $M$ tiene el tipo $\sigma$ ». El símbolo $\vdash$ separa las suposiciones (los tipos asignados a las variables libres) de la afirmación demostrada (el enunciado $M : \sigma$ ). Un contexto no es un adorno: sin conocer los tipos de las variables libres de $M$ , en general no puede asignarse tipo alguno a $M$ .

Nota (Dos torniquetes distintos)

El símbolo $\vdash$ (el torniquete) reaparecerá en el módulo 3 con un significado distinto. En la Definición 9.3, $\Gamma$ es un conjunto de fórmulas proposicionales y $\Gamma \vdash \varphi$ afirma que la fórmula $\varphi$ es derivable a partir de $\Gamma$ mediante deducción natural . Aquí, en cambio, $\Gamma$ es una lista de declaraciones de variables y lo que se deriva es un enunciado de tipado $M : \sigma$ . Son dos relaciones definidas sobre objetos diferentes y no deben confundirse. La coincidencia tipográfica, sin embargo, no es casual: la correspondencia de Curry–Howard identificará ambas lecturas de manera precisa (Definición 7.60).

Anatomía de un contexto

Los contextos son listas finitas y admiten las operaciones de manipulación habituales. Las siguientes cuatro nociones son la contabilidad básica con la que se enuncian las propiedades generales de $\lambda\rightarrow$ .

Definición 7.55 (Propiedades de contextos)

Considérese:

Dominio ( $\operatorname{dom}$ ): el dominio de un contexto $\Gamma$ , escrito $\operatorname{dom}(\Gamma)$ , es la secuencia ordenada de las variables declaradas en él. Así, para $\Gamma \equiv x_1 : \sigma_1, \ldots, x_n : \sigma_n$ , su dominio es $(x_1, \ldots, x_n)$ .
Subcontexto ( $\subseteq$ ): un contexto $\Gamma'$ es subcontexto de $\Gamma$ si cada declaración en $\Gamma'$ también existe en $\Gamma$ , manteniendo el mismo orden.
Permutación: un contexto $\Gamma'$ es una permutación de $\Gamma$ si ambos contextos están compuestos por el mismo conjunto de declaraciones, sin importar el orden en que aparecen.
Proyección ( $\upharpoonright$ ): la proyección de un contexto $\Gamma$ sobre un conjunto de variables $\Phi$ , escrita $\Gamma \upharpoonright \Phi$ , produce un subcontexto de $\Gamma$ que contiene exclusivamente las declaraciones de $\Gamma$ cuyas variables son miembros de $\Phi$ . Formalmente, el dominio del nuevo contexto es la intersección $\operatorname{dom}(\Gamma) \cap \Phi$ .

Ejemplo 7.56 (Dominio, subcontexto, permutación y proyección)

Dado el contexto $\Gamma \equiv y : \sigma,\ x_1 : \rho_1,\ x_2 : \rho_2,\ z : \tau,\ x_3 : \rho_3$ :

Su dominio es $\operatorname{dom}(\Gamma) = (y, x_1, x_2, z, x_3)$ . El dominio del contexto vacío, $\operatorname{dom}(\varnothing)$ , es la lista vacía, $()$ .
La relación de subcontexto se ilustra con $\varnothing \subseteq (x_1 : \rho_1,\ z : \tau) \subseteq \Gamma$ .
Un reordenamiento como $x_2 : \rho_2,\ x_1 : \rho_1,\ z : \tau,\ x_3 : \rho_3,\ y : \sigma$ es una permutación de $\Gamma$ .
La proyección de $\Gamma$ sobre el conjunto $\{z, u, x_1\}$ resulta en $x_1 : \rho_1,\ z : \tau$ : la variable $u$ no está declarada en $\Gamma$ , así que simplemente no aporta nada.

Con el lenguaje ya fijado, queda lo esencial: las tres reglas que permiten derivar juicios $\Gamma \vdash M : \sigma$ , y el primer dividendo de esta contabilidad, el Lema 7.57 de variables libres, que conecta $FV(M)$ con $\operatorname{dom}(\Gamma)$ .