Cálculo de la construcción

El cálculo de construcciones ( CoC ) es una teoría de tipos basada en un cálculo λ polimórfico de orden superior con tipos dependientes , desarrollado por Thierry Cocan y Gerard Huet en 1986. Está situado en el punto más alto del cubo lambda de Barendregt , siendo el más ancho de sus sistemas constituyentes- . Se puede utilizar como base para construir un lenguaje de programación tipado y como un sistema de fundamentos constructivos para las matemáticas . $\lambda p\omega$

Se utiliza como base para el sistema de prueba interactivo Coq y varias herramientas similares (incluida Matita ).

Entre las opciones de cálculo se encuentran el cálculo de construcciones inductivas [1] (utiliza tipos inductivos ), el cálculo de construcciones co-inductivas (utilizando coinducción ), el cálculo predicativo de construcciones inductivas (elimina parte de la no predicatividad ).

En términos de la correspondencia de Curry-Howard , el cálculo de construcción establece la relación entre los tipos dependientes y las pruebas en el cálculo de predicados intuicionista secuencial .

Estructura

Baños

Un término en el cálculo de la construcción se construye de acuerdo con las siguientes reglas:

T es un término (también conocido como Tipo );
P es un término (también conocido como Prop , este es el tipo al que se refieren todas las declaraciones);
Las variables ( x , y , …) son términos;
Si A y B son términos, entonces la expresión ( A B ) también es un término;
Si A y B son términos y x es una variable, entonces las siguientes expresiones también son términos:
- (λx : A . B ) ,
- (∀x : A . B).

En otras palabras, la sintaxis de un término, cuando se escribe usando BNF , es:

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 la construcción utiliza cinco tipos de objetos:

pruebas que tienen el tipo de ciertas afirmaciones ;
aserciones , también llamados tipos pequeños ;
predicados , que son funciones que devuelven afirmaciones ;
tipos grandes que son tipos para predicados ( P es un ejemplo de un tipo tan grande);
T como tal, que es el tipo al que pertenecen los tipos grandes.

Juicios

El cálculo de construcción permite probar juicios sobre tipos .

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

se puede leer como una implicación:

Si las variables son de tipo , entonces el término es de tipo .

x_{1},x_{2},\ldots

A_{1},A_{2},\ldots

t

B

Las proposiciones válidas para el cálculo de la construcción se pueden derivar de un conjunto de reglas de inferencia. En lo que sigue, usamos símbolo para denotar una secuencia de asignaciones de tipos y K para denotar P o T. La fórmula se utilizará para reemplazar el término de cada variable libre en el término . $\Gama$ $x_{1}:A_{1},x_{2}:A_{2},\ldots$ ${\ estilo de visualización B [x: = N]}$ $norte$ $X$ $B$

Las reglas de inferencia se escriben en el siguiente formato:

{\displaystyle {\Gamma \vdash A:B} \over {\Gamma '\vdash C:D))

significa:

Si es una proposición válida, entonces

{\ estilo de visualización \ Gamma \ vdash A: B}

\Gamma '\vdash C:D

Reglas de inferencia para el cálculo de la construcción

1 . ${\displaystyle {{} \over {}\Gamma \vdash P:T))$

2 . ${\Gamma \vdash A:K \over {\Gamma,x:A\vdash x:A))$

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

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

5 . ${\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 la construcción incluye un número muy pequeño de operadores básicos: el único operador lógico para la formación de declaraciones . Sin embargo, esta declaración por sí sola es suficiente para definir todos los demás operadores lógicos: $\para todos$

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

Definición de tipos de datos

El cálculo de construcción le permite definir los tipos de datos básicos utilizados en informática:

valores booleanos

\forall A:PA\Rightarrow A\Rightarrow A

enteros

\forall A:P.(A\Rightarrow A)\Rightarrow (A\Rightarrow A)

Trabajar

A\veces B

A \ cuña B

Unión exclusiva (notación variante)

A+B

A\vee B

Tenga en cuenta que los valores booleanos y numéricos se definen de manera similar a la codificación de la Iglesia . Sin embargo, surgen problemas adicionales de la extensionalidad de las declaraciones y la irrelevancia[ aclarar ] evidencia [2] .

Notas

↑ Cálculo de construcciones inductivas Archivado el 10 de junio de 2020 en Wayback Machine y en Coq Core Standard Libraries: Archivado el 10 de junio de 2020 en Wayback Machine y Archivado el 10 de junio de 2020 en Wayback Machine .Datatypes Logic
↑ Biblioteca estándar | El asistente de prueba de Coq . Consultado el 24 de junio de 2020. Archivado desde el original el 21 de julio de 2011. (indefinido)