Matteo Acclavio
I2M, Aix-Marseille Université
http://matteoacclavio.com/Math.html
Date(s) : 14/12/2016 iCal
14 h 00 min - 15 h 30 min
Soutenance de thèse
–
Dans le dernier siècle, nombreux sciences ont enrichi leur syntaxe pour pouvoir modeler des interactions. Entre eux on peut compter l’informatique, la physique quantique, et aussi la biologie et l’économie : toutes ces sciences sont des exemples de domaines qui ont besoin d’une syntaxe et d’une sémantique soit pour la concurrence que pour la séquentialité.
Les diagrammes des cordes sont bien adaptés à cet effet. Dans leur syntaxe on peut retrouver deux compositions : une composition parallèle et une composition séquentielle, qui peuvent interagir à travers une loi d’interchange. Si on considère cette loi comme une égalité, les diagrammes de cordes sont une syntaxe pour les catégories monoidales strictes, avec une représentation graphique plus intuitive que les formules algébriques traditionnelles.
Dans cette thèse, on étudie cette syntaxe de dimension 2 et sa sémantique. On considère la réécriture des diagrammes et on donne des applications de cette méthode :
• une preuve détaillée du théorème de cohérence de Mac Lane pour les catégories monoidales symétriques basée sur un système de réécriture convergent donnée en arXiv:1606.01722 ;
• une interprétation des dérivations de preuves avec les diagrammes de preuve pour le fragment MELL de la logique linéaire, qui capture l’équivalence de preuves. On peut vérifier la séquentialité en temps linéaire, c’est à dire vérifier si un diagramme corresponds à une preuve. Cette interprétation est une extension de celle pour le fragment MLL donnée en arXiv:1606.09016 en donnant aussi un résultat de élimination du coupure.
–
Abstract : String diagram rewriting: applications in category and proof theory
In the last century, several sciences enriched their syntax in order to model interactions. Not only computer science and quantum physics, but also biology and economics are examples of fields requiring syntax and semantics for concurrency as well as for sequentiality.Retour ligne automatique
String diagrams are suitable for that purpose. In that syntax, we have two compositions : the parallel one and the sequential one, which may interact by the interchange rule. If we consider this rule as an equality, string diagrams are a syntax for strict monoidal categories, with a more intuitive graphical representation than traditional algebraic formulas.Retour ligne automatique
In this thesis, we study this 2-dimensional syntax and its semantics. We consider diagram rewriting and we give two applications of those methods :Retour ligne automatique
• a detailed proof of Mac Lane’s coherence theorem for symmetric monoidal categories based on convergent diagram rewriting, which is given in arXiv:1606.01722 ;Retour ligne automatique
• an interpretation of proof derivations by string diagrams for the MELL fragment of linear logic, which captures proof equivalence. We get a linear sequentializability test to verify if a diagram corresponds to a proof . This interpretation extends the one for the MLL fragment given in arXiv:1606.09016, providing also a cut-elimination result.
–
Membres du jury :
Directeur de thèse
– Yves LAFONT (I2M, Marseille)
–
Rapporteurs proposés :
– Willem HEIJLTIES (Lecturer & Prize fellow, Bath)
– Samuel MIMRAM (CR HDR, Ecole Polytechnique)
– Pierre-Louis CURIEN (DR, INRIA Paris)
–
Autres membres du jury :
– Michele ABRUSCI (Professore Ordinario, Roma 3)
– Myriam QUATRINI (MCF HDR, AMU, I2M, Marseille)
– Luigi SANTOCANALE (PR, AMU)
– Lorenzo TORTORA de FALCO (Professore Associato, Roma 3)
–
Liens :
– theses.fr
– SUDOC Abes
Catégories