Sémantique Dynamique Versatile – DYVERSE

L'approche proposée par DyVerSe appartient à la famille des « sémantiques interactives », qui représentent les programmes non pas par des fonctions, mais par leur comportement dynamique en interaction avec leur environnement d'exécution. En particulier, la « sémantique des jeux » représente cette interaction dans un langage inspiré par la théorie des jeux. L'exécution y est représentée par un jeu à deux joueurs échangeant des coups correspondants à des événements calculatoires observables. Par le passé, la sémantique des jeux a eu de nombreux succès pour représenter de façon unifiée de nombreux effets calculatoires, en particulier séquentiels.

Plus précisément, l'outil central de DyVerSe est la « sémantique des jeux causale », qui repose sur des structures mathématiques importées de théorie de la concurrence. Plutôt que représenter l'exécution en listant les événements calculatoires de façon chronologique, la sémantique des jeux causale enregistre la dépendance causale entre ces événements. Capturer des (combinaisons d') effets calculatoires revient alors à comprendre, fondamentalement, quels sont les motifs causaux engendrés par ces combinaisons d'effets.

Plus précisément, DyVerSe s'articule en 5 axes:

A. Comprendre et développer certaines structures causales en vue de leur application à la sémantique.

B. Modéliser plus d'effets calculatoires ou de combinaisons d'effets. Un objectif central, identifié comme verrou scientifique, est la combinaison { concurrence, mémoire partagée, choix probabiliste }, mais DyVerSe ne s'y limite pas.

C. Lier plus fortement ces structures causales à la sémantique opérationnelle des programmes.

D. Les exploiter pour mieux comprendre les systèmes de types tels que celui de Rust, qui contraignent les intéractions (l'interférence) entre phrases de codes séparées.

E. Appliquer ces outils à l'analyse et la vérification de programmes, ainsi qu'à la logique via la « correspondance de Curry-Howard ».

Juste avant le début du projet, de Visme a proposé une notion de structure d’événements pouvant exprimer la combinaison entre choix probabiliste et non-déterministe dans un cadre de concurrence « vraie »; un préalable technique pour la combinaison { concurrence, mémoire partagée, choix probabiliste } visée par DyVerSe.

Au delà du choix probabiliste, Clairambault et de Visme ont précédemment construit un modèle de jeux pour un langage de programmation d'ordre supérieur avec primitives quantiques. Récemment, ils ont montré que ce modèle de jeux était pleinement adéquat, c'est à dire que des programmes sont égalisés par le modèle si et seulement s'ils sont indistinguables. Ils ont également établi un pont avec le modèle relationnel quantique de Pagani, Selinger et Valiron; il s'ensuit que celui-ci était déjà pleinement adéquat.

Également dans l'objectif de lier différents modèles, Blondeau-Patissier et Clairambault ont montré que pour les stratégies innocentes totales finies, l’écrasement vers le modèle relationnel est en réalité injectif, réduisant significativement la distance entre ces deux modèles.

Sur le versant opérationnel, deux travaux sont en cours d'aboutissement:

Castellan et Clairambault ont établit une sémantique opérationnelle, formulée comme une géométrie de l'interaction multi-jetons, pour IPA (langage avec ordre supérieur, mémoire partagée et parallélisme), avec un théorème de dépliage vers le modèle de jeux causaux. La machine d’évaluation résultante pour IPA a été implémentée.

Par ailleurs, Castellan a travaillé à une autre approche d’implémentation des jeux causaux. L’idée est d’éviter la définition habituelle, dénotationnelle, de l’interprétation, et de la présenter à la place comme une traduction monadique du langage source. En résulte une définition plus directe et plus facile à calculer de l’interprétation. De plus, ce développement suggère une nouvelle approche monadique pour la concurrence.

Le travail sur DyVerSe est juste entamé, et suit son cours.

Les travaux récents ont souligné une convergence entre les jeux causaux, et les développements relevant de la « sémantique quantitative » inspirée de la logique linéaire: d'une part, les modèles dits à base de trame (modèles relationnels, espaces de cohérence); et d'autre part le développement de Taylor des lambda-termes. Dans l'optique de créer des ponts entre modèles, et en plus de ses objectifs initiaux, DyVerSe étudiera et développera cette convergence.

Pierre Clairambault, Marc de Visme: Full abstraction for the quantum lambda-calculus. Proc. ACM Program. Lang. 4(POPL): 63:1-63:28 (2020)

Lison Blondeau-Patissier, Pierre Clairambault: Positional Injectivity for Innocent Strategies. Proc. FSCD 2021.

DyVerSe cherche à développer un cadre théorique pour la sémantique dynamique des langages de programmation, capturant de façon unifiée un spectre d'aspects calculatoires, représentatif de l'hétérogénéité du logiciel. Notre ambition est (1) d'aider à unifier la sémantique dénotationnelle en produisant le
chaînon manquant entre divers modèles incompatibles spécialisés sur des effets particuliers, et (2) en extraire une boîte à outils pour raisonner compositionnellement sur la dynamique des programmes, avec en ligne de mire des problèmes de vérification ou spécification.

La sémantique opérationnelle est une méthodologie puissante et extensible, parfaitement adaptée à la formalisation; mais son déploiement s'accompagne
parfois de choix ad-hoc. Elle est liée à la syntaxe, et peine à être compositionnelle. La sémantique dénotationnelle est indépendante de la syntaxe, et se base sur des principes théoriques solides. C'est un excellent outil pour raisonner sur l'équivalence de programmes, ou pour guider la conception de langages, et elle apporte des techniques de raisonnement compositionnels sur les programmes. En échange, elle est mathématiquement plus exigeante et est souvent peu modulaire pour ce qui est des langages: différents fragments d'un même langage peuvent demander des représentations radicalement différentes. Les modèles dénotationnels sont difficilement étendus ou combinés.

DyVerSe chercher à construire le chaînon manquant entre une sémantique opérationnelle liée à la syntaxe, et un spectre de sémantiques dénotationnelles
incomparables et à la porté réduite: une description de l'exécution aussi bien fine qu'indépendante de la syntaxe, qui pourra servir comme une sémantique
opérationnelle unifiée pour de nombreux aspects calculatoires, et comme un pont entre des modèles dénotationnels spécifiques. En plus de construire ce chaînon manquant, DyVerSe propose de l'exploiter pour obtenir des principes de raisonnement sur des langages de haut niveau riches en effets calculatoires, pour permettre une extraction de modèle préalable à la vérification automatique des programmes, ou encore pour examiner les structures utilisées pour éliminer les conflits entre ressources dans les langages tels que Rust.

Pour accomplir ceci, DyVerSe repose sur des développements récents en sémantique des jeux. La sémantique des jeux se distingue de la sémantique
dénotationnelle traditionnelle en représentant le comportement intéractif des programmes plutôt que simplement leur comportement entrée/sortie. Elle a permis de donner un cadre unifié pour la sémantique de nombreux aspects calculatoires (état, opérateurs de contrôle, ordre d'évaluation) pour les programmes déterministes et séquentiels. Cependant, au delà des programmes déterministes et séquentiels, bien qu'il existe des modèles de jeux, ceux-ci sont spécifiques à des effets fixés, et ne s'inscrivent plus dans un cadre unifié. À cet état de fait, des travaux récents suggèrent le diagnostic que les jeux traditionnels ne disposent pas d'une structure assez fine pour représenter le branchement (le parallélisme, le choix non déterministe et le choix probabiliste).

Pour exprimer ce branchement, DyVerSe s'appuie sur les jeux Asynchrones / Concurrents, une branche de la sémantique des jeux représentant la structure
causale sous-tendant les actions des programmes, plutôt que simplement leurs observations par un environnement d'évaluation. Suite à une forte dynamique
récente, les jeux concurrents se rapprochent finalement de l'expressivité des modèles traditionnels, permettant ce programme. DyVerSe poursuivra le
développement des jeux concurrents (leur structure, leur utilisation en sémantique, leur lien avec la sémantique opérationnelle) pour construire le chaînon manquant, et exploitera ces structures pour de meilleurs outils pour vérifier et raisonner sur les programmes.