¿Puedes explicar una intuición detrás de los espacios coherentes?

La lógica lineal se interpreta utilizando espacios coherentes , y ocupan un lugar destacado en los documentos de Girard. Conozco las tres formas principales de definirlas formalmente, y realmente no plantean ningún problema para usar y probar cosas, pero no puedo entender lo que significan .

Realmente parece que hay algún tipo de forma de entenderlos . En primer lugar, hay algunos ejemplos sobre ellos que usan funciones en booleanos (como en un wiki en alguna parte ). Y sugiere algo interesante y significativo detrás de la definición formal. Sin embargo, booles un espacio coherente muy simple, sin una camarilla de tamaño > 1. ¿Alguien puede dar más detalles?

Otra cosa que Girard dice en alguna parte es que cada punto de un espacio coherente representa una "secuencia de preguntas / respuestas" específica, con dos puntos coherentes si "se bifurcan negativamente (es decir, en preguntas diferentes)", e incoherente si se bifurcan en respuestas diferentes [1] Parece una idea fácil de entender, pero no puedo inventar un ejemplo, así que realmente no lo entiendo ...

¿Podría alguien ayudarme con eso?

[1] JY Girard, El fantasma de la transparencia . URL: http://iml.univ-mrs.fr/~girard/longo1.pdf

La intuición detrás de los espacios de coherencia es que los elementos de un espacio de coherencia representan observaciones de algunos datos subyacentes, y la relación de coherencia le dice si dos observaciones podrían provenir del mismo dato.

Concretamente, supongamos que tenemos un conjunto de animales

Animals = {cat, duck, fish}

Ahora, podemos tener un conjunto de observaciones:

Observations = {warm-blooded, swims, water-breathing, furry}

Digamos que dos observaciones son compatibles si ambas pudieran hacerse del mismo animal. Cada observación es compatible consigo misma, y ​​además:

• de sangre caliente peludo$\stackrel{{\large\frown}}{{\small\smile}}$
• sangre caliente nada$\stackrel{{\large\frown}}{{\small\smile}}$
• de sangre caliente peludo$\stackrel{{\large\frown}}{{\small\smile}}$
• nada respirando agua$\stackrel{{\large\frown}}{{\small\smile}}$

Sabemos que ser de sangre caliente es compatible con la natación, porque los patos son de sangre caliente y nadan. Pero ser de sangre caliente y respirar agua no son compatibles, ya que no tenemos animales que sean de sangre caliente y respiren agua.

Observations$\stackrel{{\large\frown}}{{\small\smile}}$Observations$\stackrel{{\large\frown}}{{\small\smile}}$

Siempre tuve problemas para formar una intuición para los espacios de coherencia, hasta que me familiaricé más con la teoría de dominios y leí "El sistema F de tipos variables, de Girard, quince años después". Los espacios de coherencia son solo un tipo especial de dominio, y me resultó mucho más fácil entender qué significa coherencia a partir de ahí. Trataré de dar una explicación que tenga más o menos sentido para mí.

Imagine que desea estudiar programas que llevan entradas enteras a salidas enteras. En general, estos programas pueden repetirse para siempre, por lo que tiene sentido modelarlos matemáticamente como funciones parciales de enteros a enteros: si el programa se repite, la función parcial correspondiente no está definida en esa entrada. Podemos ver una función ftan parcial como un gráfico : un conjunto de pares de enteros (n, m)tal que fse define en ne igual a m. Esto nos permite representar estas funciones como un espacio de coherencia:

• La red del espacio de coherencia es el conjunto de pares de enteros (n, m).
• Dos pares (n, m)y (n', m')son coherentes si y solo si ny n'son diferentes, o my m'son iguales.

Al desempacar las definiciones, vemos que cada camarilla de este espacio de coherencia es el gráfico de funciones parciales, y viceversa. Podemos interpretar la relación de coherencia como diciendo que, una función parcial se define en una entrada, solo produce un resultado para esa entrada. Si está acostumbrado a otros tipos de semántica teórica de dominio, la inclusión de camarillas corresponde al orden habitual de Scott en funciones parciales en enteros.