21/06/2001: Virgile Mogbil (IML, Marseille)
Un critère de correction quadratique pour la logique non commutative.
Résumé
La logique non commutative (NL) développée par P.Ruet est une
généralisation de la logique linéaire (LL) et de la logique cyclique
linéaire (extension conservative du calcul de Lambek). C'est à dire que le
calcul des séquents autorise la cohabitation de connecteurs commutatifs et
non commutatifs.
S.Guerrini a montré que la correction des réseaux de preuve multiplicatifs
de LL se fait en temps linéaire. On est loin de ce résultat en logique
non-commutative multiplicative (MNL) : on connaît un critère utilisant les
longs voyages à la J.-Y.Girard (M.Abrusci et P.Ruet) et récemment R.Maieli
en a montré un à la Danos-Regnier. Ils sont donc en temps exponentiel.
Le travail que je vais présenter est une première étape vers un algorithme
en temps linéaire. On établit un critère de contraction pour MNL qui
présente l'avantage d'être en temps quadratique. Il se présente sous la
forme de régles de réécriture inspirées par le calcul des séquents de
MNL. On des résultats de confluence, d'adéquation et de séquentialisation.
Enfin, les précédents critères connus ne fonctionnent pas avec la règle de
coupure alors que celui-ci peux y être étendu sans en changer la
complexité (on a alors de bonnes propriétées comme la préservation de la
correction par élimination des coupures, acyclicité et connexité des
réseaux de preuve de MNL, ...). Il généralise alors le critère de
contraction de V.Danos.