доказательства о регулярных выражениях

См. Perl Regular Expression Matching is NP-Hard

Regex Matching is NP-hard when regexes are allowed to have backreferences.

Сокращение 3-CNF-SAT до Соответствие регулярных выражений Perl

[...] 3-CNF-SAT является NP-полным. Если здесь были эффективными (полиномиальное время) алгоритм вычисления того, действительно ли регулярное выражение соответствует определенной строке, мы мог бы использовать его для быстрого вычисления решения проблемы 3-CNF-SAT, и, как следствие, к ранцу проблема, коммивояжер проблема и т. д. и т. д.

Я не знаю ни одной разработки, которая обрабатывала бы регулярные выражения сами по себе.

Конечные автоматы, однако, актуальны с NFA являются стандартным способом сопоставления этих регулярных выражений, были изучены в NuPRL . Посмотрите: Роберт Л. Констебл, Пол Б. Джексон, Павел Наумов, Хуан Урибе. Конструктивная формализация теории автоматов .

Если вы заинтересованы в приближении к этим формальным языкам через алгебру , в особенности. развивая теорию конечных полугрупп , существует число библиотек алгебры , разработанных в различных программах доказательства теорем, которые вы могли бы подумать об использовании, с один особенно эффективен в ограниченных условиях .

Сертифицированное программирование с зависимыми типами есть раздел о создании проверенного сопоставителя регулярных выражений. Coq Contribs имеет автоматическое добавление , которое может быть полезно. Ян-Оливер Кайзер формализовал эквивалентность между регулярными выражениями, конечными автоматами и характеристикой Майхилла-Нероде в Coq в своей дипломной работе бакалавра .

Морейра, Перейра и де Соуза, О механизации алгебры Клини в Coq дает хорошо проверенную конструкцию производной Антимирова от регулярных выражений в Coq. Довольно легко прочитать CFA из этой конструкции и вычислить пересечение регулярных выражений.

Я не уверен, почему вы отделяете Coq от программирования с зависимой типизацией: Coq по сути является программированием в полиморфном лямбда-исчислении с зависимой типизацией с индуктивным типы (т.е. CIC, исчисление индуктивных конструкций).

Я никогда не слышал о формализации регулярных выражений в языке с зависимой типизацией, и я не слышал о чем-то вроде производной типа Антимирова для регулярных выражений с возвратом с возвратом, но Бекки и Кроули, Расширение конечных автоматов для эффективного сопоставления Perl-совместимых регулярных выражений предоставляет понятие конечных автоматов, которое соответствует Perl-подобным языкам регулярных выражений. Это может быть привлекательно для формализаторов в ближайшем будущем.