Approches dynamiques en sémantique de la logique linéaire : jeux et géométrie de l'interaction / Patrick Baillot ; sous la direction de Jean-Yves Girard

Bibliogr. p. 135-137. Index

Thèse de doctorat mathématiques discrètes et fondements de l'informatique 1999 Aix-Marseille 2

Cette thèse concerne le calcul, sous la forme de la normalisation des preuves de la logique linéaire. Elle vise à explorer les liens entre trois domaines de la théorie de la démonstration. La sémantique dénotationnelle interprète les preuves par des invariants extensionnels de la normalisation. La géométrie de l'interaction (GdI) décrit les preuves comme des objets communiquant et le calcul comme un flot d'information (l'exécution) circulant entre ces objets. La sémantique des jeux occupe une position intermédiaire : les preuves sont des stratégies qui admettent une description extensionnelle à la manière de la sémantique dénotationnelle, mais également dynamique à la manière de la GdI. Nous donnons une nouvelle preuve de définissabilité pour le modèle de Hyland-Ong de la logique linéaire multiplicative utilisant le critère de correction des longs voyages pour les réseaux. Nous associons ensuite une application à tout réseau multiplicatif exponentiel ; cette application permet de calculer l'interprétation d'une preuve intuitionniste (IMELL) dans le modèle d'Abramsky-Jagadeesan-Malacaria. Nous définissons un modèle de jeux (modèle des stratégies saturées) pour la logique linéaire classique (MELL) et étudions ses liens avec la GdI. Nous le comparons ensuite à des modèles dénotationnels en décrivant un (pseudo-)foncteur d'oubli du temps de ce modèle vers une variante du modèle relationnel : le modèle des relations pointées. Deux raffinements de ce dernier modèle sont étudiés : les espaces de positions bipolarisées et les ordres polarisés ; pour chacun nous établissons des liens précis avec le modèle de jeux. La dernière partie aborde le problème des bornes de complexité en GdI : nous introduisons un modèle de clauses permettant l'interprétation de la logique linéaire élémentaire et définissons une variante de l'exécution terminant en temps élémentaire