Nivel 1 · El cálculo lambda

Hacia los tipos

El cálculo lambda no tipado, junto con el Teorema de Church-Rosser, ofrece un modelo robusto de computación. Sin embargo, no establece restricciones específicas sobre qué puede aplicarse a qué, lo que permite construir términos como el combinador $\Omega \equiv (\lambda x .\, x\, x)(\lambda x .\, x\, x)$ , que no se normaliza y produce bucles infinitos de cómputo (Ejemplo 7.36). Peor aún: si se intenta usar el sistema sin tipos como base para la lógica, admite paradojas, como la de Kleene-Rosser, que vuelve el sistema contradictorio; el fenómeno se discute en Sørensen y Urzyczyn (2006) . Debido a esto se introduce una restricción fundamental: los tipos.

El remedio: tipos simples

El cálculo lambda simplemente tipado $\lambda\rightarrow$ nace de esta necesidad. Al asignar un tipo a cada término se prohíben las construcciones mal formadas como $x\, x$ , y con ello se garantiza que todo término bien formado termina (la propiedad de normalización fuerte, Definición 7.35). Este es el primer paso para transformar el cálculo lambda de un modelo teórico de computabilidad en una base sólida para la lógica, siguiendo a Nederpelt y Geuvers (2014) .

Definición 7.45 (Conjunto 𝕋 de tipos simples)

Sea $\mathbb{V} = \{\alpha, \beta, \gamma, \ldots\}$ un conjunto infinito de variables de tipo. El conjunto $\mathbb{T}$ de tipos simples se define recursivamente:

(Variable de tipo) Si $\alpha \in \mathbb{V}$ , entonces $\alpha \in \mathbb{T}$ .
(Tipo flecha) Si $\sigma, \tau \in \mathbb{T}$ , entonces $(\sigma \rightarrow \tau) \in \mathbb{T}$ .

Nota 7.46 (Notación de tipos)

Las letras griegas $\alpha, \beta, \dots$ representan variables de tipo en $\mathbb{V}$ .
Los símbolos $\sigma, \tau, \ldots$ denotan tipos simples arbitrarios.
Los paréntesis externos pueden omitirse.
El conector de tipos flecha $\rightarrow$ se agrupa por la derecha: el tipo $\alpha \rightarrow \beta \rightarrow \gamma$ se interpreta como $\alpha \rightarrow (\beta \rightarrow \gamma)$ .

La interpretación es la esperada: las variables de tipo representan tipos básicos (como los números naturales), y un tipo flecha $\sigma \rightarrow \tau$ representa las funciones que reciben un argumento de tipo $\sigma$ y devuelven un resultado de tipo $\tau$ . El enunciado $M : \sigma$ se lee «el término $M$ tiene el tipo $\sigma$ », y para los términos compuestos rigen dos requisitos:

Aplicación: si $M : \sigma \rightarrow \tau$ y $N : \sigma$ , entonces $M N : \tau$ .
Abstracción: si $x : \sigma$ y $M : \tau$ , entonces $\lambda x .\, M : \sigma \rightarrow \tau$ .

Definición 7.48 (Término tipable)

Un término $M$ es tipable si existe un tipo $\sigma$ tal que $M : \sigma$ .

Ejemplo 7.49 (Tipables y no tipables)

$x : \sigma \implies \lambda x .\, x : \sigma \rightarrow \sigma$ . La función identidad devuelve un resultado del mismo tipo que su argumento.
$y : \sigma \rightarrow \tau,\ x : \sigma \implies y\, x : \tau$ . Aplicar una función de tipo $\sigma \rightarrow \tau$ a un término de tipo $\sigma$ produce un resultado de tipo $\tau$ .
$x\, x$ no es tipable: se exigiría que $x$ tuviera simultáneamente los tipos $\sigma \rightarrow \tau$ (como función) y $\sigma$ (como argumento), lo que implica la ecuación imposible $\sigma = \sigma \rightarrow \tau$ en el sistema de tipos simples.
La asociatividad derecha de los tipos flecha y la asociatividad izquierda de la aplicación permiten escribir: $f : \rho \rightarrow \sigma \rightarrow \tau,\quad x : \rho,\quad y : \sigma \implies f x : \sigma \rightarrow \tau,\quad (f x)\, y : \tau.$

El punto 3 es la moraleja de todo el módulo: la autoaplicación $x\, x$ , el ingrediente con el que se construyó $\Omega$ , queda prohibida por el sistema de tipos. En $\lambda\rightarrow$ el término $\Omega$ ni siquiera puede escribirse, y la amenaza de la no terminación desaparece por completo.

Anticipo: el juicio de tipado

¿Cómo se demuestra que un término tiene un tipo? La afirmación central de $\lambda\rightarrow$ es el juicio de tipado, cuya forma se define ya con precisión; las reglas para derivarlo se estudian en el nivel 2 del sitio (próximamente).

Definición 7.50 (λ-términos pre-tipados, Λ𝕋)

El conjunto de λ-términos pre-tipados se define por:

\Lambda_{\mathbb{T}} = V \ \mid\ (\Lambda_{\mathbb{T}}\, \Lambda_{\mathbb{T}}) \ \mid\ (\lambda V : \mathbb{T} .\, \Lambda_{\mathbb{T}}),

adaptando las condiciones de la Definición 7.1: ahora cada abstracción anota el tipo de su variable de enlace, como en $\lambda x : \sigma .\, x$ .

Definición 7.51 (Enunciado, declaración, contexto, juicio)

Considérense las siguientes definiciones:

Un enunciado tiene la forma $M : \sigma$ , donde $M \in \Lambda_{\mathbb{T}}$ y $\sigma \in \mathbb{T}$ . En este enunciado, $M$ se llama el sujeto y $\sigma$ el tipo.
Una declaración es un enunciado con una variable como sujeto.
Un contexto es una lista de declaraciones con sujetos distintos.
Un juicio tiene la forma $\Gamma \vdash M : \sigma$ , con $\Gamma$ un contexto y $M : \sigma$ un enunciado.

Un ejemplo concreto de juicio, tomado de la tesis:

x : \alpha \rightarrow \alpha,\ y : (\alpha \rightarrow \alpha) \rightarrow \beta \ \vdash\ (\lambda z : \beta .\, \lambda u : \gamma .\, z)(y\, x) : \gamma \rightarrow \beta.

Se lee así: «asumiendo que la variable $x$ tiene tipo $\alpha \rightarrow \alpha$ y la variable $y$ tiene tipo $(\alpha \rightarrow \alpha) \rightarrow \beta$ (el contexto), se demuestra que el término $(\lambda z : \beta .\, \lambda u : \gamma .\, z)(y\, x)$ resulta en una función de tipo $\gamma \rightarrow \beta$ ». El símbolo $\vdash$ separa las suposiciones de la afirmación demostrada. Las tres reglas de derivación que generan todos los juicios válidos (variable, aplicación y abstracción) son el corazón de la teoría de tipos y se presentan en el nivel 2.

Anticipo: proposiciones como tipos

Hay una segunda lectura del juicio $\Gamma \vdash M : \sigma$ , y es la razón de ser de esta tesis. Obsérvese el término constante del ejemplo anterior, sin anotaciones: $\lambda x .\, \lambda y .\, x$ , de tipo $\sigma \rightarrow (\tau \rightarrow \sigma)$ . Si se leen las variables de tipo como proposiciones y la flecha como implicación, ese tipo es el esquema $A \rightarrow (B \rightarrow A)$ , un conocido axioma de la lógica proposicional. La interpretación PAT (propositions as types, proofs as terms) establece que los tipos corresponden a proposiciones y que los términos que habitan un tipo corresponden a pruebas de la proposición; por ejemplo,

\lambda x : A .\, \lambda y : B .\, x \quad \text{prueba que} \quad A \rightarrow B \rightarrow A.

Esta es la correspondencia de Curry–Howard , sobre la que se construyen los asistentes de pruebas como Lean: demostrar un teorema es, literalmente, construir un término del tipo correspondiente. Dos panoramas excelentes son Sørensen y Urzyczyn (2006) y Wadler (2015) .

El otro lado del puente: la lógica

Para que la consigna «tipos = proposiciones, términos = pruebas» tenga contenido matemático hace falta el otro extremo del puente: una presentación rigurosa de la lógica que se pretende capturar. Por eso el sitio no salta todavía a la teoría de tipos completa: el nivel 3 desarrolla primero la lógica proposicional con sus dos nociones de consecuencia, la sintáctica $\vdash$ (deducibilidad mediante deducción natural ) y la semántica $\models$ (verdad en toda valuación ), junto con los dos teoremas que las conectan: solidez y completitud , siguiendo a Huth y Ryan (2004) . La demostración de completitud que la tesis formaliza en Lean pasa por el lema de Kalmár , debido a Kalmár (1935) . Solo con ambos lados en su lugar (el cálculo con tipos de este módulo y la lógica del nivel 3) puede apreciarse el puente que los identifica.