Kennt jemand Beispiele für die folgenden?Beweise über reguläre Ausdrücke
Siehe Perl Regular Expression Matching is NP-Hard
Regex Matching ist NP-schwer, wenn reguläre Ausdrücke erlaubt sind Rückreferenzierungen zu haben.
Reduction of 3-CNF-SAT to Perl Regular Expression Matching
[...] 3-CNF-SAT ist NP-vollständig. Wenn es eine effiziente (Polynom-Zeit) ist Algorithmus zur Berechnung, ob oder nicht ein regulären Ausdruck eine bestimmte Zeichenfolge abgestimmt, wir könnten es verwenden, um schnell Lösungen für das 3-CNF-SAT Problem zu berechnen, und durch Erweiterung auf den Ranzen Problem, der Handlungsreis Problem, etc. etc.
Mehr noch: Reguläre Expressionsmuster, die mit Rückreferenzen übereinstimmen, wurden von Alfred Aho schon vor einiger Zeit durch Reduktion aus dem Vertex-Coverage-Problem als NP-vollständig nachgewiesen. Siehe Satz 6.2 von [A. V. Aho. Algorithmen zum Finden von Mustern in Strings. In Jan van Leeuwen, Herausgeber, Handbuch der theoretischen Informatik, Band A: Algorithmen und Komplexität, Seiten 255-300. Die MIT-Presse, 1990]. –
ich weiß nicht jeder Entwicklung, die reguläre Ausdrücke für sich behandelt.
Finite Automaten, jedoch relevant seit NFAs sind die Standardmethode, um diese regulären Ausdrücke zu entsprechen, wurden in NuPRL untersucht. Schau dir an: Robert L. Constable, Paul B. Jackson, Pavel Naumov, Juan Uribe. Constructively Formalizing Automata Theory.
Sollten Sie daran interessiert sein, diese formalen Sprachen durch algebra, esp. entwickelt finite semigroup theory, gibt es eine number von algebra libraries in verschiedenen Theorem-Prüfer entwickelt, die Sie verwenden könnten, mit one particularly efficient in a finite setting.
Certified Programming with Dependent Types enthält einen Abschnitt zum Erstellen eines überprüften Matcher für reguläre Ausdrücke. Coq Contribs hat eine automata contribution, die nützlich sein könnte. Jan-Oliver Kaiser formalisierte die Gleichwertigkeit zwischen regulären Ausdrücken, endlichen Automaten und der Myhill-Nerode-Charakterisierung in Coq für seine bachelors thesis.
Richtig, ich habe diesen Absatz in CPDT vor ein paar Wochen auch notiert. Es trifft den Ball. Gemäss dem Automatenbeitrag ist es sicher. Es verwendet jedoch Axiome. Zum Beispiel 4 Axiome in dem Beweis, dass reguläre Sprachen durch NFAs definiert sind (Modul RatReg). Ein Beweis ohne Axiome ist ebenfalls möglich (aber nicht in den Coq-Beiträgen enthalten). –
Moreira, Pereira & de Sousa, On the Mechanisation of Kleene Algebra in Coq gibt eine schön verifizierte Konstruktion des Antimirov-Derivats von Regexps in Coq. Es ist ziemlich einfach, einen CFA von dieser Konstruktion abzulesen und die Schnittmenge von Regexps zu berechnen.
Ich bin nicht sicher, warum Sie Coq von abhängig typisierten Programmierung zu trennen: Coq ist im Wesentlichen Programmieren in einem polymorphen abhängig typed Lambda-Kalkül mit induktiven Typen (d. H. CIC, der Kalkül der induktiven Konstruktionen).
Ich habe noch nie von einer Formalisierung von regexps in einer abhängig typisierte Sprache gehört, noch habe ich etwas wie ein Antimirov artigen Derivat für regexps mit Rückziehern gehört, aber Becchi & Crowley, bietet Extending Finite Automata to Efficiently Match Perl-Compatible Regular Expressions eine Vorstellung von endlichen Automaten, die mit Perl-ähnlichen Regexp-Sprachen übereinstimmen. Das könnte in naher Zukunft für Formalisierer attraktiv sein.
Der Beweis Assistent Isabelle/HOL Schiffe eine Reihe von formalisierten Beweisen in Bezug auf reguläre Ausdrücke (ohne Rückbezug): http://afp.sourceforge.net/browser_info/devel/HOL/Regular-Sets/
(here ist ein Papier von den Autoren in Bezug auf was sie taten genau).
Ein weiterer Ansatz ist reguläre Ausdrücke über Myhill-Nerode Theorem zu charakterisieren: http://www.dcs.kcl.ac.uk/staff/urbanc/Publications/itp-11.pdf
Laut „Reguläre Ausdrücke“ (ein Buch, das ich empfehlen, siehe http://regex.info/) reguläre Ausdrücke durchaus nicht regelmäßig sind in Aufgrund ihrer verbesserten Fähigkeiten ist die mathematische Theorie nur für einfache Regex-Typen verfügbar. Hat das Auswirkungen auf die Verwendung in der Proof-Unterstützung? –
Ja, tut es: es macht Beweise komplizierter :) In der Tat, mit "regulären Ausdrücken" meine ich die grundlegenden, die streng in der formalen Sprachtheorie definiert sind. Ich würde gerne wissen, ob es Versuche gab, Rückreferenzen oder andere nicht-reguläre Konstruktionen zu spezifizieren. Ich bin mir der ziemlich beschränkten Formalisierung von grundlegenden r.e. in Nuprl und Coq. Da diese Formalisierungen eher von der Theorie als von der Programmierungspraxis herrührten, berücksichtigten sie nicht nicht reguläre Merkmale. –