Dans les réseaux de démonstration, on peut sauter à l’élastique en toute sécurité (et c’est la preuve de séquentialisation du LLHandbook)
Date(s) : 05/10/2023 iCal
11h00 - 12h30
Dans un cours d’introduction à la logique linéaire, si on parle de réseaux, on énonce généralement un résultat de séquentialisation : tout réseau est la traduction d’une dérivation. Parfois même, on le prouve. Je propose de faire exactement ça, pour les réseaux multiplicatifs.
Je mobiliserai une technique nouvelle baptisée « saut à l’élastique » : dans un réseau, si on considère un cycle, il contient forcément des ponts (un pont = un passage par un ⅋, en arrivant par une prémisse et en repartant par l’autre) ; et si le cycle respecte des conditions raisonnables (qu’on sait toujours satisfaire), alors on peut s’élancer depuis n’importe quel pont sans risque de revenir taper dans le cycle.
Avec ce résultat sous la main, on peut montrer que les arêtes (ou nœuds) maximaux pour un certain ordre naturellement induit par le critère de Danos-Regnier ont des tas de bonnes propriétés.
Ceci est (une partie d’)un travail en commun et en cours avec Rémi Di Guardia, Olivier Laurent et Lorenzo Tortora de Falco, réinvesti dans la partie « réseaux pour les enfants » du brouillon courant du LLHandbook.
Catégories
