Pourquoi des graphes réflexifs pour la paramétricité?

En regardant les modèles de polymorphisme paramétrique, je suis curieux de savoir pourquoi les catégories de graphe réflexif sont utilisées?

En particulier, pourquoi n'incluent-ils pas la composition relationnelle? En regardant les modèles, ils semblent tous soutenir une notion naturelle de composition relationnelle:

$$x(R;S)z \iff \exists y. xRy \wedge y S z$$

La plupart des articles récents qui utilisent des graphiques réflexifs semblent tenir cela pour acquis, et le seul article plus ancien que j'ai pu trouver qui a discuté était «Relational Parametricity and Local Variables» par O'Hearn et Tennent qui disent:

Une raison pour ne pas exiger la composabilité est que, comme cela est bien connu, la composition n'est pas préservée par des relations logiques à des types supérieurs.

Et je ne suis pas tout à fait sûr de ce que cela signifie, donc ma première question est de savoir ce que cela signifie et, espérons-le, une meilleure référence sur cette question.

Je pense que cela signifie que, par exemple, l'exponentielle ne préserve pas nécessairement la composition relationnelle du nez. En particulier, nous ne pouvons pas montrer . Cela signifie que l'exponentielle ne s'étend pas à un foncteur sur une catégorie de relations.$(R;R') \to (S;S') \equiv ((R \to S);(R' \to S'))$

Cependant, bien que je ne puisse pas montrer l'équivalence entre les relations ci-dessus, je peux certainement prouver une inclusion , non?$((R \to S);(R' \to S')) \subset ((R;R') \to (S;S'))$

Étant donné , alors il existe un de type approprié avec , donc étant donné un , je peux montrer . Cela ne signifie-t-il pas que l'exponentielle me donne un foncteur laxiste , ce qui semble être une mauvaise propriété à jeter? Ma deuxième question est donc: y a-t-il des exemples où l'inclusion dans cette direction n'est pas non plus prouvable?$f((R \to S);(R' \to S')) h$$g$$f(R\to S)g(R'\to S')h$$xRyR'z$$f(x) S g(y) S' h(z)$

Dans les mois qui se sont écoulés depuis que j'ai posé cette question, je pense avoir trouvé une réponse sensée.

Souvent, le type de relations envisagé ne se compose pas . Par exemple, si votre notion d'une relation entre ω CPO est un sous-ensemble complet de chaînes ω de | D | × | E | , alors la relation R : ω + 1 → N entre les naturels ordonnés plus l'infini ω + 1 et le CPO plat des naturels N donné par R ( n , n ) tient et rien d'autre, alors$R : D \to E$$\omega$$\omega$$|D|\times |E|$$R : \omega + 1 \to \mathbb{N}$$\omega+1$$\mathbb{N}$$R(n,n)$ est admissible, tout comme son contraire, mais le composite R ; R T : ω + 1 → ω + 1 n'est pas une chaîne complète, car n R ; R T n pour tout naturel, mais nous n'avons pas ω R ; R T ω .$R$$R;R^T : \omega+1 \to \omega + 1$$n R;R^T n$$\omega R; R^T \omega$