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. 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 ortogonal a cada miembro de F , es decir, tal que S ⊥ T para todo T ∈ F. Ael espacio coherente F sobre C es una familia de subconjuntos C para los cuales F = ( F ⊥ ) ⊥ .
En Pruebas y tipos, los espacios coherentes se denominan espacios de coherencia. Una nota a pie de página explica que, aunque en el original francés eran espaces cohérents , se utilizó la traducción del espacio de coherencia porque los espacios espectrales a veces se denominan espacios coherentes.
Según lo definido por 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:
Los elementos de los conjuntos en se conocen como tokens y son los elementos del conjunto .
Los espacios de coherencia se corresponden uno a uno con gráficos (no dirigidos) (en el sentido de una biyección del conjunto de espacios de coherencia al de los gráficos no dirigidos). La gráfica correspondiente a que se llama la web de y es la gráfica inducida por un reflexiva , relación simétrica sobre el espacio de contadores de conocida como coherencia módulo define como:
