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)

Lionel Vaux Auclair
I2M, Aix-Marseille
https://www.i2m.univ-amu.fr/perso/lionel.vaux/

Date(s) : 05/10/2023   iCal
11 h 00 min - 12 h 30 min

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.

Emplacement
Site Sud, Luminy, Ancienne BU

Catégories



Retour en haut 

Secured By miniOrange