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.