关于正则表达式的证明
Does anyone know any examples of the following?
- Proof developments about regular expressions (possibly extended with backreferences) in proof assistants (such as Coq).
- Programs in dependently-typed languages (such as Agda) about regular expressions.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（5）
依赖类型认证编程有一个关于创建经过验证的正则表达式匹配器的部分。 Coq Contribs 有一个 自动机贡献 可能有用。 Jan-Oliver Kaiser 在 Coq 中形式化了正则表达式、有限自动机和 Myhill-Nerode 表征之间的等价性，其 学士论文。
Certified Programming with Dependent Types has a section on creating a verified regular expression matcher. Coq Contribs has an automata contribution that might be useful. Jan-Oliver Kaiser formalized the equivalence between regular expressions, finite automata and the Myhill-Nerode characterization in Coq for his bachelors thesis.
莫雷拉、佩雷拉和 de Sousa，On the Mechanization of Kleene Algebra in Coq 给出了一个经过验证的很好的构造Coq 中正则表达式的 Antimirov 衍生物。 从这个结构中读取 CFA 并计算正则表达式的交集非常容易。
我不确定为什么将 Coq 与依赖类型编程分开：Coq 本质上是在具有归纳类型的多态依赖类型 lambda 演算（即 CIC，归纳结构演算）中进行编程。
我从未听说过依赖类型语言中的正则表达式的形式化，也没有听说过带有回溯功能的类似 Antimirov 的正则表达式导数，但 Becchi & Crowley，扩展有限自动机以有效匹配与 Perl 兼容的正则表达式 提供与类似 Perl 的正则表达式语言相匹配的有限状态自动机的概念。 在不久的将来，这可能会对形式化者有吸引力。
Moreira, Pereira & de Sousa, On the Mechanisation of Kleene Algebra in Coq gives a nice verified construction of the Antimirov derivative of regexps in Coq. It's pretty easy to read off a CFA from this construction, and to compute the intersection of regexps.
I'm not sure why you separate Coq from dependently typed programming: Coq essentially is programming in a polymorphic dependently typed lambda calculus with inductive types (i.e., CIC, the calculus of inductive constructions).
I've never heard of a formalisation of regexps in a dependently typed language, nor have I heard of something such as an Antimirov-like derivative for regexps with backtracking, but Becchi & Crowley, Extending Finite Automata to Efficiently Match Perl-Compatible Regular Expressions provide a notion of finite-state automata that matches a Perl-like regexp languages. That might attractive to formalisers in the near future.
请参阅 Perl 正则表达式匹配是 NP 难的
See Perl Regular Expression Matching is NP-Hard
我不知道有任何开发可以单独处理正则表达式。
然而，有限自动机相关，因为 NFAs 是匹配这些正则表达式的标准方法，已经被研究过在NuPRL。 看看：罗伯特·L·康斯特布尔，保罗·B·杰克逊，帕维尔·瑙莫夫，胡安·乌里韦。 建设性地形式化自动机理论。
如果您有兴趣通过代数来接触这些形式语言，尤其是代数。 发展有限半群理论，有一个 “noreferrer”>代数库在您可以考虑使用的各种定理证明器中开发，在有限环境中特别有效。
I don't know of any development that treats regular expressions by themselves.
Finite automata, however, relevant since NFAs are the standard way to match those regular expressions, have been studied in NuPRL. Have a look at : Robert L. Constable, Paul B. Jackson, Pavel Naumov, Juan Uribe. Constructively Formalizing Automata Theory.
Should you be interested in approaching those formal languages through algebra, esp. developing finite semigroup theory, there are a number of algebra libraries developed in various theorem provers that you could think of using, with one particularly efficient in a finite setting.
证明助理 Isabelle/HOL 提供了许多有关正则表达式的形式化证明（无反向引用）：
http://afp.sourceforge.net/browser_info/devel/HOL/Regular- Sets/
（这里是一篇论文作者关于他们到底做了什么）。
另一种方法是通过 Myhill-Nerode 定理 来表征正则表达式：
http://www.dcs.kcl.ac.uk /staff/urbanc/Publications/itp-11.pdf
The proof assistant Isabelle/HOL ships a number of formalized proofs regarding regular expressions (without back reference):
http://afp.sourceforge.net/browser_info/devel/HOL/Regular-Sets/
(here is a paper by the authors regarding what they did exactly).
Another approach is to characterize regular expressions via Myhill-Nerode Theorem:
http://www.dcs.kcl.ac.uk/staff/urbanc/Publications/itp-11.pdf