Soutenance de thèse de MAESTRACCI Valentin
Titre de thèse
Un petit pas vers une logique "Open Source"
A small step towards an Open Source Logic
Résumé de la thèse
Cette thèse porte sur l'étude de modèles de calculs utilisés pour faire de la réalisabilité en logique linéaire (Geometrie de l'Interaction):
-Un premier chapitre explique l'histoire du domaine, en présentant au passage plusieurs modèles de calculs existant dans la littérature.
-Un deuxième chapitre étudie en détail un modèle de calcul précis: les graphes d'interactions de Seiller. On en définit une généralisation comme une instance d'un cadre abstrait nouveau de modele de calcul, dans lequel on prouve la propriété clé d'associativité de l'execution. Ainsi on peut définir un modèle de calcul pour la réalisabilité linéaire pour n'importe quelle instance du cadre. On étudie ensuite une autre instance du cadre qui a la propriété de résoudre un problème qui existait dans une généralisation des graphes d'interaction: les graphes épais. On explique enfin pourquoi le modèle des flots est trop général pour être une instance du cadre.
-Un troisième chapitre porte sur un modèle "intermédiaire": le modèle des étoiles. Ce modèle, définit dans la thèse de Eng, généralise les flots en un sens combinatoire, mais reste proche du cadre. Y est donnée une nouvelle version de ce modèle, ou sont corrigées et rafinnées les définitions et propriétés essentielles, qui bien que pour certaines présente dans la thèse de Eng, posaient problème.
-Un dernier chapitre, très exploratoire, tente de mieux comprendre certaines propriétés combinatoires et géométriques des graphes d'interaction en s'inspirant de domaines des mathématiques (cobordismes, topologie dirigée, catégories). Y est aussi défendu l'idée que la notion de "location statique" est en faite affaire de recollement et de "système ouvert".
Thesis resume
This thesis studies computational models used for realizability for linear logic (as part of Geometry of Interaction):
-A first chapter explains the history of the field, presenting several computational models existing in the literature as well as their connection to linear logic.
-A second chapter studies in detail a specific computational model: Seiller's interaction graphs. We define a generalization of this model, we show that it is an instance of a new, "low-level" framework to define abstract computational model, in which we prove the key property of associativity of execution. This makes it possible to automatically prove this property, and thus to define a computational model for any instance of the framework. We study another instance of the framework solving a problem that existed in a generalization of interaction graphs (thick graphs). Finally, we explain why the model of flows is too general to be an instance of the framework.
-A third chapter focuses on an "intermediate" model: the star model, defined in Eng's thesis, which generalizes flows in a combinatorial sense, but remains somehow similar to the framework defined previously. We study a new version of this model, correcting and refining essential definitions and properties, some of which, although present in Eng's thesis, were problematic.
-The final, highly exploratory chapter, attempts to better understand certain combinatorial and geometric properties of the interaction graph model, drawing inspiration from several areas of mathematics (cobordism, directed spaces, category theory...). We also defend the idea that "static locations" are similar to gluing and to the notion of "open system".