Teoría de tipos creada por Thierry Coquand
En lógica matemática y ciencias de la computación , el cálculo de construcciones ( CoC ) es una teoría de tipos creada por Thierry Coquand . Puede servir tanto como lenguaje de programación tipado como como fundamento constructivo para las matemáticas . Por esta segunda razón, el CoC y sus variantes han sido la base de Coq y otros asistentes de demostración .
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 cierta impredicatividad ). [2]
Rasgos generales
El CoC es un cálculo lambda tipificado de orden superior , desarrollado inicialmente por Thierry Coquand . Es conocido por estar en la cima del cubo lambda de Barendregt . En el CoC es posible definir funciones de términos a términos, así como de términos a tipos, de tipos a tipos y de tipos a términos.
El CoC es fuertemente normalizador y, por lo tanto, consistente . [3]
Uso
El CoC se desarrolló junto con el asistente de pruebas Coq . A medida que se agregaron características (o se eliminaron posibles inconvenientes) a la teoría, se hicieron disponibles en Coq.
Se utilizan variantes del CoC en otros asistentes de prueba, como Matita y Lean .
Los fundamentos del cálculo de construcciones
El cálculo de construcciones puede considerarse una extensión del isomorfismo de Curry-Howard . El isomorfismo de Curry-Howard asocia un término del cálculo lambda de tipos simples con cada prueba de deducción natural en la lógica proposicional intuicionista . El cálculo de construcciones extiende este isomorfismo a las pruebas en el cálculo de predicados intuicionista completo , que incluye pruebas de enunciados cuantificados (que también llamaremos "proposiciones").
Términos
Un término en el cálculo de construcciones se construye utilizando las siguientes reglas:
- es un término (también llamado tipo );
- es un término (también llamado prop , el tipo de todas las proposiciones);
- Las variables ( ) son términos;
- Si y son términos, entonces también lo es ;
- Si y son términos y es una variable, entonces los siguientes también son términos:
- ,
- .
En otras palabras, el término sintaxis, en la forma Backus-Naur , es entonces:
El cálculo de construcciones tiene cinco tipos de objetos:
- pruebas , que son términos cuyos tipos son proposiciones ;
- proposiciones , que también se conocen como tipos pequeños ;
- predicados , que son funciones que devuelven proposiciones;
- tipos grandes , que son los tipos de predicados ( es un ejemplo de un tipo grande);
- en sí, que es el tipo de tipos grandes.
Sentencias
El cálculo de construcciones permite demostrar juicios de tipificación :
- ,
lo cual puede leerse como la implicación
- Si las variables tienen, respectivamente, tipos , entonces el término tiene tipo .
Los juicios válidos para el cálculo de construcciones se derivan de un conjunto de reglas de inferencia. En lo sucesivo, usamos para significar una secuencia de asignaciones de tipo ; para significar términos; y para significar o bien o bien . Escribiremos para significar el resultado de sustituir el término por la variable libre en el término .
Una regla de inferencia se escribe en la forma
- ,
lo que significa
- Si es un juicio válido, entonces también lo es .
Reglas de inferencia para el cálculo de construcciones
1 .
2 .
3 .
4 .
5 .
6 .
Definición de operadores lógicos
El cálculo de construcciones tiene muy pocos operadores básicos: el único operador lógico para formar proposiciones es . Sin embargo, este operador es suficiente para definir todos los demás operadores lógicos:
Definición de tipos de datos
Los tipos de datos básicos utilizados en informática se pueden definir dentro del cálculo de construcciones:
- Booleanos
- Naturales
- Producto
- Unión disjunta
Tenga en cuenta que los valores booleanos y naturales se definen de la misma manera que en la codificación de Church . Sin embargo, surgen problemas adicionales debido a la extensionalidad proposicional y la irrelevancia de la prueba. [2]
Véase también
Referencias
- ^ Cálculo de construcciones inductivas y bibliotecas estándar básicas: tipos de datos y lógica.
- ^ ab "Biblioteca estándar | El asistente de pruebas Coq". coq.inria.fr . Consultado el 8 de agosto de 2020 .
- ^ Coquand, Thierry; Gallier, Jean H. (julio de 1990). "Una prueba de normalización fuerte para la teoría de construcciones utilizando una interpretación similar a la de Kripke". Technical Reports (Cis) : 14.
Fuentes
- Coquand, Thierry ; Huet, Gérard (1988). "El cálculo de construcciones" (PDF) . Información y computación . 76 (2–3): 95–120. doi : 10.1016/0890-5401(88)90005-3 .
- También disponible en libre acceso en línea: Coquand, Thierry; Huet, Gerard (1986). El cálculo de las construcciones (Informe técnico). INRIA , Centro de Rocquencourt. 530.
Tenga en cuenta que la terminología es bastante diferente. Por ejemplo, ( ) se escribe [ x : A ] B .
- Bunder, MW; Seldin, Jonathan P. (2004). "Variantes del cálculo básico de construcciones". CiteSeer x : 10.1.1.88.9497.
- Frade, Maria João (2009). "Cálculo de construcciones inductivas" (PDF) . Archivado desde el original (discusión) el 29 de mayo de 2014 . Consultado el 3 de marzo de 2013 .
- Huet, Gérard (1988). "Principios de inducción formalizados en el cálculo de construcciones" (PDF) . En Fuchi, K.; Nivat, M. (eds.). Programación de computadoras de la futura generación . Holanda Septentrional. págs. 205–216. ISBN . 0444704108. Archivado desde el original (PDF) el 1 de julio de 2015.— Una aplicación del CoC