Hypercohérences et jeux

Cette thèse porte sur les propriétés mathématiques du Calcul et, plus
particulièrement, sur le déterminisme et la séquentialité. Dans une
perspective issue de la théorie de la démonstration, elle porte aussi
sur l’accès aux ressources, avec l’étude des exponentielles de
la Logique Linéaire, ainsi que sur l’interactivité interne du Calcul,
dont la Ludique de J.-Y. Girard tire par ailleurs parti.

Notre point de vue est celui de la sémantique dénotationnelle :
nous modélisons le Calcul en interprétant ses agents par des
objets invariants par exécution. Les modèles sont de deux sortes :
certains, statiques, exhibent des relations qui unissent les agents du
Calcul, et d’autres, dynamiques, focalisent sur l’historique des
interactions entre agents, comme dans la sémantique des jeux où
les agents sont des stratégies.

Le modèle des hypercohérences, où les agents sont des cliques
dans des hypergraphes, bien que statique, a de bonnes propriétés de
séquentialité : T. Ehrhard a montré que les hypercohérences forment le
collapse extensionnel des algorithmes séquentiels. La
dynamique du Calcul y est internalisée : nous la reconstruisons, par
déploiement d’hypergraphes. Nous obtenons des jeux à
bord où les polarités logiques, telles qu’étudiées par
O. Laurent, prévalent. Le bord est le lieu où les calculs terminent.
Dans le cas linéaire il correspond précisément, par effacement des
historiques, au modèle statique des relations.

Les hypercohérences sont un raffinement uniforme de ce dernier
modèle. Uniforme signifie que les agents n’anticipent leurs arguments
que comme produit par d’autres agents. Cette uniformité efface de la
structure du Calcul et limite les possibilités de reconstruction.

Un récent procédé de A. Bucciarelli et T. Ehrhard fournit des modèles
non-uniformes proches des hypercohérences. Nous en améliorons certains
en construisant leur exponentielle libre. Ces modèles
non-uniformes ne sont pas séquentiels mais, chose surprenante, le
déterminisme est au rendez-vous. Le retour à l’uniforme consiste alors
en une restriction simple et immédiate aux lieux de
l’interaction. Ceci fournit un cadre sémantique très modulaire,
idéal pour la comparaison avec les modèles dynamiques.

Ce travail met aussi en évidence une réversibilité temporelle des jeux
à bord, correspondant au passage à l’orthogonal. Nous montrons comment
cette réversibilité suggère une nouvelle lecture des jeux polarisés
d’O. Laurent qui devrait fournir le bon cadre pour
la comparaison avec les hypercohérences.