Les sémantiques de jeux s'attachent à caractériser le comportement interactif des preuves et des programmes, en les modélisant par des stratégies qui décrivent la façon dont ils réagissent à leur environnement. Afin de prendre en compte les aspects concurrents des preuves en logique linéaire, nous avons été amenés à retravailler les notions et techniques classiques de sémantique des jeux pour les étendre à un cadre asynchrone et non-alterné. Dans une première partie, nous définissons une famille de stratégies asynchrones donnant lieu à un modèle de logique linéaire, pleinement complet pour le fragment multiplicatif. Ces stratégies sont définies de façon locale par une série d'axiomes diagrammatiques ; elles sont ensuite raffinées par un critère dynamique d'ordonnancement, dont nous montrons qu'il impose une version orientée du critère de correction des réseaux de preuve. Cette formulation asynchrone permet d'unifier des modèles variés de la logique linéaire - aussi bien séquentiels que concurrents, dynamiques que statiques - où les preuves sont vues comme des stratégies séquentielles, des stratégies concurrentes, des relations ou des structures d'événements. Dans une seconde partie, nous abordons une autre approche pour décrire la causalité induite par les preuves et introduisons une sémantique de jeux capturant les dépendances engendrées par les connecteurs du premier ordre en logique propositionnelle. Nous montrons que la catégorie résultante peut être finiment présentée par un 2-polygraphe et étudions la possibilité d'orienter cette présentation en un système de réécriture confluent, notamment en introduisant un algorithme d'unification dans ce cadre 2-dimensionnel.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00338643 |
| Date | 01 December 2008 |
| Creators | Mimram, Samuel |
| Publisher | Université Paris-Diderot - Paris VII |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0021 seconds