Você pode explicar uma intuição por trás dos Espaços Coerentes?

A lógica linear é interpretada usando espaços coerentes , e eles aparecem com destaque nos papéis de Girard. Conheço todas as três principais maneiras de defini-las formalmente, e elas realmente não apresentam nenhum problema para usar e provar coisas, mas simplesmente não consigo entender o que elas significam .

Realmente parece que existe algum tipo de maneira de entendê- las. Primeiro de tudo, existem alguns exemplos sobre eles que usam funções em booleanos (como em um wiki em algum lugar ). E isso sugere algo interessante e significativo por trás da definição formal. No entanto, boolé um espaço coerente muito simples, sem cliques de tamanho > 1. Alguém pode elaborar?

Outra coisa que Girard diz em algum lugar que todo ponto de um espaço coerente representa uma "sequência de perguntas / respostas" específica, com dois pontos sendo coerentes se "bifurcam negativamente (ou seja, em perguntas diferentes)" e incoerentes se bifurcam em respostas diferentes [1] Parece uma idéia fácil de entender, mas eu simplesmente não consigo inventar um exemplo, então isso significa que eu realmente não entendo ...

Alguém poderia me ajudar com isso?

[1] JY Girard, O fantasma da transparência . URL: http://iml.univ-mrs.fr/~girard/longo1.pdf

A intuição por trás dos espaços de coerência é que os elementos de um espaço de coerência representam observações de alguns dados subjacentes, e a relação de coerência informa se duas observações poderiam ter vindo do mesmo dado.

Concretamente, suponha que tenhamos um conjunto de animais

Animals = {cat, duck, fish}

Agora, podemos ter um conjunto de observações:

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

Digamos que duas observações sejam compatíveis se ambas puderem ser feitas do mesmo animal. Toda observação é compatível consigo mesma e, além disso:

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

Sabemos que ser de sangue quente é compatível com a natação, porque os patos são de sangue quente e nadam. Mas ser de sangue quente e respirar pela água não são compatíveis, uma vez que não temos animais com sangue quente e respirando na água.

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

Eu sempre tive problemas para formar uma intuição para espaços de coerência, até me familiarizar com a teoria de domínio e ler o "Sistema F de tipos variáveis, de quinze anos depois", de Girard. Os espaços de coerência são apenas um tipo especial de domínio, e achei muito mais fácil entender o que significa coerência a partir daí. Vou tentar dar uma explicação que fez mais ou menos sentido para mim.

Imagine que você deseja estudar programas que levam entradas inteiras para saídas inteiras. Em geral, esses programas podem repetir-se para sempre; portanto, faz sentido modelá-los matematicamente como funções parciais de inteiros para inteiros: se o programa for repetido, a função parcial correspondente será indefinida nessa entrada. Podemos visualizar uma função parcial fcomo um gráfico : um conjunto de pares de números inteiros (n, m), fdefinidos ne iguais a m. Isso nos permite representar essas funções como um espaço de coerência:

• A teia do espaço de coerência é o conjunto de pares de números inteiros (n, m).
• Dois pares (n, m)e (n', m')são coerentes se e somente se ne n'são diferentes, ou mem' são iguais.

Ao descompactar as definições, vemos que cada clique desse espaço de coerência é o gráfico de uma função parcial e vice-versa. Podemos interpretar a relação de coerência como dizendo que, uma função parcial é definida em uma entrada, ela produz apenas um resultado para essa entrada. Se você está acostumado a outros tipos de semântica teórica de domínio, a inclusão de cliques corresponde à ordem usual de Scott em funções parciais em números inteiros.