Cálculo de construcciones

Teoría de tipos creada por Thierry Coquand

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 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 de 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 cierta impredicatividad ).

Rasgos generales

El CoC es un cálculo lambda tipificado de orden superior , desarrollado inicialmente por Thierry Coquand . Es bien conocido por estar en la cima del cubo lambda de Barendregt . Dentro de 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 tanto, coherente . ^[2]

Uso

El CoC se ha desarrollado junto con el asistente de prueba Coq . A medida que se agregaron características (o se eliminaron posibles responsabilidades) a la teoría, estuvieron disponibles en Coq.

En otros asistentes de prueba, como Matita y Lean , se utilizan variantes del CoC .

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 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").

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 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 clases 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 tipo grande); ${\displaystyle \mathbf {P} }$
5. ${\displaystyle \mathbf {T} }$en sí, que es el tipo de tipos grandes.

Juicios

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

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

que 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, nos referimos a una secuencia de asignaciones de tipos ; significar términos; y significar cualquiera o . Escribiremos en el sentido del 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 Church . Sin embargo, surgen problemas adicionales debido a la extensionalidad proposicional y la irrelevancia de la prueba. ^[3]

Ver también

• Sistema de tipo puro
• cubo lambda
• Sistema F
• tipo dependiente
• Teoría de tipos intuicionista
• Teoría del tipo de homotopía

Referencias

1. Cálculo de construcciones inductivas y bibliotecas estándar básicas: tipos de datos y lógica.
2. Coquand, Thierry; Gallier, Jean H. (julio de 1990). "Una prueba de una fuerte normalización de la teoría de las construcciones utilizando una interpretación similar a Kripke". Informes Técnicos (Cis) : 14.
3. "Biblioteca estándar | El asistente de prueba de Coq". coq.inria.fr . Consultado el 8 de agosto de 2020 .

Fuentes

• Coquand, Thierry ; Huet, Gerard (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 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.
    La terminología de las notas 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”. CiteSeerx : ^{10.1.1.88.9497} .
• Frade, María 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, Gerard (1988). «Principios de Inducción Formalizados en el Cálculo de Construcciones» (PDF) . En Fuchi, K.; Nivat, M. (eds.). Programación de Computadoras de Futura Generación . Holanda del Norte. págs. 205-216. ISBN 0444704108. Archivado desde el original (PDF) el 1 de julio de 2015.— Una aplicación del CoC