Subsitutions explicites, logique et normalisation

• Main Author: Polonovski, Emmanuel
• Language: FRE
• Published: Université Paris-Diderot - Paris VII 2004
• Subjects: [INFO:INFO_MO] Computer Science/Modeling and Simulation; [INFO:INFO_SE] Computer Science/Software Engineering; lambda-calcul; substitutions explicites; réécriture; calcul symétrique; normalisation; logique classique; logique linéaire; réseaux de preuve
• Online Access: http://tel.archives-ouvertes.fr/tel-00007962; http://tel.archives-ouvertes.fr/docs/00/04/75/43/PDF/tel-00007962.pdf

Les substitutions explicites ont été introduites comme un raffinement du lambda-calcul, celui-ci étant le<br />formalisme utilisé pour étudier la sémantique des langages de programmation. L'objet de cette thèse<br />est l'étude de leurs propriétés de normalisation forte et de préservation de la normalisation forte. Ce<br />manuscrit rend compte de plusieurs travaux autour de ces propriétés de normalisation, regroupés en<br />trois volets.<br /><br />Le premier d'entre eux formalise une technique générale de preuve de normalisation forte utilisant<br />la préservation de la normalisation forte. On applique cette technique à un spectre assez large de calculs<br />avec substitutions explicites afin de mesurer les limites de son utilisation. Grâce à cette technique, on<br />prouve un résultat nouveau : la normalisation forte du lambda-upsilon-calcul simplement typé.<br /><br />Le deuxième travail est l'étude de la normalisation d'un calcul symétrique non-déterministe issu de<br />la logique classique formulée dans le calcul des séquents, auquel est ajouté des substitutions explicites.<br />La conjonction des problèmes posés par les calculs symétriques et ceux posés par les substitutions<br />explicites semble vouer à l'échec l'utilisation de preuves par réductibilité. On utilise alors la technique<br />formalisée dans le premier travail, ce qui nous demande de prouver tout d'abord la préservation de la<br />normalisation forte. A cette fin, on utilise un fragment de la théorie de la perpétuité dans les systèmes<br />de réécriture.<br /><br />La définition d'une nouvelle version du lambda-ws-calcul avec nom, le lambda-wsn-calcul, constitue le troisième<br />volet de la thèse. Pour prouver sa normalisation forte par traduction et simulation dans les réseaux<br />de preuve, on enrichit l'élimination des coupures de ceux-ci avec une nouvelle règle, ce qui nous oblige<br />à prouver que cette nouvelle notion de réduction est fortement normalisante.