Propriétés de Fermeture des Grammaires Générales -- Formellement Vérifiées

Informations Fondamentales

• Identifiant de l'article: 2302.06420
• Titre: Closure Properties of General Grammars -- Formally Verified
• Auteurs: Martin Dvorak (Institute of Science and Technology Austria), Jasmin Blanchette (Ludwig-Maximilians-Universität München)
• Classification: cs.FL (Langages Formels et Théorie des Automates)
• Conférence de Publication: 14ème Conférence Internationale sur la Vérification Interactive de Théorèmes (ITP 2023)
• Lien de l'article: https://arxiv.org/abs/2302.06420

Résumé

Cet article formalise les grammaires générales (c'est-à-dire les grammaires de type 0) en utilisant l'assistant de preuve Lean 3. Les auteurs définissent les concepts fondamentaux des règles de réécriture et des mots dérivés par une grammaire, et prouvent que la classe des langages de type 0 est fermée sous quatre opérations : l'union, l'inversion, la concaténation et l'étoile de Kleene. La littérature se concentre principalement sur les arguments basés sur les machines de Turing, qui pourraient être plus difficiles à formaliser. Pour l'étoile de Kleene, les auteurs n'ont pas pu suivre la littérature et ont proposé leur propre construction basée sur les grammaires.

Contexte de Recherche et Motivation

Contexte du Problème

1. Importance de la théorie des langages formels: Les concepts de langages formels sont au cœur de l'informatique et peuvent être reconnus par plusieurs formalismes, notamment les machines de Turing et les grammaires formelles
2. Équivalence entre les grammaires de type 0 et les machines de Turing: Les machines de Turing et les grammaires générales caractérisent la même classe de langages énumérables récursivement ou langages de type 0
3. Limitations des travaux de formalisation existants: Bien qu'il existe de nombreux travaux sur la formalisation des machines de Turing dans les assistants de preuve, les travaux de formalisation des grammaires générales sont relativement rares

Motivation de la Recherche

1. Avantages des grammaires: Les grammaires générales sont plus faciles à définir que les machines de Turing, et certaines preuves concernant les grammaires générales sont beaucoup plus simples que les preuves analogues pour les machines de Turing
2. Importance des propriétés de fermeture: Les propriétés de fermeture des langages de type 0 sont des résultats fondamentaux de la théorie des langages formels
3. Besoin de vérification formelle: Il est nécessaire de disposer de preuves vérifiées par machine pour assurer l'exactitude de ces résultats fondamentaux

Contributions Principales

1. Première formalisation complète des grammaires générales: Définition complète des concepts fondamentaux et des opérations des grammaires de type 0 en Lean 3
2. Preuves formalisées de quatre propriétés de fermeture:
   • Fermeture sous l'union
   • Fermeture sous l'inversion
   • Fermeture sous la concaténation
   • Fermeture sous l'étoile de Kleene
3. Construction innovante de l'étoile de Kleene: Faute de construction basée sur les grammaires dans la littérature, les auteurs ont inventé leur propre méthode de construction fondée sur les grammaires
4. Cadre d'abstraction réutilisable: Développement de la structure lifted_grammar pour réduire la duplication de code et fournir des modèles de preuve génériques
5. Base de code Lean open-source d'environ 12 500 lignes: Fourniture d'une implémentation formelle complète pour la communauté

Détails de la Méthode

Structure des Définitions Fondamentales

Système de Symboles

inductive symbol (T : Type) (N : Type)
| terminal : T → symbol  
| nonterminal : N → symbol

Représentation des Règles de Grammaire

structure grule (T : Type) (N : Type) :=
( input_L : list (symbol T N))
( input_N : N)  
( input_R : list (symbol T N))
( output_string : list (symbol T N))

Définition de la Grammaire

structure grammar (T : Type) :=
(nt : Type)
(initial : nt)
(rules : list (grule T nt))

Définitions des Opérations Principales

Relation de Transformation de Grammaire

def grammar_transforms (g : grammar T) (w1 w2 : list (symbol T g.nt)) : Prop :=
∃ r : grule T g.nt,
  r ∈ g.rules ∧
  ∃ u v : list (symbol T g.nt),
    w1 = u ++ r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R ++ v ∧
    w2 = u ++ r.output_string ++ v

Relation de Dérivation

def grammar_derives (g : grammar T) : 
  list (symbol T g.nt) → list (symbol T g.nt) → Prop :=
relation.refl_trans_gen (grammar_transforms g)

Points d'Innovation Technique

1. Cadre d'Abstraction lifted_grammar

Pour réduire la duplication de code, les auteurs ont développé une structure d'abstraction :

• Contient une grammaire plus petite g0 et une grammaire plus grande g
• Fournit les fonctions lift_nt et sink_nt pour la conversion entre différents types de non-terminaux
• Assure l'injectivité et la correction des règles correspondantes

2. Traitement Innovant de la Concaténation

La construction classique de concaténation pour les grammaires hors-contexte échoue pour les grammaires générales. La solution des auteurs :

• Crée des non-terminaux proxy pour chaque terminal
• Assure une séparation complète des non-terminaux utilisés par g1 et g2
• Évite les problèmes d'appariement de chaînes au-delà des frontières de concaténation

3. Construction Originale de l'Étoile de Kleene

Faute de construction basée sur les grammaires dans la littérature, les auteurs ont inventé une nouvelle méthode :

• Introduit un séparateur # pour construire des « compartiments » isolant les mots
• Utilise un nettoyeur R qui traverse de haut en bas et supprime les séparateurs
• Nouvel ensemble de règles : P* = P ∪ {Z → ZS#, Z → R#, R# → R, R# → ε} ∪ {Rt → tR | t ∈ T}

Configuration Expérimentale

Environnement de Formalisation

• Assistant de preuve: Lean 3
• Bibliothèque mathématique: mathlib
• Échelle du code: Environ 12 500 lignes de code Lean bien formaté
• Métaprogrammation: Utilisation du cadre de métaprogrammation de Lean pour développer une petite automatisation

Méthode de Vérification

• Induction structurelle: Preuves par induction structurelle sur les relations de dérivation
• Analyse de cas: Analyse exhaustive des différents cas d'application de règles
• Maintenance des invariants: Maintien des invariants clés dans les preuves complexes

Résultats Expérimentaux

Théorèmes Principaux

1. Fermeture sous l'union: theorem T0_of_T0_u_T0 (L1 L2 : language T) : is_T0 L1 ∧ is_T0 L2 → is_T0 (L1 + L2)
2. Fermeture sous l'inversion: theorem T0_of_reverse_T0 (L : language T) : is_T0 L → is_T0 (reverse_lang L)
3. Fermeture sous la concaténation: theorem T0_of_T0_c_T0 (L1 L2 : language T) : is_T0 L1 ∧ is_T0 L2 → is_T0 (L1 * L2)
4. Fermeture sous l'étoile de Kleene: theorem T0_of_star_T0 (L : language T) : is_T0 L → is_T0 L.star

Analyse de la Complexité des Preuves

• Union et inversion: Relativement simples, utilisant principalement des constructions standard
• Concaténation: Complexité moyenne, nécessitant de traiter les problèmes d'appariement aux frontières
• Étoile de Kleene: La plus complexe, le seul lemme star_induction dépassant 3 000 lignes de code

Résultats Secondaires

• Grammaires hors-contexte: Les preuves peuvent être réutilisées pour établir la fermeture des langages hors-contexte
• Lemmes de concaténation: theorem CF_of_CF_u_CF et autres peuvent être directement appliqués aux langages hors-contexte

Travaux Connexes

Formalisation des Grammaires

• Grammaires hors-contexte: Carlson et al. (Mizar), Minamide (Isabelle/HOL), Barthwal et Norrish (HOL4), Firsov et Uustalu (Agda), Ramos (Coq)
• Grammaires générales: Cet article est la première formalisation complète

Autres Modèles de Calcul

• Automates finis: Thompson et Dillies (Lean), formalisations d'expressions régulières
• Machines de Turing: Implémentations dans plusieurs assistants de preuve, les travaux récents de Balbach prouvant même le théorème de Cook-Levin
• Calcul lambda: Norrish (HOL4), Forster et al. (Coq)
• Fonctions partiellement récursives: Norrish (HOL4), Carneiro (Lean)

Conclusion et Discussion

Conclusions Principales

1. Les grammaires surpassent les machines de Turing: Pour les preuves de propriétés de fermeture, les grammaires peuvent être plus pratiques que les machines de Turing
2. Faisabilité de la formalisation: Les résultats complexes de la théorie des langages peuvent être formalisés avec succès dans les assistants de preuve modernes
3. Importance de l'abstraction: Les bonnes abstractions (comme lifted_grammar) sont cruciales pour la formalisation à grande échelle

Limitations

1. Classes de complexité: Les grammaires ne peuvent pas définir les classes de complexité importantes (comme la classe P), nécessitant toujours des modèles comme les machines de Turing
2. Constructivité: Les auteurs n'ont pas tenté de rendre le développement constructif
3. Fermeture sous l'intersection: La fermeture sous l'intersection n'a pas été formalisée, car aucune construction élégante basée uniquement sur les grammaires n'est connue

Directions Futures

1. Hiérarchie de Chomsky complète: Intégration des grammaires sensibles au contexte, hors-contexte et régulières dans la bibliothèque
2. Preuves d'équivalence: Tentative de preuve de l'équivalence entre les grammaires générales et les machines de Turing
3. Connexion avec mathlib: Liaison des résultats mathlib sur les langages réguliers avec cette bibliothèque

Évaluation Approfondie

Points Forts

1. Travail novateur: Première formalisation complète des grammaires générales, comblant une lacune importante
2. Innovation technique: La construction originale de l'étoile de Kleene démontre une profonde maîtrise théorique
3. Qualité d'ingénierie: 12 500 lignes de code de haute qualité avec une conception d'abstraction excellente
4. Contribution théorique: Preuve que les méthodes basées sur les grammaires sont supérieures aux méthodes basées sur les machines de Turing dans certains cas
5. Réutilisabilité: Les abstractions comme lifted_grammar fournissent une base pour les travaux futurs

Insuffisances

1. Limitations d'expressivité: Incapacité à traiter les concepts importants de la théorie de la complexité
2. Absence de constructivité: Absence de considération pour les exigences des mathématiques constructives
3. Complétude: Absence de traitement d'opérations importantes comme l'intersection
4. Documentation: Certains détails techniques pourraient être expliqués plus en détail

Impact

1. Signification théorique: Pose les fondations pour la vérification mécanique de la théorie des langages formels
2. Valeur méthodologique: Démontre les meilleures pratiques pour les projets de formalisation à grande échelle
3. Contribution à la communauté: La base de code open-source favorisera les recherches connexes
4. Valeur pédagogique: Peut servir d'excellent cas d'étude pour l'apprentissage des méthodes formelles

Domaines d'Application

1. Informatique théorique: Recherche en théorie des langages et théorie des automates
2. Mathématiques formalisées: Recherche mathématique nécessitant des preuves rigoureuses
3. Vérification de compilateurs: Garanties de correction pour l'analyse syntaxique et le traitement des langages
4. Enseignement: Matériel d'appui pour les cours de langages formels

Références Bibliographiques

L'article cite 26 références importantes, couvrant :

• Manuels classiques : Théorie de l'analyse d'Aho & Ullman, Théorie des automates de Hopcroft et al.
• Travaux de formalisation : Implémentations de modèles de calcul dans divers assistants de preuve
• Documentation des outils : Documentation pertinente de Lean 3 et mathlib

Résumé: Cet article est un travail de haute qualité en informatique théorique qui apporte non seulement des contributions techniques importantes, mais fournit également une expérience précieuse en méthodologie de formalisation. Le travail des auteurs pose les fondations solides pour la construction d'une hiérarchie de Chomsky formalisée complète et possède une valeur importante pour la théorie des langages formels et la communauté des assistants de preuve.