Cálculo de construcciones

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 ha desarrollado junto con el asistente de pruebas Coq . A medida que se añadieron características (o se eliminaron posibles inconvenientes) a la teoría, estas estuvieron 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:

• ${\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, entonces los siguientes también son términos: ${\displaystyle A}$ ${\displaystyle B}$ ${\displaystyle x}$
  • ${\displaystyle (\lambda x:A.B)}$,
  • ${\displaystyle (\forall x:A.B)}$.

En otras palabras, el término sintaxis, en la forma Backus-Naur , es entonces:

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

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} }$en sí, que es el tipo de tipos grandes.

Sentencias

El cálculo de construcciones permite demostrar juicios de tipificación :

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

lo cual puede leerse como la implicación

Si las variables tienen, respectivamente, tipos , entonces el término tiene 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 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 . ${\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 se escribe 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:A.B):L}}}$

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

5 . ${\displaystyle {\Gamma \vdash M:(\forall x:A.B)\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:A.B&(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)&\\\exists x:A.B&\equiv &\forall C:\mathbf {P} .(\forall x:A.(B\Rightarrow C))\Rightarrow C&\end{array}}}$

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

• Sistema de tipos puros
• Cubo lambda
• Sistema F
• Tipo dependiente
• Teoría de tipos intuicionista
• Teoría de tipos de homotopía

Referencias

1. Cálculo de construcciones inductivas y bibliotecas estándar básicas: tipos de datos y lógica.
2. "Biblioteca estándar | El asistente de pruebas Coq". coq.inria.fr . Consultado el 8 de agosto de 2020 .
3. 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 . ${\displaystyle \forall 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 del Norte. pp. 205–216. ISBN. 0444704108. Archivado desde el original (PDF) el 1 de julio de 2015.— Una aplicación del CoC