Cálculo de construcciones - Calculus of constructions

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 (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 .

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:

• ${\ Displaystyle \ mathbf {T}}$es un término (también llamado tipo );
• ${\ Displaystyle \ mathbf {P}}$es un término (también llamado prop , el tipo de todas las proposiciones);
• Las variables ( ) son términos;${\ Displaystyle x, y, \ ldots}$
• Si y son términos, entonces también lo es ;${\ Displaystyle A}$${\ Displaystyle B}$${\ Displaystyle (AB)}$
• Si y son términos y es una variable, los siguientes también son términos: ${\ Displaystyle A}$${\ Displaystyle B}$${\ Displaystyle x}$
  • ${\ Displaystyle (\ lambda x: AB)}$,
  • ${\ Displaystyle (\ forall x: AB)}$.

En otras palabras, el término sintaxis, en BNF , es entonces:

${\ Displaystyle e :: = \ mathbf {T} \ mid \ mathbf {P} \ mid x \ mid e \, e \ mid \ lambda x {\ mathbin {:}} ee \ mid \ forall x {\ mathbin { :}} ee}$

El cálculo de construcciones tiene cinco tipos de objetos:

1. pruebas , que son términos cuyos tipos son proposiciones ;
2. proposiciones , que también se conocen como tipos pequeños ;
3. predicados , que son funciones que devuelven proposiciones;
4. tipos grandes , que son los tipos de predicados ( es un ejemplo de un tipo grande);${\ Displaystyle \ mathbf {P}}$
5. ${\ Displaystyle \ mathbf {T}}$ sí mismo, que es el tipo de tipos grandes.

Juicios

El cálculo de construcciones permite probar juicios mecanográficos :

${\ Displaystyle x_ {1}: A_ {1}, x_ {2}: A_ {2}, \ ldots \ vdash t: B}$

Que se puede leer como la implicación

Si las variables tienen tipos , el término tiene un tipo .${\ Displaystyle x_ {1}, x_ {2}, \ ldots}$${\ Displaystyle A_ {1}, A_ {2}, \ ldots}$${\ Displaystyle t}$${\ Displaystyle B}$

Los juicios válidos para el cálculo de construcciones son derivables de un conjunto de reglas de inferencia. A continuación, usamos para referirnos a una secuencia de asignaciones de tipos ; significar términos; y significar o bien . Escribiremos para significar el resultado de sustituir el término por la variable libre en el término . ${\ Displaystyle \ Gamma}$${\ Displaystyle x_ {1}: A_ {1}, x_ {2}: A_ {2}, \ ldots}$${\ Displaystyle A, B, C, D}$${\ Displaystyle K, L}$${\ Displaystyle \ mathbf {P}}$${\ Displaystyle \ mathbf {T}}$${\ Displaystyle B [x: = N]}$${\ Displaystyle N}$${\ Displaystyle x}$${\ Displaystyle B}$

Una regla de inferencia está escrita en la forma

${\ Displaystyle {\ frac {\ Gamma \ vdash A: B} {\ Gamma '\ vdash C: D}}}$

lo que significa

Si es un juicio válido, entonces también lo es${\ Displaystyle \ Gamma \ vdash A: B}$${\ Displaystyle \ Gamma '\ vdash C: D}$

Reglas de inferencia para el cálculo de construcciones

1 .${\ Displaystyle {{} \ over \ Gamma \ vdash \ mathbf {P}: \ mathbf {T}}}$

2 .${\ Displaystyle {{} \ over {\ Gamma, x: A, \ Gamma '\ vdash x: A}}}$

3 .${\ Displaystyle {\ Gamma \ vdash A: K \ qquad \ qquad \ Gamma, x: A \ vdash B: L \ over {\ Gamma \ vdash (\ forall x: AB): L}}}$

4 .${\ Displaystyle {\ Gamma \ vdash A: K \ qquad \ qquad \ Gamma, x: A \ vdash N: B \ over {\ Gamma \ vdash (\ lambda x: AN): (\ forall x: AB)}} }$

5 .${\ Displaystyle {\ Gamma \ vdash M: (\ forall x: AB) \ qquad \ qquad \ Gamma \ vdash N: A \ over {\ Gamma \ vdash MN: B [x: = N]}}}$

6 . ${\ Displaystyle {\ Gamma \ vdash M: A \ qquad \ qquad A = _ {\ beta} B \ qquad \ qquad \ Gamma \ vdash B: K \ over {\ Gamma \ vdash M: B}}}$

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: ${\ Displaystyle \ forall}$

${\ Displaystyle {\ begin {array} {ccll} A \ Rightarrow B & \ equiv & \ forall x: AB & (x \ notin B) \\ A \ wedge B & \ equiv & \ forall C: \ mathbf {P}. ( A \ Rightarrow B \ Rightarrow C) \ Rightarrow C & \\ A \ vee B & \ equiv & \ forall C: \ mathbf {P}. (A \ Rightarrow C) \ Rightarrow (B \ Rightarrow C) \ Rightarrow C & \\\ neg A & \ equiv & \ forall C: \ mathbf {P}. (A \ Rightarrow C) & \\\ existe x: AB & \ equiv & \ forall C: \ mathbf {P}. (\ forall x: A. ( B \ Rightarrow C)) \ Rightarrow C & \ end {matriz}}}$

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

${\ Displaystyle \ forall A: \ mathbf {P} .A \ Rightarrow A \ Rightarrow A}$

Naturales

${\ Displaystyle \ forall A: \ mathbf {P}. (A \ Rightarrow A) \ Rightarrow (A \ Rightarrow A)}$

Producto ${\ Displaystyle A \ times B}$

${\ Displaystyle A \ wedge B}$

Unión disjunta ${\ Displaystyle A + B}$

${\ Displaystyle A \ vee B}$

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.

Ver también

• Sistema de tipo puro
• Cubo lambda
• Sistema F
• Tipo dependiente
• Teoría de tipos intuicionistas
• Teoría del tipo de homotopía

Referencias