Álgebra combinatoria parcial

En informática teórica y lógica matemática , específicamente en realizabilidad , un álgebra combinatoria parcial (ACP) es una estructura algebraica que abstrae un modelo de computación . La definición de ACP utiliza una idea de la lógica combinatoria . El topos de realizabilidad sobre un ACP es un modelo de lógica intuicionista de orden superior donde, informalmente, toda función es computable en el modelo de computación especificado por el ACP.

Una estructura aplicativa parcial es simplemente un conjunto${\displaystyle A}$equipado con una operación binaria parcial${\displaystyle A\times A\rightharpoonup A}$llamada aplicación . En el contexto de realizabilidad, esta operación se suele denotar mediante una simple yuxtaposición, es decir,${\displaystyle (a,b)\mapsto ab}$. Por lo general no es asociativo; por convención, la notación${\displaystyle abc}$asociados a la izquierda como${\displaystyle (ab)c}$, que coincide con la convención estándar en el cálculo λ . ^{[ 1 ] : 1}

Los términos (o expresiones ) sobre una estructura aplicativa parcial${\displaystyle A}$se definen inductivamente: ^{[ 1 ] : 2 [ 2 ] : 27}

• Una constante${\displaystyle a\in A}$es una expresión,
• Una variable, de algún conjunto fijo e infinito numerable de variables, es una expresión,
• Si${\displaystyle e_{1}}$y${\displaystyle e_{2}}$son expresiones, entonces${\displaystyle e_{1}e_{2}}$es una expresión.

(En otras palabras, forman el magma libre sobre la unión disjunta)${\displaystyle A+V}$dónde${\displaystyle V}$es el conjunto de variables.)

Un término es cerrado cuando no contiene variables. Un término cerrado puede evaluarse de la forma natural: una constante.${\displaystyle a\in A}$se evalúa a sí mismo, y si los términos${\displaystyle e_{1}}$y${\displaystyle e_{2}}$respectivamente evaluar a${\displaystyle a_{1}}$y${\displaystyle a_{2}}$, entonces${\displaystyle e_{1}e_{2}}$evalúa a${\displaystyle a_{1}a_{2}}$, si esto está definido. Tenga en cuenta que la evaluación es una operación parcial, ya que no todas las aplicaciones están definidas. Escribimos${\displaystyle t\downarrow }$expresar simultáneamente que el término${\displaystyle t}$se evalúa a un valor definido y denotamos este valor (esto coincide con la notación estándar para valores de funciones parciales ). También escribimos${\displaystyle t\simeq u}$cuando ambos términos cerrados${\displaystyle t}$y${\displaystyle u}$o bien no se evalúan a un valor definido, o bien se evalúan al mismo valor.

Una operación de sustitución también se define de forma natural: si${\displaystyle t}$es un término,${\displaystyle x}$es una variable y${\displaystyle u}$es otro término,${\displaystyle t[u/x]}$denota el término${\displaystyle t}$con todas las ocurrencias de${\displaystyle x}$reemplazado por${\displaystyle u}$.

Se dice que la estructura aplicativa parcial A es combinatoriamente completa o funcionalmente completa si, para cada término${\displaystyle t(x_{0},\dots ,x_{n})}$(es decir, un término${\displaystyle t}$cuyas variables se encuentran entre${\displaystyle x_{0},\dots ,x_{n}}$), existe un elemento${\displaystyle a\in A}$de tal manera que: ^{[ 2 ] : 27 [ 1 ] : 3}

• ${\displaystyle aa_{0}\dots a_{n-1}\downarrow }$a pesar de${\displaystyle a_{0},\dots ,a_{n-1}\in A}$,
• ${\displaystyle aa_{0}\dots a_{n}\simeq t[a_{0}/x_{0},\dots ,a_{n}/x_{n}]}$a pesar de${\displaystyle a_{0},\dots ,a_{n}\in A}$.

Un álgebra combinatoria parcial (pca) es una estructura aplicativa parcial combinatoria completa. Un álgebra combinatoria total (tca) es un pca cuya operación de aplicación es total.

De manera informal, la condición de completitud combinatoria requiere que exista dentro del PCA un análogo de la operación de abstracción del cálculo lambda.

De la misma manera que existe una traducción de términos λ a términos del cálculo combinatorio SKI mediante la eliminación de abstracciones λ utilizando combinadores, los pca pueden caracterizarse por la existencia de elementos que satisfacen ecuaciones análogas a las de los combinadores S y K. Sin embargo, cabe señalar que se debe tener cuidado en el enunciado y la demostración, ya que la aplicación no siempre está definida en un pca.

Teorema: ^{[ 2 ] : 28 [ 1 ] : 3} Una estructura aplicativa parcial${\displaystyle A}$es combinatoriamente completa si y solo si existen dos elementos${\displaystyle k,s\in A}$de tal manera que:

• ${\displaystyle Kxy\downarrow =x}$a pesar de${\displaystyle x,y\in A}$,
• ${\displaystyle Sxy\downarrow }$a pesar de${\displaystyle x,y\in A}$,
• ${\displaystyle Sxyz\simeq (xz)(yz)}$a pesar de${\displaystyle x,y,z\in A}$.

Para la demostración, en la dirección hacia adelante, si${\displaystyle A}$es combinatoriamente completo, basta con aplicar la definición de completitud combinatoria a los términos${\displaystyle t_{K}(x,y):=x}$y${\displaystyle t_{S}(x,y,z):=(xz)(yz)}$para obtener${\displaystyle K}$y${\displaystyle S}$con las propiedades requeridas.

Es lo contrario lo que implica la eliminación de la abstracción. Supongamos que tenemos${\displaystyle K}$y${\displaystyle S}$como se indicó. Dada una variable${\displaystyle x}$y un término${\displaystyle t}$, definimos un término${\displaystyle \langle x\rangle t}$cuyas variables son las de${\displaystyle t}$menos${\displaystyle x}$, que desempeña un papel similar a${\displaystyle \lambda x\cdot t}$en el cálculo λ. La definición es por inducción sobre${\displaystyle t}$de la siguiente manera: ^{[ 1 ] : 3 [ 2 ] : 28}

• ${\displaystyle \langle x\rangle a=Ka}$por una constante${\displaystyle a\in A}$,
• ${\displaystyle \langle x\rangle x=I}$dónde${\displaystyle I:=SKK}$,
• ${\displaystyle \langle x\rangle y=Ky}$si${\displaystyle y}$es una variable diferente de${\displaystyle x}$,
• ${\displaystyle \langle x\rangle (uv)=S(\langle x\rangle u)(\langle x\rangle v)}$.

Tenga cuidado con la analogía entre${\displaystyle \langle x\rangle t}$y${\displaystyle \lambda x\cdot t}$no es perfecto. Por ejemplo, los términos${\displaystyle (\langle x\rangle t)t'}$y${\displaystyle t[t'/x]}$No son generalmente equivalentes en un sentido razonable, por ejemplo, tomando una variable.${\displaystyle y}$diferente de${\displaystyle x}$y${\displaystyle a,b\in A}$constantes, tenemos${\displaystyle (\langle x\rangle y)(ab)=Ky(ab)}$, que no puede considerarse equivalente a${\displaystyle y}$porque este último siempre se evalúa a${\displaystyle c}$si${\displaystyle y}$es reemplazado por una constante${\displaystyle c\in A}$, mientras que el primero puede no serlo${\displaystyle ab}$puede no estar definido. ^{[ 1 ] : 4–5}

Sin embargo, si${\displaystyle t'}$es una constante${\displaystyle a}$, entonces${\displaystyle (\langle x\rangle t)a}$es de hecho equivalente a${\displaystyle t[a/x]}$en el sentido de que sustituir todas las variables por algunas constantes en estos dos términos da el mismo resultado (por${\displaystyle \simeq }$). ^{[ 1 ] : 4}

Además, sustituir variables por constantes en${\displaystyle \langle x\rangle t}$siempre se evalúa a un resultado definido, incluso si esto no sería el caso al sustituir variables en${\displaystyle t}$. Por ejemplo, si${\displaystyle a,b\in A}$son dos constantes, el término${\displaystyle \langle x\rangle (ab)}$(abstraer una variable que no aparece) es igual a${\displaystyle S(Ka)(Kb)}$Por los supuestos sobre${\displaystyle K}$y${\displaystyle S}$, esto está bien definido, aunque${\displaystyle ab}$puede que no esté bien definido. ^{[ 1 ] : 4}

Estas observaciones implican que para todos los términos${\displaystyle t(x_{0},\dots ,x_{n})}$, el valor${\displaystyle a:=\langle x_{0}\rangle \dots \langle x_{n}\rangle t\downarrow }$está bien definido y satisface los dos requisitos de completitud combinatoria. ^{[ 1 ] : 4}