Nets between determinism and nondeterminism
Paolo Tranquilli · OpenGrey (Institut de l'Information Scientifique et Technique) · 2009
Cette these de theorie de la demonstration etudie les proprietes de la syntaxe parallele de la logique lineaire (LL) de Girard, les reseaux de preuve. La premiere partie presente le terrain commun sur lequel s'appuient les parties suivantes. En particulier, le paradigme des reseaux d'interaction de Lafont est utilise pour presenter les principaux objets de recherche de la these : d'un cote, les reseaux de preuve de Hughes et van Glabbeek pour la logique lineaire multiplicative additive (MAIL) ; de l'autre, les reseaux differentiels d'Ehrhard et Regnier pour la logique lineaire differentielle (DiLL) obtenue en ajoutant des operateurs differentiels a LL multiplicative exponentielle. Dans la deuxieme partie, nous nous concentrons sur MALL, en etudiant ses relations avec la semantique denotationnelle des espace hypercoherents d'Ehrhard. Un critere est etabli sur les reseaux de preuve de MALL caracterisant ceux interpretes (par la notion d'experience de Girard) comme des hypercliques, c'est-a-dire des objets des espaces hypercoherents. On montre ensuite la stabilite de ce critere par reduction des coupures. Dans la troisieme partie, nous passons a DiLL. Nous prouvons la confluence des reseaux purs de DiLL en utilisant un resultat de developpements finis. Ensuite, nous montrons un theoreme correspondant a la standardisation de LL (recemment prouve par Pagani et Tortora de Falco), a partir duquel la normalisation forte du cas simplement type peut etre deduite. Enfin, nous presentons une version du lambda-calcul avec ressources de Boudol, ainsi qu'une traduction de celle-ci dans les reseaux intuitionnistes de DiLL. Cette traduction permet de prouver la confluence de ce calcul.