Est-ce que quelqu'un connaît des exemples de ce qui suit?preuves sur les expressions régulières
Voir Perl Regular Expression Matching is NP-Hard
correspondant Regex est NP-dur quand regexes sont autorisés à avoir des références arrières.
Reduction of 3-CNF-SAT to Perl Regular Expression Matching
[...] 3-CNF-SAT est NP-complet. S'il était un moyen efficace (polynomial) algorithme pour calculer si oui ou non une expression rationnelle correspond une certaine chaîne, nous pourrions l'utiliser pour calculer rapidement solutions au problème 3-CNF-SAT, et, par extension , au problème havresac , le problème vendeur de voyage, etc., etc.
Encore plus que cela: il a été prouvé que le modèle d'expression régulière correspondant aux références arrières était NP-complet par Alfred Aho il y a déjà quelque temps par la réduction du problème de la couverture des sommets. Voir le théorème 6.2 de [A. V. Aho. Algorithmes pour trouver des modèles dans les chaînes. Dans Jan van Leeuwen, éditeur, Handbook of Theoretical Computer Science, volume A: Algorithmes and Complexity, pages 255-300. The MIT Press, 1990]. –
Je ne sais pas de tout développement qui traite des expressions régulières par eux-mêmes.
Les automates finis, pertinents puisque NFAs sont la façon standard de faire correspondre ces expressions régulières, ont été étudiés dans NuPRL. Jetez un oeil à: Robert L. Constable, Paul B. Jackson, Pavel Naumov, Juan Uribe. Constructively Formalizing Automata Theory.
Si vous êtes intéressé par l'approche de ces langages formels via algebra, esp. développant finite semigroup theory, il y a un number de algebra libraries développé dans divers prouveurs de théorème que vous pourriez penser à employer, avec one particularly efficient in a finite setting.
Certified Programming with Dependent Types comporte une section sur la création d'un comparateur d'expressions régulières vérifié. Coq Contribs a un automata contribution qui pourrait être utile. Jan-Oliver Kaiser a formalisé l'équivalence entre les expressions régulières, les automates finis et la caractérisation de Myhill-Nerode en Coq pour son bachelors thesis.
Bon, j'ai aussi noté ce paragraphe dans CPDT il y a quelques semaines. Ça frappe la balle. Selon la contribution des automates, c'est certainement le cas. Cependant, il utilise des axiomes. Par exemple, 4 axiomes dans la preuve que les langages réguliers sont définis par les NFA (module RatReg). Une preuve sans axiomes est également possible (mais pas contenue dans les contributions Coq). –
Moreira, Pereira & de Sousa, On the Mechanisation of Kleene Algebra in Coq donne une belle construction vérifiée de la dérivée Antimirov des regexps dans Coq. Il est assez facile de lire un CFA à partir de cette construction, et de calculer l'intersection des expressions rationnelles. Je ne suis pas sûr de savoir pourquoi vous séparez Coq de la programmation typée dépendante: Coq est essentiellement la programmation dans un lambda-calcul polymorphe de type dépendante avec des types inductifs (c.-à-d. CIC, le calcul des constructions inductives).
Je ne l'ai jamais entendu parler d'une formalisation des expressions régulières dans une langue dépendamment tapé, et je n'ai entendu parler de quelque chose comme un dérivé Antimirov comme pour regexps avec retours en arrière, mais Becchi & Crowley, Extending Finite Automata to Efficiently Match Perl-Compatible Regular Expressions fournir une notion de finie automates d'état qui correspondent à des langages d'expression rationnelle de type Perl. Cela pourrait intéresser les formalisateurs dans un proche avenir.
aide à la preuve navires Isabelle/HOL un certain nombre de preuves officielles concernant les expressions régulières (sans renvoi): http://afp.sourceforge.net/browser_info/devel/HOL/Regular-Sets/
(here est un papier par les auteurs sur ce qu'ils ont fait exactement).
Une autre approche est de caractériser les expressions régulières via Myhill-Nerode Theorem: http://www.dcs.kcl.ac.uk/staff/urbanc/Publications/itp-11.pdf
Selon « Maîtrise des expressions régulières » (un livre que je recommande, voir http://regex.info/) les expressions régulières sont tout à fait non régulière En raison de leurs capacités améliorées, la théorie mathématique n'est disponible que pour les types regex simples/basiques. Est-ce que cela a des implications pour les utiliser dans l'aide à la preuve? –
Oui, c'est le cas: cela rend les preuves plus compliquées :) En fait, par "expressions régulières", je veux dire celles qui sont strictement définies dans la théorie du langage formel. J'aimerais savoir s'il y a eu des tentatives pour spécifier des références arrières ou d'autres constructions non-régulières. Je suis conscient de formalisations assez limitées de r.e. à Nuprl et Coq. Puisque ces formalisations découlaient de la théorie, plutôt que de la pratique de programmation, elles ne tenaient pas compte des caractéristiques non régulières. –