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

Ответ 1

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

Ответ 2

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

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

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

Ответ 3

См. Perl Regular Expression Matching NP-Hard

Соответствие регулярных выражений NP-hard, когда регулярным выражениям разрешено иметь обратные ссылки.

Уменьшение соответствия 3-CNF-SAT для соответствия регулярному выражению Perl

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

Ответ 4

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

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

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

Ответ 5

Помощник доказательства Isabelle/HOL отправляет ряд формализованных доказательств относительно регулярных выражений (без обратной ссылки): http://afp.sourceforge.net/browser_info/devel/HOL/Regular-Sets/

(здесь является статьей авторов относительно того, что они сделали точно).

Другой подход состоит в том, чтобы охарактеризовать регулярные выражения с помощью Myhill-Nerode Theor: http://www.dcs.kcl.ac.uk/staff/urbanc/Publications/itp-11.pdf