Espacio coherente

En la teoría de la prueba , un espacio coherente (también espacio de coherencia) es un concepto introducido en el estudio semántico de la lógica lineal .

Sea un conjunto C dado. Se dice que dos subconjuntos S , T ⊆ C son ortogonales , escritos S ⊥ T , si S ∩ T es ∅ o un singleton . El dual de una familia F ⊆ ℘( C ) es la familia F ^⊥ de todos los subconjuntos S ⊆ C ortogonales a cada miembro de F , es decir, tales que S ⊥ T para todo T ∈ F . Un espacio coherente F sobre C es una familia de C -subconjuntos para los cuales F = ( F ^⊥ ) ^⊥ .

En Demostraciones y tipos, los espacios coherentes se denominan espacios de coherencia. Una nota al pie explica que, si bien en el original francés se denominaban espaces cohérents , se utilizó la traducción espacio de coherencia porque los espacios espectrales a veces se denominan espacios coherentes.

Definiciones

Según la definición de Jean-Yves Girard , un espacio de coherencia es una colección de conjuntos que satisfacen el cierre descendente y la completitud binaria en el siguiente sentido: ${\displaystyle {\mathcal {A}}}$

• Cierre hacia abajo: todos los subconjuntos de un conjunto permanecen en : ${\displaystyle {\mathcal {A}}}$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle a'\subset a\in {\mathcal {A}}\implies a'\in {\mathcal {A}}}$
• Completitud binaria: para cualquier subconjunto de , si la unión por pares de cualquiera de sus elementos está en , entonces también lo está la unión de todos los elementos de : ${\displaystyle M}$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle M}$ ${\displaystyle \forall M\subset {\mathcal {A}},\left((\forall a_{1},a_{2}\in M,\ a_{1}\cup a_{2}\in {\mathcal {A}})\implies \bigcup M\in {\mathcal {A}}\right)}$

Los elementos de los conjuntos en se conocen como tokens , y son los elementos del conjunto . ${\displaystyle {\mathcal {A}}}$ ${\displaystyle |{\mathcal {A}}|=\bigcup {\mathcal {A}}=\{\alpha |\{\alpha \}\in {\mathcal {A}}\}}$

Los espacios de coherencia se corresponden uno a uno con los grafos (no dirigidos) (en el sentido de una biyección del conjunto de espacios de coherencia al de grafos no dirigidos). El grafo correspondiente a se llama red de y es el grafo inducido por una relación reflexiva y simétrica sobre el espacio de tokens de conocida como coherencia módulo definida como: En la red de , los nodos son tokens de y se comparte una arista entre nodos y cuando (es decir , .) Este grafo es único para cada espacio de coherencia y, en particular, los elementos de son exactamente las camarillas de la red de es decir, los conjuntos de nodos cuyos elementos son adyacentes por pares (comparten una arista .) ${\displaystyle {\mathcal {A}}}$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle \sim }$ ${\displaystyle |{\mathcal {A}}|}$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle {\mathcal {A}}}$ $${\displaystyle a\sim b\iff \{a,b\}\in {\mathcal {A}}}$$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle |{\mathcal {A}}|}$ ${\displaystyle a}$ ${\displaystyle b}$ ${\displaystyle a\sim b}$ ${\displaystyle \{a,b\}\in {\mathcal {A}}}$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle {\mathcal {A}}}$

Los espacios de coherencia como tipos

Los espacios de coherencia pueden actuar como una interpretación de los tipos en la teoría de tipos , donde los puntos de un tipo son puntos del espacio de coherencia . Esto permite que se discuta cierta estructura sobre los tipos. Por ejemplo, a cada término de un tipo se le puede dar un conjunto de aproximaciones finitas que, de hecho, es un conjunto dirigido con la relación de subconjunto. Al ser un subconjunto coherente del espacio de tokens (es decir, un elemento de ), cualquier elemento de es un subconjunto finito de y, por lo tanto, también coherente, y tenemos ${\displaystyle {\mathcal {A}}}$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle a}$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle I}$ ${\displaystyle a}$ ${\displaystyle |{\mathcal {A}}|}$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle I}$ ${\displaystyle a}$ ${\displaystyle a=\bigcup a_{i},a_{i}\in I.}$

Funciones estables

Las funciones entre tipos se consideran funciones estables entre espacios de coherencia. Una función estable se define como aquella que respeta aproximaciones y satisface un cierto axioma de estabilidad. Formalmente, es una función estable cuando ${\displaystyle {\mathcal {A}}\to {\mathcal {B}}}$ ${\displaystyle F:{\mathcal {A}}\to {\mathcal {B}}}$

1. Es monótono con respecto al orden del subconjunto (respeta la aproximación, categóricamente , es un funtor sobre el poset ): ${\displaystyle {\mathcal {A}}}$ ${\displaystyle a'\subset a\in {\mathcal {A}}\implies F(a')\subset F(a).}$
2. Es continua (categóricamente, conserva los colimites filtrados ): donde es la unión dirigida sobre , el conjunto de aproximantes finitos de . ${\textstyle F(\bigcup _{i\in I}^{\uparrow }a_{i})=\bigcup _{i\in I}^{\uparrow }F(a_{i})}$ ${\textstyle \bigcup _{i\in I}^{\uparrow }}$ ${\displaystyle I}$ ${\displaystyle a}$
3. Es estable : Categóricamente, esto significa que preserva el retroceso : ${\displaystyle a_{1}\cup a_{2}\in {\mathcal {A}}\implies F(a_{1}\cap a_{2})=F(a_{1})\cap F(a_{2}).}$

   

Espacio de productos

Para ser consideradas estables, las funciones de dos argumentos deben satisfacer el criterio 3 anterior en esta forma: lo que significaría que además de la estabilidad en cada argumento solo, el retroceso $${\displaystyle a_{1}\cup a_{2}\in {\mathcal {A}}\land b_{1}\cup b_{2}\in {\mathcal {B}}\implies F(a_{1}\cap a_{2},b_{1}\cap b_{2})=F(a_{1},b_{1})\cap F(a_{2},b_{2})}$$

se conserva con funciones estables de dos argumentos. Esto conduce a la definición de un espacio de producto que realiza una biyección entre funciones binarias estables (funciones de dos argumentos) y funciones unarias estables (un argumento) sobre el espacio de producto. El espacio de coherencia de producto es un producto en el sentido categórico, es decir, satisface la propiedad universal de los productos. Se define por las ecuaciones: ${\displaystyle {\mathcal {A}}\ \&\ {\mathcal {B}}}$

• ${\displaystyle |{\mathcal {A}}\ \&\ {\mathcal {B}}|=|{\mathcal {A}}|+|{\mathcal {B}}|=(\{1\}\times |{\mathcal {A}}|)\cup (\{2\}\times |{\mathcal {B}}|)}$(es decir, el conjunto de tokens de es el coproducto (o unión disjunta ) de los conjuntos de tokens de y . ${\displaystyle {\mathcal {A}}\ \&\ {\mathcal {B}}}$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle {\mathcal {B}}}$
• Los tokens de diferentes conjuntos son siempre coherentes y los tokens del mismo conjunto son coherentes exactamente cuando son coherentes en ese conjunto.
  • ${\displaystyle (1,\alpha )\sim _{{\mathcal {A}}\ \&\ {\mathcal {B}}}(1,\alpha ')\iff \alpha \sim _{\mathcal {A}}\alpha '}$
  • ${\displaystyle (2,\beta )\sim _{{\mathcal {A}}\ \&\ {\mathcal {B}}}(2,\beta ')\iff \beta \sim _{\mathcal {B}}\beta '}$
  • ${\displaystyle (1,\alpha )\sim _{{\mathcal {A}}\ \&\ {\mathcal {B}}}(2,\beta ),\forall \alpha \in |{\mathcal {A}}|,\beta \in |{\mathcal {B}}|}$

Referencias

• Girard, J.-Y .; Lafont, Y.; Taylor, P. (1989), Pruebas y tipos (PDF) , Cambridge University Press.
• Girard, J.-Y. (2004), "Entre la lógica y la cuántica: un tratado", en Ehrhard; Girard; Ruet; et al. (eds.), Lógica lineal en informática (PDF) , Cambridge University Press.