Qualcuno conosce qualche esempio di quanto segue?prove sulle espressioni regolari
Vedi Perl Regular Expression Matching is NP-Hard
Regex matching è NP-difficile quando espressioni regolari sono autorizzati ad avere backreference.
Reduction of 3-CNF-SAT to Perl Regular Expression Matching
[...] 3-CNF-SAT è NP-completo. Se non ci erano una (polinomiale) efficiente algoritmo per il calcolo se o meno una regex corrisponde una certa stringa, si potuto usarlo per calcolare rapidamente soluzioni al problema 3-CNF-SAT, e, per estensione , per il problema dello zaino , il commesso viaggiatore problema, ecc ecc
Anche più di questo: il pattern di espressioni regolari che corrisponde a backreferences è stato dimostrato essere già NP-completo da Alfred Aho un po 'di tempo fa con la riduzione del problema di cover vertice. Vedi il Teorema 6.2 da [A. V. Aho. Algoritmi per la ricerca di schemi nelle stringhe. In Jan van Leeuwen, editore, Handbook of Theoretical Computer Science, volume A: Algorithms and Complexity, pagine 255-300. The MIT Press, 1990]. –
non so di qualsiasi sviluppo che tratta le espressioni regolari da loro stessi.
Gli automi finiti, tuttavia rilevanti dal NFAs sono il modo standard per abbinare tali espressioni regolari, sono stati studiati in NuPRL. Date un'occhiata a: Robert L. Constable, Paul B. Jackson, Pavel Naumov, Juan Uribe. Constructively Formalizing Automata Theory.
Se sei interessato ad avvicinarti a quei linguaggi formali tramite algebra, esp. sviluppando finite semigroup theory, ci sono uno number di algebra libraries sviluppato in vari teoremi che si potrebbe pensare di utilizzare, con one particularly efficient in a finite setting.
Certified Programming with Dependent Types ha una sezione sulla creazione di un verificatore di espressioni regolari verificato. Coq Contribs ha un automata contribution che potrebbe essere utile. Jan-Oliver Kaiser ha formalizzato l'equivalenza tra espressioni regolari, automi finiti e la caratterizzazione di Myhill-Nerode in Coq per il suo bachelors thesis.
Giusto, ho anche notato questo paragrafo in CPDT alcune settimane fa. Colpisce la palla. Come per il contributo degli automi, lo è certamente. Tuttavia, usa gli assiomi. Ad esempio, 4 assiomi nella dimostrazione che le lingue regolari sono definite dagli NFA (modulo RatReg). È anche possibile una dimostrazione senza assiomi (ma non contenuta nei contributi di Coq). –
Moreira, Pereira & de Sousa, On the Mechanisation of Kleene Algebra in Coq dà una bella costruzione verificata del derivato Antimirov di regexps in Coq. È abbastanza facile leggere un CFA da questa costruzione e calcolare l'intersezione delle espressioni regolari.
Non sono sicuro del motivo per cui si separa il Coq dalla programmazione tipizzata in modo dipendente: Coq essenzialmente è la programmazione in un calcolo lambda tipicamente tipizzato polimorfico con tipi induttivi (cioè CIC, il calcolo delle costruzioni induttive).
Non ho mai sentito parlare di una formalizzazione di espressioni regolari in una lingua dipendente tipizzato, né ho sentito parlare di qualcosa come un derivato Antimirov simile per espressioni regolari con backtracking, ma Becchi & Crowley, Extending Finite Automata to Efficiently Match Perl-Compatible Regular Expressions fornire una nozione di finite- stato automata che corrisponde a un linguaggio regexp simile a Perl. Ciò potrebbe attrarre i formalisti nel prossimo futuro.
l'assistente prova di Isabelle/HOL navi un numero di prove formali riguardanti le espressioni regolari (senza riferimento indietro): http://afp.sourceforge.net/browser_info/devel/HOL/Regular-Sets/
(here è una carta da parte degli autori per quanto riguarda quello che hanno fatto esattamente).
Un altro approccio è quello di caratterizzare le espressioni regolari via Myhill-Nerode Theorem: http://www.dcs.kcl.ac.uk/staff/urbanc/Publications/itp-11.pdf
Secondo "Mastering Regular Expressions" (un libro che consiglio, vedi http://regex.info/) le espressioni regolari sono abbastanza non regolare Infatti, grazie alle loro capacità potenziate, la teoria matematica è disponibile solo per i tipi di espressioni regolari semplici/di base. Questo ha implicazioni per usarli nell'assistenza alla prova? –
Sì, lo fa: rende le prove più complicate :) Infatti, per "espressioni regolari" intendo quelle fondamentali che sono strettamente definite nella teoria del linguaggio formale. Mi piacerebbe sapere se ci sono stati tentativi di specificare backward o altre costruzioni non regolari. Sono a conoscenza di formalizzazioni piuttosto limitate di base r.e. in Nuprl e Coq. Dal momento che queste formalizzazioni derivavano dalla teoria, piuttosto che dalla pratica della programmazione, non rendevano conto delle caratteristiche non regolari. –