123. Cálculo de construcciones y asistentes de prueba

Idea central

El cálculo de construcciones es un único lenguaje en el que se escriben a la vez programas, especificaciones, proposiciones y pruebas. Lleva al extremo la lectura de las proposiciones como tipos: una prueba de \(A\) es un término de tipo \(A\), y comprobar una prueba es comprobar un tipo, tarea mecánica y decidible. Coquand y Huet combinaron en un solo sistema dos ingredientes que hasta entonces iban separados: los tipos dependientes, que permiten que un tipo dependa de un término (como en Automath y en la teoría de Martin-Löf), y el polimorfismo impredicativo del Sistema F, que permite cuantificar sobre todas las proposiciones. El gesto distintivo es práctico además de teórico: un núcleo pequeño y fiable que verifica pruebas, sobre el que se construyen asistentes que permiten formalizar matemática real.

Principios, axiomas y reglas de inferencia

Sintaxis (Coquand y Huet, «The calculus of constructions», Information and Computation, 1988). Dos «géneros» o sorts: \(*\) (las proposiciones, luego Prop) y \(\square\) (el tipo de \(*\)). Los términos son variables, géneros, productos dependientes \(\Pi x{:}A.\,B\), abstracciones \(\lambda x{:}A.\,t\) y aplicaciones \(t\,u\).

Reglas de tipado (juicios \(\Gamma \vdash t : A\)):

• Axioma: \(\vdash * : \square\).
• Variable: si \(\Gamma \vdash A : s\), entonces \(\Gamma, x{:}A \vdash x : A\). Debilitamiento análogo.
• Producto: si \(\Gamma \vdash A : s_1\) y \(\Gamma, x{:}A \vdash B : s_2\), entonces \(\Gamma \vdash \Pi x{:}A.\,B : s_2\), para todo par \((s_1, s_2)\) de géneros. Admitir los cuatro pares sitúa el sistema en el vértice superior del cubo lambda de Barendregt: el par \((*, *)\) da el cálculo simplemente tipado, y cada uno de los otros tres añade una de las tres dimensiones del cubo.
• Abstracción: si \(\Gamma, x{:}A \vdash t : B\) y \(\Gamma \vdash \Pi x{:}A.\,B : s\), entonces \(\Gamma \vdash \lambda x{:}A.\,t : \Pi x{:}A.\,B\).
• Aplicación: si \(\Gamma \vdash f : \Pi x{:}A.\,B\) y \(\Gamma \vdash a : A\), entonces \(\Gamma \vdash f\,a : B[a/x]\).
• Conversión: si \(\Gamma \vdash t : A\), \(A =_\beta B\) y \(\Gamma \vdash B : s\), entonces \(\Gamma \vdash t : B\).

Codificación de la lógica. La implicación es el producto no dependiente, \(A \to B = \Pi x{:}A.\,B\); el cuantificador universal es \(\Pi\). Las demás conectivas se definen impredicativamente:

• \(\bot := \Pi P{:}*.\,P\); \(\neg A := A \to \bot\).
• \(A \land B := \Pi C{:}*.\,(A \to B \to C) \to C\).
• \(A \lor B := \Pi C{:}*.\,(A \to C) \to (B \to C) \to C\).
• \(\exists x{:}A.\,P(x) := \Pi C{:}*.\,(\Pi x{:}A.\,P(x) \to C) \to C\).
• Igualdad de Leibniz: \(x =_A y := \Pi P{:}A \to *.\,P\,x \to P\,y\).

La lógica resultante es la intuicionista de orden superior. El tercio excluso y la eliminación de la doble negación no son derivables, pero pueden postularse como axiomas.

Metateoría. Normalización fuerte (Coquand), de la que se siguen la consistencia (ningún término cerrado habita \(\bot\)) y la decidibilidad de la comprobación de tipos. La impredicatividad (\(\Pi P{:}*.\,P\) es a su vez de tipo \(*\)) da mucha potencia, pero impide derivar los principios de inducción para los tipos de datos codificados.

Cálculo de construcciones inductivas (CIC; Coquand y Paulin-Mohring, «Inductively defined types», COLOG-88, publicado en 1990). Añade:

• definiciones inductivas primitivas con condición de positividad estricta, que generan constructores y principios de eliminación (recursión e inducción);
• una jerarquía predicativa de universos \(\mathrm{Type}_0 : \mathrm{Type}_1 : \dots\) junto a Prop impredicativo y, en Coq, Set;
• definiciones por punto fijo con condición de guarda para asegurar la terminación.

Ejemplo. Los naturales se definen con dos constructores, \(0 : \mathbb{N}\) y \(S : \mathbb{N} \to \mathbb{N}\). El sistema genera \(\mathrm{nat\_ind} : \Pi P{:}\mathbb{N} \to \mathrm{Prop}.\,P\,0 \to (\Pi n{:}\mathbb{N}.\,P\,n \to P\,(S\,n)) \to \Pi n{:}\mathbb{N}.\,P\,n\). Una prueba por inducción es literalmente la aplicación de este término.

Asistentes. Coq (hoy Rocq) implementa CIC desde finales de los años ochenta, con extracción de programas certificados (Paulin-Mohring). Lean (de Moura, desde 2013) usa una variante de CIC con irrelevancia de pruebas y cocientes. El «criterio de de Bruijn» exige que la fiabilidad dependa solo de un núcleo pequeño que cualquiera pueda revisar.

Genealogía

Procede del cálculo lambda tipado: el cálculo de construcciones es el vértice superior del cubo de Barendregt (1991), que clasifica los sistemas tipados según qué dependencias admiten entre términos y tipos; en sus otros vértices están el lambda simplemente tipado, el Sistema F, el \(\lambda\)P de los tipos dependientes y el F\(\omega\). De la teoría de tipos de Martin-Löf y de la correspondencia de Curry y Howard toma los tipos dependientes y la identificación entre proposiciones y tipos, así como, en CIC, la idea de tipos inductivos con reglas de introducción y eliminación; se aparta de Martin-Löf al admitir un universo impredicativo. De su línea procede a su vez la teoría homotópica de tipos: Voevodsky escribió su biblioteca univalente, Foundations, en Coq antes de que existieran asistentes pensados para HoTT.

La otra línea de antecedentes es la de los verificadores de pruebas: Automath de N. G. de Bruijn (desde 1967), que ya usaba tipos dependientes y la lectura de proposiciones como tipos, y la tradición LCF de Milner, de la que viene el uso de tácticas.

Contexto y relevancia

Coq se desarrolló en el INRIA en el proyecto Formel de Huet. Con él Georges Gonthier y Benjamin Werner formalizaron el teorema de los cuatro colores (2005) y un equipo dirigido por Gonthier el teorema de Feit–Thompson (2012); con Coq se verificó también el compilador CompCert. La comunidad de Lean, con la biblioteca Mathlib, ha extendido la formalización a buena parte de la matemática de grado y a resultados recientes. Para la pregunta «¿una lógica o muchas?» el caso es notable: el núcleo es intuicionista, pero el usuario puede añadir el tercio excluso, el axioma de elección o la extensionalidad según lo que quiera probar. La lógica deja de ser un fondo fijo y se convierte en un parámetro declarado del sistema, verificado por máquina.

Fuentes

• Thierry Coquand y Gérard Huet, «The calculus of constructions», Information and Computation 76 (1988), 95–120.
• Thierry Coquand y Christine Paulin-Mohring, «Inductively defined types», en COLOG-88, Lecture Notes in Computer Science 417, Springer, 1990, 50–66.
• Henk Barendregt, «Lambda calculi with types», en Handbook of Logic in Computer Science, vol. 2, Oxford University Press, 1992.
• Yves Bertot y Pierre Castéran, Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions, Springer, 2004.

← Índice de lógicas