Categorical combinatorics for non-déterministic innocent strategies
Combinatoire catégorielle pour les stratégies innocentes non-déterministes
par Clément JACQ sous la direction de Paul-André MELLIÈS
Thèse de doctorat en Mathématiques. Logique et fondements de l'informatique
ED 386 Sciences Mathematiques de Paris Centre

Soutenue le mardi 03 décembre 2019 à Université Paris Cité

Sujets
  • Langages de programmation
  • Logique mathématique
  • Sémantique selon la théorie des jeux

Les thèses de doctorat soutenues à Université Paris Cité sont déposées au format électronique

Consultation de la thèse sur d’autres sites :

Theses.fr

Description en anglais
Description en français
Mots clés
Modèles bicategoriels de la logique linéaire, Stratégies innocentes
Resumé
Il y a vingt-cinq ans, Hyland et Ong ont résolu le problème de l'abstaction pour le langage PCF en construisant une sémantique des jeux basées sur la notion fondamentale de stratégie innocente. Dans cette thèse, nous continuons leurs travaux et construisons une bicatégorie de stratégies innocentes et non-déterministes étendant leur modèle original de jeux déterministiques et innocents.Notre point de départ est fourni par l'approche combinatoire des stratégies innocentes développée par Harmer, Hyland et Melliès dans un article publié il y a douze ans. Dans ces travaux, ils élaborent une description combinatoire de la structure de pointeur des jeux d'arènes, et prouvent que l'innocence peut être obtenue en se servant d'un nombre de propriétés catégorielles remarquables, plus particulièrement l'existence d'une loi distributive entre la monade générant les Vues Joueurs et la comonade générant les Vues Opposants.Dans cette thèse, nous étudions en détail la reconstruction du modèle de jeux innocents décrit par Harmer, Hyland et Melliès, et étendons ce modèle dans deux directions. Dans la première direction, nous expliquons comment voir le modèle de Harmer, Hyland et Melliès en tant qu'instance d'une catégorie de dialogue, une notion initiallement introduite par Melliès, en se servant de la symétrie entre Joueur et Opposant dans les catégories de jeux et stratégies. Dans la seconde direction, nous construisons une sémantique des jeux bicatégorielle de PCF non-déterministe en équipant chaque jeu d'un pré-faisceau des stratégies non-déterministes, au lieu d'un ensemble de stratégies. Pour opérer ce changement de dimension d'ensemble à pré-faisceau, nous adaptons les constructions catégorielles du modèle Harmer-Hyland-Melliès, et construisons une loi pseudo-distributive entre la pseudo-monade générant les Vues Joueurs et la pseudo-comonade générant les Vues Opposants dans notre modèle non-déterministe. Nous obtenons ainsi une bicatégorie de jeux, stratégies non-déterministes et simulations, que nous comparons avec des formules alternatives de sémantiques des jeux non-déterministes et innocentes apparaissant dans la littérature