El cálculo de construcciones inductivas

Conversación: Calculus of inductive constructions (resumen). Índice: documentos.

El CIC es la teoría de tipos sobre la que están construidos Coq/Rocq y, con variantes, Lean. Interesa al libro por una razón precisa: es el sistema donde lógica y computación son literalmente lo mismo, y donde los «axiomas» dejan de ser verdades para convertirse en reglas de construcción.

Propiedades

Metateóricas

Propiedad	Qué dice	Para qué sirve
Normalización fuerte	Todo término bien tipado reduce a forma normal en un número finito de pasos, por cualquier camino	Todas las funciones definibles terminan; de ahí la exigencia de recursión estructural o bien fundada
Confluencia (Church-Rosser)	El resultado no depende del orden de reducción	La forma normal es única
Preservación de tipos	Si un término tiene tipo T, lo conserva al reducirse	El tipado es estable bajo cómputo
Consistencia	No hay término cerrado de tipo `False`	No se puede demostrar una contradicción
Decidibilidad del chequeo de tipos	Verificar si un término tiene un tipo dado es decidible	El ordenador puede comprobar demostraciones mecánicamente

Estructurales

Tipos dependientes: un tipo puede depender de un valor («vector de longitud n»).
Curry-Howard: las proposiciones son tipos y las demostraciones, programas.
Tipos inductivos: naturales, listas, árboles y predicados, con sus principios de eliminación e inducción.
Jerarquía de universos: Prop impredicativo, Type₀ : Type₁ : … predicativo y estratificado.
Positividad estricta: los constructores no pueden mencionar el tipo que se define a la izquierda de una flecha. Sin esta condición se pierde la consistencia.
Lógica constructiva: el tercio excluso no es demostrable, aunque añadirlo como axioma no vuelve el sistema inconsistente.
Extracción de programas: de una demostración se obtiene código ejecutable borrando las partes de Prop.

Lo que no trae de serie: extensionalidad de funciones, irrelevancia de pruebas obligatoria y univalencia.

Con qué lógica se corresponde

Con la lógica intuicionista de orden superior enriquecida con definiciones inductivas.

Rasgo del sistema	Lectura lógica
Constructivo	Demostrar «existe x» exige construir x; sin tercio excluso ni doble negación
Tipos dependientes `Π x:A. P x`	Cuantificador universal; los tipos Σ dan el existencial
Universo impredicativo `Prop`	Cuantificación sobre proposiciones: más que primer orden
Tipos inductivos	Inducción, aritmética de Heyting, conectivos definidos

En el cubo lambda de Barendregt, el Cálculo de Construcciones sin inductivos ocupa el vértice λC. La escala completa es instructiva: lógica proposicional ↔︎ λ-cálculo simplemente tipado; segundo orden ↔︎ Sistema F; orden superior ↔︎ Fω; al añadir tipos dependientes se obtiene la lógica de predicados correspondiente.

Impredicatividad

Una definición es impredicativa cuando cuantifica sobre una totalidad a la que ella misma pertenece. En Prop:

∀ P : Prop, P → P

Esa expresión es a su vez una Prop, de modo que al definirla se cuantifica sobre todas las proposiciones, ella incluida. Lo contrario, lo predicativo, sube de nivel:

∀ A : Type₀, A → A   :   Type₁

	Ventaja	Riesgo	Precio
Impredicatividad en `Prop`	Permite codificar conectivos y definiciones dentro de `Prop`	Sin control produce paradojas: Russell, y la de Girard, que muestra que `Type : Type` es inconsistente	Restricción de eliminación: de una prueba en `Prop` no se puede extraer información para construir datos en `Type`

El antecedente histórico es la crítica de Poincaré y Russell a las definiciones de «círculo vicioso» y la teoría ramificada de tipos. CIC llega a un compromiso: tolera la impredicatividad, pero solo en el mundo de las proposiciones.

Para el libro esto es más que un detalle técnico. La impredicatividad es la misma figura que está detrás de las aporías reflexivas: una totalidad que se incluye a sí misma. La diferencia es que aquí no se la prohíbe ni se la padece, sino que se la confina: se permite donde no hace daño y se estratifica donde lo haría. Es una tercera salida, junto a los tipos de Russell y al silencio del Tractatus, al problema que recoge Copiar y nombrar: la diagonal que une a Cantor y Gödel.

Qué son los «axiomas» aquí

No hay un único conjunto de axiomas de «la lógica»; depende del sistema y de la presentación.

Presentación de Hilbert (proposicional clásica): tres esquemas y una regla.

A → (B → A)
(A → (B → C)) → ((A → B) → (A → C))
(¬B → ¬A) → (A → B)
Regla: modus ponens.

La versión intuicionista sustituye el tercero por uno más débil, por ejemplo A → (¬A → B); lo que se pierde es exactamente ¬¬A → A y A ∨ ¬A. En primer orden se añaden los esquemas de cuantificación y la regla de generalización.

Deducción natural, en cambio, prescinde casi de axiomas y usa reglas de introducción y eliminación por conectiva. Y ahí está el punto: esas reglas son los constructores y eliminadores de los tipos de CIC. El sistema no necesita axiomas lógicos porque las reglas de tipado ya hacen ese trabajo. Los axiomas pasan a ser extras opcionales:

Axioma opcional	Qué añade
Tercio excluso / doble negación	Lógica clásica
Extensionalidad de funciones	Igualdad de funciones punto a punto
Irrelevancia de pruebas	Todas las pruebas de una `Prop` se identifican
Univalencia	Igualdad como equivalencia (HoTT)
Elección	El axioma de elección

Los axiomas, vistos así, fijan reglas de inferencia, no verdades sobre el mundo.

Después del CoC

La línea de evolución va del Cálculo de Construcciones de Coquand y Huet (años ochenta, sin inductivos nativos) al CIC con tipos inductivos, luego a los coinductivos y a las variantes predicativas de Lean, y de ahí a la teoría de tipos homotópica y a la cúbica, donde la univalencia deja de ser un axioma y pasa a tener contenido computacional.

Fuentes

Ninguna se citó en la conversación.

T. Coquand y G. Huet, «The Calculus of Constructions», Information and Computation 76 (1988).
H. Barendregt, «Lambda Calculi with Types» (1992), para el cubo.
J.-Y. Girard, su paradoja y la inconsistencia de Type : Type (tesis, 1972).
The Coq Development Team, manual de referencia, capítulo sobre CIC.
The Univalent Foundations Program, Homotopy Type Theory, IAS, 2013.
En el repo: la ficha claude/logicas/123_calculo-de-construcciones.md, Aprender Lean 4 y las transcripciones de transcripciones/lean/.

Correcciones y puntos pendientes

Corregido: False := ∀ P, P y la igualdad de Leibniz impredicativa son codificaciones del CoC puro. En CIC, False, la igualdad y los conectivos son tipos inductivos. La conversación mezclaba los dos sistemas.
Matizado: «la consistencia se sigue de la normalización» vale como esquema, pero la consistencia de CIC con universos no se demuestra dentro del propio sistema — es el segundo teorema de Gödel otra vez.
Matizado: la equiparación de fuerza con «ZF intuicionista con universos inaccesibles» es aproximada y depende de la variante.
Matizado: decir que «sin axiomas el sistema ya es una lógica completa y consistente» es impreciso: la completitud en sentido de Gödel no se aplica aquí.
Pendiente: Lean ofrece tercio excluso y elección como axiomas disponibles en su biblioteca; «de serie» o «no de serie» depende de si se cuenta el núcleo o Mathlib.
Fuera de alcance: el tramo final de la conversación (ThrottleStop, temperaturas de un portátil HP) no tiene relación con el libro.