Cálculo de construcciones

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);
• Variables (${\displaystyle x,y,\ldots }$) son términos;
• Si${\displaystyle A}$y${\displaystyle B}$son términos, entonces también lo es${\displaystyle (AB)}$;
• Si${\displaystyle A}$y${\displaystyle B}$son términos y${\displaystyle x}$Si es una variable, entonces los siguientes también son términos:
  • ${\displaystyle (\lambda x:A.B)}$,
  • ${\displaystyle (\forall x:A.B)}$.

En otras palabras, el término sintaxis, en la forma de 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 (${\displaystyle \mathbf {P} }$es un ejemplo de un tipo grande);
5. ${\displaystyle \mathbf {T} }$sí mismo, que es el tipo de tipos grandes.

Al igual que el cálculo lambda sin tipos, el cálculo de construcciones utiliza una noción básica de equivalencia de términos, conocida como${\displaystyle \beta }$-equivalencia. Esto captura el significado de${\displaystyle \lambda }$-abstracción:

• ${\displaystyle (\lambda x:A.B)N=_{\beta }B(x:=N)}$

${\displaystyle \beta }$-equivalencia es una relación de congruencia para el cálculo de construcciones, en el sentido de que

• Si${\displaystyle A=_{\beta }B}$y${\displaystyle M=_{\beta }N}$, entonces${\displaystyle AM=_{\beta }BN}$.

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${\displaystyle x_{1},x_{2},\ldots }$tienen, respectivamente, tipos${\displaystyle A_{1},A_{2},\ldots }$, entonces término${\displaystyle t}$tiene tipo${\displaystyle B}$.

Los juicios válidos para el cálculo de construcciones se derivan de un conjunto de reglas de inferencia . A continuación, utilizamos${\displaystyle \Gamma }$significa una secuencia de asignaciones de tipo ${\displaystyle x_{1}:A_{1},x_{2}:A_{2},\ldots }$;${\displaystyle A,B,C,D}$para significar términos; y${\displaystyle K,L}$para significar cualquiera${\displaystyle \mathbf {P} }$o${\displaystyle \mathbf {T} }$Escribiremos.${\displaystyle B[x:=N]}$significar el resultado de sustituir el término${\displaystyle N}$para la variable libre${\displaystyle x}$en el término${\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${\displaystyle \Gamma \vdash A:B}$Si es un juicio válido, entonces también lo es.${\displaystyle \Gamma '\vdash C:D}$.

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

2 .${\displaystyle {{\Gamma \vdash A:K} \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}}}$

El cálculo de construcciones tiene muy pocos operadores básicos: el único operador lógico para formar proposiciones es${\displaystyle \forall }$Sin embargo, este único operador es suficiente para definir todos los demás operadores lógicos:

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

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

Los booleanos y los 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 ]}