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 ).
Rasgos generales
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 , aunque es imposible probar esta propiedad dentro del CoC ya que implica consistencia, que por el teorema de incompletitud de Gödel es imposible de probar desde dentro del propio sistema.
Uso
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.
Las variantes del CoC se utilizan en otros asistentes de prueba, como Matita .
Los fundamentos del cálculo de construcciones.
El cálculo de construcciones puede considerarse una extensión del isomorfismo Curry-Howard . El isomorfismo de Curry-Howard asocia un término en el cálculo lambda simplemente tipado 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").
Condiciones
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);
- Variables () son términos;
- Si y son términos, entonces también lo es ;
- Si y son términos y es una variable, los siguientes también son términos:
- ,
- .
En otras palabras, el término sintaxis, en BNF , 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 tipo grande);
- sí mismo, que es el tipo de tipos grandes.
Juicios
El cálculo de construcciones permite probar juicios mecanográficos :
Que se puede leer como la implicación
- Si las variables tener tipos , luego termine tiene tipo .
Los juicios válidos para el cálculo de construcciones son derivables de un conjunto de reglas de inferencia. En lo siguiente, usamos para significar una secuencia de asignaciones de tipo ; significar términos; y para significar ya sea o . Vamos a escribir para significar el resultado de sustituir el término para la variable libre en el plazo .
Una regla de inferencia está escrita 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 booleanos y los naturales se definen de la misma manera que en la codificación de Church . Sin embargo, surgen problemas adicionales de la extensionalidad proposicional y la irrelevancia de la prueba. [2]
Ver también
Referencias
- ^ Cálculo de construcciones inductivas y bibliotecas estándar básicas:
Datatypes
yLogic
. - ^ "Biblioteca estándar | El asistente de prueba de Coq" . coq.inria.fr . Consultado el 8 de agosto de 2020 .
- Coquand, Thierry ; Huet, Gérard (1988). "El cálculo de las construcciones" (PDF) . Información y Computación . 76 (2-3): 95-120. doi : 10.1016 / 0890-5401 (88) 90005-3 .
- También disponible de forma gratuita accesible en línea: Coquand, Thierry; Huet, Gérard (1986). El cálculo de construcciones (Informe técnico). INRIA, Centre de Rocquencourt. 530.
Tenga en cuenta que la terminología es bastante diferente. Por ejemplo, () Se escribe [ x : A ] B .
- También disponible de forma gratuita accesible en línea: Coquand, Thierry; Huet, Gérard (1986). El cálculo de construcciones (Informe técnico). INRIA, Centre de Rocquencourt. 530.
- Bunder, MW; Seldin, Jonathan P. (2004). "Variantes del cálculo básico de construcciones". CiteSeerX 10.1.1.88.9497 . Cite journal requiere
|journal=
( ayuda ) - Frade, Maria João (2009). "Cálculo de construcciones inductivas" (PDF) . Archivado desde el original (charla) 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 Generación Futura . Holanda Septentrional. págs. 205–216. ISBN 0444704108. Archivado desde el original (PDF) el 1 de julio de 2015. - Una aplicación del CoC