¿Alguien conoce algún ejemplo de lo siguiente?pruebas sobre expresiones regulares
Ver Perl Regular Expression Matching is NP-Hard
expresión regular coincidente es NP-duro cuando se les permite expresiones regulares para tener referencias hacia atrás.
Reduction of 3-CNF-SAT to Perl Regular Expression Matching
[...] 3-CNF-SAT es NP-completo. Si hay eran una eficiente (tiempo polinomio) algoritmo para calcular si o no una expresión regular coincide con una determinada cadena, que podría utilizar para calcular rápidamente soluciones al problema 3-CNF-SAT, y, por extensión, , con el problema de la mochila , el viajante de comercio problema, etc, etc
Incluso más que eso: Alfred Aho ha demostrado que la coincidencia de patrones de expresión regular con referencias posteriores es NP-completa hace bastante tiempo por reducción del problema de cobertura de vértices. Ver el Teorema 6.2 de [A. V. Aho. Algoritmos para encontrar patrones en cadenas. En Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, volumen A: Algorithms and Complexity, páginas 255-300. The MIT Press, 1990]. –
no sé de cualquier desarrollo que se considera que las expresiones regulares por sí mismos.
Los autómatas finitos, sin embargo, relevantes desde NFAs son la forma estándar de coincidir con esas expresiones regulares, se han estudiado en NuPRL. Eche un vistazo a: Robert L. Constable, Paul B. Jackson, Pavel Naumov, Juan Uribe. Constructively Formalizing Automata Theory.
Si le interesa acercarse a los idiomas formales a través de algebra, esp. desarrollando finite semigroup theory, hay un number de algebra libraries desarrollado en varios demostradores de teoremas que podría pensar en usar, con one particularly efficient in a finite setting.
Certified Programming with Dependent Types tiene una sección sobre la creación de un verificador de expresiones regulares verificado. Coq Contribs tiene un automata contribution que puede ser útil. Jan-Oliver Kaiser formalizó la equivalencia entre expresiones regulares, autómatas finitos y la caracterización de Myhill-Nerode en Coq para su bachelors thesis.
Derecha, también he notado este párrafo en CPDT hace unas semanas. Golpea la pelota. Según la contribución del autómata, ciertamente lo es. Sin embargo, usa axiomas. Por ejemplo, 4 axiomas en la prueba de que los lenguajes regulares están definidos por los NFA (módulo RatReg). Una prueba sin axiomas también es posible (pero no incluida en las contribuciones de Coq). –
Moreira, Pereira & de Sousa, On the Mechanisation of Kleene Algebra in Coq da una buena construcción verificada de la derivada Antimirov de regexps en Coq. Es bastante fácil leer un CFA de esta construcción y calcular la intersección de las expresiones regulares.
No estoy seguro de por qué separa Coq de la programación dependiente: Coq esencialmente está programando en un cálculo lambda de tipo dependiente polimórfica con tipos inductivos (es decir, CIC, el cálculo de construcciones inductivas).
nunca he oído hablar de una formalización de las expresiones regulares en un idioma escrito de forma dependiente, ni he oído hablar de algo como un derivado Antimirov similar a las expresiones regulares con marcha atrás, pero Becchi & Crowley, Extending Finite Automata to Efficiently Match Perl-Compatible Regular Expressions proporcionar una idea de finito un autómata de estado que coincide con un lenguaje de expresiones regulares tipo Perl. Eso podría ser atractivo para los formalisers en el futuro cercano.
El asistente prueba Isabelle/HOL barcos una serie de pruebas formales en relación con las expresiones regulares (sin referencia hacia atrás): http://afp.sourceforge.net/browser_info/devel/HOL/Regular-Sets/
(here es un documento elaborado por los autores con respecto a lo que hicieron exactamente).
Otro enfoque es la caracterización de las expresiones regulares a través de Myhill-Nerode Theorem: http://www.dcs.kcl.ac.uk/staff/urbanc/Publications/itp-11.pdf
Según "El dominio de expresiones regulares" (un libro que recomiendo, ver http://regex.info/) expresiones regulares son bastante ocasional en hecho debido a sus habilidades mejoradas, por lo que la teoría matemática solo está disponible para tipos de expresiones regulares simples/básicas. ¿Esto tiene implicaciones para usarlos en la asistencia de prueba? –
Sí, lo hace: hace las pruebas más complicadas :) De hecho, por "expresiones regulares" me refiero a las básicas que están estrictamente definidas en la teoría del lenguaje formal. Me gustaría saber si hubo intentos de especificar referencias retrospectivas u otras construcciones no regulares. Soy consciente de formalisations bastante limitadas de r.e básico. en Nuprl y Coq. Dado que estas formalizaciones se derivaron de la teoría, en lugar de la práctica de programación, no explicaron las características no regulares. –