Fragments de logique linéaire non-commutative avec complexité sous-algébrique

Informations fondamentales

• ID de l'article: 2511.02348
• Titre: Non-commutative linear logic fragments with sub-context-free complexity
• Auteurs: Yusaku Nishimiya (University of Illinois Springfield & RIKEN AIP), Masaya Taniguchi (RIKEN AIP)
• Classification: cs.LO (Logique en informatique), cs.CC (Complexité computationnelle), cs.FL (Langages formels), math.LO (Logique mathématique)
• Date de publication: 4 novembre 2025 (prépublication arXiv)
• Lien de l'article: https://arxiv.org/abs/2511.02348

Résumé

Cet article propose de nouvelles caractérisations de complexité descriptive pour trois classes de langages : les langages réguliers (REG), les langages algébriques linéaires (LCFL) et les langages algébriques (CFL), obtenues en restreignant les règles d'inférence, la taille des formules et les connecteurs autorisés dans le calcul de Lambek. Le calcul de Lambek est un fragment de la logique linéaire non-commutative et intuitioniste avec des implications sensibles à la direction. Les auteurs identifient pour la première fois des fragments du calcul de Lambek possédant une complexité de preuve REG et LCFL, et démontrent que les variantes logiques « les plus faibles » n'autorisant qu'une seule règle d'inférence possèdent une complexité CFL. Les preuves reposent sur des traductions directes entre les grammaires de logique de type et les grammaires formelles, ainsi que sur l'induction structurelle sur les séquents prouvables, ce qui constitue une approche plus simple et plus intuitive que les travaux antérieurs.

Contexte et motivation de la recherche

Contexte du problème

1. Étude de la logique substructurelle: Les théoriciens de la preuve étudient la logique substructurelle pour comprendre l'impact de l'autorisation ou de l'élimination des règles structurelles sur les propriétés des systèmes de preuve, généralement présentés sous forme de calculs de séquents.
2. Signification computationnelle de la logique linéaire: La logique linéaire (LL) restreint les règles de contraction et d'affaiblissement, rendant les preuves plus conscientes des ressources que dans la logique classique, et donc plus pertinentes pour le calcul. Il est connu que MALL est PSPACE-complet et MLL est NP-complet.
3. Pouvoir expressif du calcul de Lambek: Le calcul de Lambek L est le fragment intuitionniste, non-commutatif et multiplicatif de LL, avec des implications sensibles à la direction. Pentus a prouvé l'équivalence entre les grammaires de Lambek et les grammaires algébriques, mais aucun fragment de L correspondant aux classes de langages inférieures dans la hiérarchie de Chomsky n'a été identifié.

Motivation de la recherche

Les recherches existantes offrent peu de compréhension de la complexité computationnelle des fragments « plus faibles » de LL, en particulier en l'absence de caractérisation des fragments du calcul de Lambek correspondant aux langages réguliers et algébriques linéaires. Cet article vise à combler cette lacune en établissant des correspondances précises entre la taille des formules logiques et les restrictions directionnelles d'une part, et les variations du pouvoir expressif des grammaires d'autre part.

Contributions principales

1. Identification inédite: Identification pour la première fois de fragments du calcul de Lambek possédant une complexité de preuve REG et LCFL
2. Complexité CFL des variantes minimales: Démonstration que les variantes logiques n'autorisant qu'une seule règle d'inférence possèdent une complexité CFL
3. Méthode de traduction directe: Fourniture de traductions directes entre les grammaires de logique de type et les grammaires formelles, ainsi que de méthodes d'induction structurelle
4. Application du théorème d'élimination de la coupure: Établissement de l'utilité conceptuelle du théorème d'élimination de la coupure dans la comparaison entre les grammaires formelles et les calculs de séquents
5. Analogie de la forme normale de Greibach: Identification de l'analogue précis de la forme normale de Greibach dans les grammaires de Lambek

Détails méthodologiques

Définition de la tâche

Cet article étudie comment caractériser les classes de langages formels de différentes complexités en restreignant les règles d'inférence, la taille des formules et les connecteurs du calcul de Lambek. La tâche spécifique consiste à établir des relations d'équivalence entre les fragments du calcul de Lambek et les classes de langages dans la hiérarchie de Chomsky.

Cadre théorique

Définition du calcul de Lambek

Le calcul de Lambek L comprend:

• Axiome: α → α
• Règle de coupure: De Γ,α,Θ → β et Δ → α, déduire Γ,Δ,Θ → β
• Six règles d'inférence: Impliquant les trois connecteurs binaires /, \ et ·

Concepts clés

1. Degré de type d(α): Nombre d'occurrences distinctes de connecteurs dans le type α
2. Ensembles de types: Tp(/) désigne l'ensemble des types contenant uniquement le connecteur /, Tpn désigne l'ensemble des types de degré ≤ n
3. Grammaire de Lambek: Quadruplet (Pr, V, SG, f), où f est une fonction d'assignation de types

Théorèmes principaux

Théorème 2 (Résultat principal): Les trois paires suivantes de grammaires de fragments de Lambek et de grammaires formelles possèdent un pouvoir expressif équivalent:

• Grammaires L(/ →) avec Tp(/) ⇔ CFG
• Grammaires L(/ →, \ →) avec Tp1(/, ) ⇔ LCFG
• Grammaires L(/ →) avec Tp1(/) ⇔ REG

Stratégie de preuve

Conditions de réductibilité (Lemme 3)

Pour une séquence de types non-vide Γ dans Tp(/), L(/ →) ⊢ Γ → SG si et seulement si:

1. Γ = α,Δ1,...,Δn, où α a la forme (···((S/βn)/βn-1)/···)/β1
2. Pour tous 1≤k≤n, L(/ →) ⊢ Δk → βk

Méthode de construction

1. CFG vers grammaire de Lambek: En supposant la forme normale de Greibach, transformer les règles de production A → aB1···Bn en assignation de type (···((A/Bn)/Bn-1)/···)/B1 ∈ f(a)
2. Grammaire de Lambek vers CFG: Transformer l'assignation de type (···((α/βn)/βn-1)/···)/β1 ∈ f(a) en règle de production α → aβ1β2···βn

Configuration expérimentale

Cet article constitue une recherche purement théorique sans vérification expérimentale, mais établit plutôt des relations d'équivalence par des preuves mathématiques rigoureuses.

Méthodes de preuve

1. Induction structurelle: Induction structurelle sur les séquents prouvables
2. Élimination de la coupure: Utilisation du théorème de Gentzen pour garantir l'existence de preuves sans coupure
3. Construction bidirectionnelle: Preuve séparée de l'équivalence des langages dans les deux directions

Résultats expérimentaux

Résultats principaux

Proposition 4 (Langages algébriques)

Les grammaires de Lambek basées sur L(/ →) avec Tp(/) reconnaissent exactement les langages algébriques ne contenant pas la chaîne vide.

Points clés de la preuve:

• CFG → Grammaire L(/ →): Utilisation de la forme normale de Greibach, construction de l'assignation de type correspondante
• Grammaire L(/ →) → CFG: Transformation de l'assignation de type en règles de production, preuve de l'équivalence des langages par induction

Proposition 6 (Langages algébriques linéaires)

Les grammaires L(/ →, \ →) restreintes à Tp1(/, ) reconnaissent exactement les langages linéaires.

Méthode de construction:

• A/B ∈ f(a) ⟺ A → aB ∈ P (linéaire à droite)
• B\A ∈ f(a) ⟺ A → Ba ∈ P (linéaire à gauche)
• A ∈ f(a) ⟺ A → a ∈ P (terminal)

Corollaire 7 (Langages réguliers)

Les grammaires L(/ →) restreintes à Tp1(/) reconnaissent exactement les langages réguliers.

Découvertes clés

1. Importance de la directionnalité: Les grammaires L(/ →) unidirectionnelles correspondent aux grammaires régulières à droite, tandis que les grammaires L(/ →, \ →) bidirectionnelles correspondent aux grammaires linéaires
2. Rôle des restrictions de degré: La restriction du degré de type à 1 correspond naturellement à la (bi)linéarité des règles de production
3. Analogie de la forme normale de Greibach: Les grammaires L(/ →) unidirectionnelles peuvent être considérées comme l'analogue théorique de la preuve de la forme normale de Greibach

Travaux connexes

Recherche sur la complexité de la logique linéaire

• MALL: PSPACE-complet LMSS92
• MLL: NP-complet Kan91
• Calcul de Lambek: NP-complet Pen06

Grammaires de Lambek et grammaires formelles

• Conjecture de Chomsky: Équivalence entre les grammaires de logique de type et les grammaires algébriques Cho63
• Résultat de Pentus: Confirmation de la conjecture de Chomsky et preuve que les grammaires de Lambek sans produit restent algébriques Pen93, Pen97
• Abrusci: Établissement du lien entre le calcul de Lambek et la logique linéaire Abr90

Conclusion et discussion

Conclusions principales

1. Caractérisation précise: Établissement de correspondances précises entre les fragments du calcul de Lambek et trois classes importantes de langages dans la hiérarchie de Chomsky
2. Simplification des méthodes: Fourniture de méthodes de preuve plus directes et plus intuitives que les travaux antérieurs
3. Intuitions théoriques: Révélation des connexions profondes entre les règles d'inférence logique et les règles de production des grammaires formelles

Limitations

1. Portée limitée: Considération uniquement de certaines classes de langages dans la hiérarchie de Chomsky
2. Traitement de la chaîne vide: Les grammaires construites n'incluent pas la chaîne vide
3. Applications pratiques: Résultats principalement théoriques, la valeur d'application pratique reste à explorer

Directions futures

Les auteurs proposent trois directions de recherche prometteuses:

1. Étude de la complexité descriptive à grain fin d'autres fragments de logique linéaire (non-commutative)
2. Identification des grammaires de Lambek équivalentes aux langages sans étoile, langages légèrement sensibles au contexte, systèmes de Lindenmayer, etc.
3. Interaction entre la sémantique de la logique linéaire et les caractérisations de théorie géométrique des groupes des langages formels

Évaluation approfondie

Avantages

1. Innovation théorique: Établissement inédit de correspondances entre REG et LCFL et les fragments du calcul de Lambek, comblant une lacune théorique importante
2. Simplicité méthodologique: Les méthodes de preuve basées sur la traduction directe et l'induction structurelle sont plus simples et plus intuitives que les travaux antérieurs
3. Complétude des résultats: Fourniture de caractérisations complètes pour trois classes de langages importantes, formant un cadre théorique unifié
4. Clarté conceptuelle: L'application du théorème d'élimination de la coupure et l'analogie de la forme normale de Greibach fournissent des intuitions théoriques profondes

Insuffisances

1. Limitations d'application: En tant que recherche purement théorique, manque de discussion sur les scénarios d'application pratique
2. Portée limitée: Implication uniquement de parties de la hiérarchie de Chomsky, sans traitement des classes de langages de niveau supérieur
3. Détails techniques: Certaines étapes de preuve pourraient être plus détaillées, en particulier la mise en œuvre concrète de l'induction structurelle

Impact

1. Contribution théorique: Fourniture de nouveaux outils théoriques pour la recherche interdisciplinaire entre la logique substructurelle et la théorie des langages formels
2. Valeur méthodologique: La méthode de traduction directe peut s'appliquer à l'étude des correspondances entre d'autres systèmes logiques et modèles computationnels
3. Développement disciplinaire: Promotion de la fusion ultérieure entre la logique et la théorie de la complexité computationnelle

Scénarios applicables

1. Informatique théorique: Fourniture de nouvelles méthodes pour étudier la complexité computationnelle des systèmes logiques
2. Théorie des langages formels: Fourniture de nouvelles perspectives pour la caractérisation logique des classes de langages
3. Traitement du langage naturel: Potentiel pour fournir une base théorique à l'analyse syntaxique basée sur la logique de type
4. Recherche en théorie de la preuve: Fourniture d'outils techniques pour la recherche ultérieure en logique substructurelle

Références bibliographiques

L'article cite les références clés du domaine, notamment:

• Travaux fondateurs de Girard sur la logique linéaire Gir87
• Travaux originaux de Lambek Lam58
• Résultats importants de Pentus sur le pouvoir expressif des grammaires de Lambek Pen93, Pen97
• Résultats classiques sur la complexité de la logique linéaire LMSS92, Kan91

Cet article fournit une contribution théorique importante à la recherche interdisciplinaire entre la logique substructurelle et la théorie des langages formels. En établissant des correspondances précises, il non seulement résout des problèmes théoriques de longue date, mais pose également des fondations solides pour des recherches ultérieures. Ses méthodes de preuve concises et ses intuitions théoriques profondes en font un progrès important dans ce domaine.