Issue des travaux sur la logique linéaire et l'analyse calculatoire de la logique classique, la notion de polarités semble jouer un rôle essentiel dans l'étude actuelle des systèmes logiques. La polarisation est une contrainte qui simplifie les objets tout en conservant une expressivité suffisante d'un point de vue informatique.<br /><br />L'objet de cette thèse est d'étudier et d'exploiter cette nouvelle structure afin en particulier de mettre à jour les relations entre la logique classique et la logique linéaire (LL). L'introduction des polarités dans LL permet de mieux appréhender ce vaste système et de prolonger le développement de différents outils trop complexes en l'absence de cette contrainte. Nous définissons ainsi, pour la logique linéaire polarisée (LLP), des réseaux de preuve intégrant les connecteurs additifs de manière satisfaisante, une sémantique des jeux polarisés qui réconcilie jeux et dualité, une géométrie de l'interaction parallèle et d'autres sémantiques dénotationnelles basées sur des notions connues (espaces de corrélation, catégories de contrôle).<br /><br />Il est important de montrer que malgré cette contrainte, LLP reste un système suffisamment expressif. Pour cela nous étudions en détail les traductions des différents systèmes de logique classique déterministe connus (LC, lambda-mu calcul, ...) aussi bien en appel par nom qu'en appel par valeur. De surcroît, les traductions obtenues pour ces systèmes sont plus simples que celles vers LL.<br /><br />Enfin la souplesse de ces traductions nous permet d'analyser plus finement certaines propriétés de la logique classique tout comme LL permet d'analyser la logique intuitionniste. On peut ainsi étudier un équivalent linéaire des CPS-traductions.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00007884 |
| Date | 11 March 2002 |
| Creators | Laurent, Olivier |
| Publisher | Université de la Méditerranée - Aix-Marseille II |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0019 seconds