regexp - pruebas sobre expresiones regulares
probar expresiones regulares (5)
El asistente de pruebas Isabelle / HOL envía una serie de pruebas formalizadas con respecto a expresiones regulares (sin referencia): http://afp.sourceforge.net/browser_info/devel/HOL/Regular-Sets/
( here hay un artículo de los autores sobre lo que hicieron exactamente).
Otro enfoque es caracterizar expresiones regulares a través del teorema de Myhill-Nerode : http://www.dcs.kcl.ac.uk/staff/urbanc/Publications/itp-11.pdf
¿Alguien sabe algún ejemplo de lo siguiente?
- backreferences de la prueba sobre expresiones regulares (posiblemente ampliadas con backreferences ) en asistentes de prueba (como Coq ).
- Programas en lenguajes de tipo dependiente (como Agda ) sobre expresiones regulares.
Moreira, Pereira & de Sousa, Sobre la Mecanización del Álgebra de Kleene en Coq ofrece una buena construcción verificada del derivado Antimirov de las expresiones regulares en Coq. Es bastante fácil leer un CFA de esta construcción y calcular la intersección de expresiones regulares.
No estoy seguro de por qué separa Coq de la programación tipificada de manera dependiente: Coq esencialmente está programando en un cálculo lambda tipificado de forma polimórfica con tipos inductivos (es decir, CIC, el cálculo de construcciones inductivas).
Nunca he oído hablar de una formalización de expresiones regulares en un lenguaje tipificado de manera dependiente, ni he oído hablar de algo como un derivado similar a Antimirov para expresiones regulares con retroceso, pero Becchi y Crowley extienden autómatas finitos para igualar eficientemente las expresiones regulares compatibles con Perl proporcione una noción de autómata de estado finito que coincida con los lenguajes de expresión regular de tipo Perl. Eso podría ser atractivo para los formalizadores en un futuro próximo.
No conozco ningún desarrollo que trate las expresiones regulares por sí mismas.
Los autómatas finitos, sin embargo, relevantes ya que las NFAs son la forma estándar de emparejar esas expresiones regulares, se han estudiado en NuPRL . Eche un vistazo a: Robert L. Constable, Paul B. Jackson, Pavel Naumov, Juan Uribe. Formalizando formalmente la teoría de autómatas .
Si está interesado en acercarse a esos lenguajes formales a través del algebra , esp. Al desarrollar la teoría de semigrupos finitos , hay number bibliotecas de álgebra desarrolladas en varios probadores de teoremas que se podrían pensar en usar, con una especialmente eficiente en un entorno finito .
Ver Perl Regular Expression Matching es NP-Hard
La coincidencia de expresiones regulares es NP-difícil cuando se permite que las expresiones regulares tengan referencias inversas.
Reducción de 3-CNF-SAT a Perl Matching de expresión regular
[...] 3-CNF-SAT es NP-completo. Si existiera un algoritmo eficiente (tiempo polinomial) para calcular si una expresión regular coincidió o no con una determinada cadena, podríamos usarla para calcular rápidamente soluciones al problema 3-CNF-SAT y, por extensión, al problema de mochila. El problema del vendedor ambulante, etc. etc.
La programación certificada con tipos dependientes tiene una sección sobre cómo crear un comparador de expresiones regulares verificado. Coq Contribs tiene una contribución de autómatas que podría 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 tesis de licenciatura .