Pouvez-vous expliquer une intuition derrière les espaces cohérents?

La logique linéaire est interprétée en utilisant des espaces cohérents , et ils figurent en bonne place dans les articles de Girard. Je connais les trois principales façons de les définir formellement, et ils ne posent pas vraiment de problème pour utiliser et prouver des choses, mais je ne comprends tout simplement pas ce qu'ils signifient .

J'ai vraiment l'impression qu'il existe une sorte de moyen de les comprendre . Tout d'abord, il y a quelques exemples à leur sujet qui utilisent des fonctions sur les booléens (comme sur un wiki quelque part ). Et cela fait allusion à quelque chose d'intéressant et de significatif derrière la définition formelle. Cependant, boolc'est un espace cohérent très simple, sans clique de taille > 1. Quelqu'un peut-il élaborer?

Une autre chose que Girard dit quelque part que chaque point d'un espace cohérent représente une "séquence de questions / réponses" spécifique, deux points étant cohérents s'ils "bifurquent négativement (c'est-à-dire sur des questions différentes)", et incohérents s'ils bifurquent sur des réponses différentes [1]. Cela semble être une idée facile à saisir, mais je ne peux tout simplement pas inventer un exemple, donc cela signifie que je ne l'ai pas vraiment compris ...

Quelqu'un pourrait-il m'aider s'il vous plaît?

[1] JY Girard, Le fantôme de la transparence . URL: http://iml.univ-mrs.fr/~girard/longo1.pdf

L'intuition derrière les espaces de cohérence est que les éléments d'un espace de cohérence représentent des observations de certaines données sous-jacentes, et la relation de cohérence vous indique si deux observations auraient pu provenir de la même donnée.

Concrètement, supposons que nous ayons un ensemble d'animaux

Animals = {cat, duck, fish}

Maintenant, nous pouvons avoir un ensemble d'observations:

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

Disons que deux observations sont compatibles si elles peuvent toutes deux être faites du même animal. Chaque observation est compatible avec elle-même, et en plus:

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

Nous savons qu'être à sang chaud est compatible avec la natation, car les canards sont à la fois à sang chaud et nagent. Mais être à sang chaud et respirer l'eau ne sont pas compatibles, car nous n'avons pas d'animaux à la fois à sang chaud et à eau.

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

J'ai toujours eu du mal à former une intuition pour les espaces de cohérence, jusqu'à ce que je me familiarise avec la théorie des domaines et que je lise «Le système F des types variables, quinze ans plus tard» de Girard. Les espaces de cohérence ne sont qu'un type particulier de domaine, et j'ai trouvé beaucoup plus facile de comprendre ce que signifie la cohérence à partir de là. Je vais essayer de donner une explication qui avait plus ou moins de sens pour moi.

Imaginez que vous vouliez étudier des programmes qui prennent des entrées entières en sorties entières. En général, ces programmes peuvent boucler indéfiniment, il est donc logique de les modéliser mathématiquement en tant que fonctions partielles d'entiers en entiers: si le programme boucle, la fonction partielle correspondante n'est pas définie sur cette entrée. Nous pouvons voir une telle fonction partielle fcomme un graphique : un ensemble de paires d'entiers (n, m)tel que fdéfini sur net égal à m. Cela nous permet de représenter ces fonctions comme un espace de cohérence:

• La toile de l'espace de cohérence est l'ensemble des paires d'entiers (n, m).
• Deux paires (n, m)et (n', m')sont cohérentes si et seulement si net n'sont différentes, ou met m'sont égales.

En décompactant les définitions, nous voyons que chaque clique de cet espace de cohérence est le graphe d'une fonction partielle, et vice versa. Nous pouvons interpréter la relation de cohérence comme disant que, une fonction partielle est définie sur une entrée, elle ne produit qu'un seul résultat pour cette entrée. Si vous êtes habitué à d'autres types de sémantique théorique du domaine, l'inclusion de cliques correspond à l'ordre de Scott habituel sur les fonctions partielles sur les entiers.