Approches dynamiques en sémantique de la logique linéaire: jeux et géométrie de l'interaction / Patrick Baillot

Auteur: Baillot, Patrick (1972-) - AuteurAuteur secondaire : Girard, Jean-Yves (1947-) - Directeur de thèseCollectivité secondaire: Université d'Aix-Marseille II - Etablissement de soutenanceType de document: ThèseLangue: français ; anglaisPays: FranceÉditeur: [S.l.] : [s.n.], 1999Description: 1 vol. (140 p.) : fig. ; 30 cmRésumé: 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.Bibliographie: Bibliogr. p. 135-137. Index.Thèse: Thèse de doctorat en mathématiques discrètes et fondements de l'informatique, soutenue en 1999, organisme : Aix-Marseille 2 Sujets MSC: 03F05 Mathematical logic and foundations -- Proof theory and constructive mathematics -- Cut-elimination and normal-form theorems
18D10 Category theory; homological algebra -- Categories with structure -- Monoidal categories, symmetric monoidal categories, braided categories
68Q55 Computer science -- Theory of computing -- Semantics
91A40 Game theory, economics, social and behavioral sciences -- Game theory -- Game-theoretic models
97A70 Mathematics education - General, mathematics and education -- Theses and postdoctoral theses
En-ligne: Site de l'auteur
Location Call Number Status Date Due
Salle S 00045-01 / Thèses BAI (Browse Shelf) Available

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

There are no comments for this item.

Log in to your account to post a comment.
Languages: English | Français | |