En lógica matemática e informática , el cálculo de construcciones ( CoC ) es una teoría de tipos creada por Thierry Coquand . Puede servir como un lenguaje de programación mecanografiado y como base constructiva para las matemáticas . Por esta segunda razón, el CoC y sus variantes han sido la base para Coq y otros asistentes de prueba .
Algunas de sus variantes incluyen el cálculo de construcciones inductivas [1] (que agrega tipos inductivos ), el cálculo de construcciones (co) inductivas (que agrega coinducción ) y el cálculo predicativo de construcciones inductivas (que elimina algo de impredicatividad ).
El cálculo de construcciones, con un axioma adicional correspondiente al axioma de elección , se puede codificar en la teoría de conjuntos con elección de Zermelo-Fraenkel (ZFC), y viceversa. Por tanto, ambos son iguales . [2]
El CoC es un cálculo lambda tipificado de orden superior , inicialmente desarrollado por Thierry Coquand . Es bien conocido por ser en la parte superior de Barendregt 's cubo lambda . Es posible dentro de CoC definir funciones de términos a términos, así como términos a tipos, tipos a tipos y tipos a términos.
El CoC se está normalizando fuertemente y, por lo tanto, es consistente . [3] Según el teorema de incompletitud de Gödel , es imposible probar la coherencia desde el propio CoC. [ cita requerida ]
El CoC se ha desarrollado junto con el asistente de pruebas Coq . A medida que se agregaron características (o se eliminaron posibles responsabilidades) a la teoría, estuvieron disponibles en Coq.