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

Question

Кто-нибудь знает примеры следующего?

1. Доказательства о регулярных выражениях (возможно, расширены с обратными ссылками ) в помощниках по проверке (таких как Coq ).
2. Программы на языках с типизированной зависимостью (например, Agda ) с регулярными выражениями.

Answer 1

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

Answer 2

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

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

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

Answer 3

См. Соответствие регулярному выражению Perl NP-Hard

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

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

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

Answer 4

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

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

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

Answer 5

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

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

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