22

有谁知道以下任何例子？

  1. 证明助手（例如Coq ）中关于正则表达式（可能通过反向引用扩展）的证明开发。
  2. 关于正则表达式的依赖类型语言（例如Agda ）的程序。
4

5 回答 5

13

Certified Programming with Dependent Types有一节介绍如何创建经过验证的正则表达式匹配器。Coq Contribs有一个可能有用的自动机贡献。Jan-Oliver Kaiser 在他的学士论文中将正则表达式、有限自动机和 Coq 中的 Myhill-Nerode 表征之间的等价形式化了。

于 2009-08-14T14:48:05.840 回答
10

Moreira、Pereira 和 de Sousa，关于 Coq 中 Kleene 代数的机械化，给出了 Coq 中正则表达式的 Antimirov 导数的良好验证构造。从这个结构中读取 CFA 并计算正则表达式的交集非常容易。

我不确定为什么要将 Coq 与依赖类型编程分开：Coq 本质上是在具有归纳类型的多态依赖类型 lambda 演算中编程（即 CIC，归纳构造的演算）。

我从来没有听说过在依赖类型语言中正则表达式的形式化，也没有听说过类似 Antimirov 的带有回溯的正则表达式的衍生物，但是 Becchi & Crowley, Extending Finite Automata to Efficiently Match Perl-Compatible Regular Expressions提供一个与 Perl 类似的正则表达式语言相匹配的有限状态自动机的概念。在不久的将来，这可能对形式化者有吸引力。

于 2009-12-24T22:26:35.307 回答
7

请参阅Perl 正则表达式匹配是 NP-Hard

当允许正则表达式具有反向引用时，正则表达式匹配是 NP-hard。

减少 3-CNF-SAT 到 Perl 正则表达式匹配

[...] 3-CNF-SAT 是 NP 完全的。如果有一种有效的（多项式时间）算法来计算正则表达式是否匹配某个字符串，我们可以使用它来快速计算 3-CNF-SAT 问题的解决方案，并扩展为背包问题的解决方案，旅行商问题等

于 2009-06-14T07:40:00.783 回答
6

我不知道有任何自己处理正则表达式的开发。

然而，有限自动机是相关的，因为NFA是匹配这些正则表达式的标准方法，已在NuPRL中进行了研究。看看：Robert L. Constable、Paul B. Jackson、Pavel Naumov、Juan Uribe。 建设性地形式化自动机理论。

您是否有兴趣通过代数来处理这些形式语言，尤其是。在开发有限半群理论的过程中，您可以考虑使用各种定理证明中开发的许多代数库，其中一个在有限设置中特别有效。

于 2009-06-26T11:34:29.153 回答
5

证明助手 Isabelle/HOL 提供了许多关于正则表达式的形式化证明（没有反向引用）： http ://afp.sourceforge.net/browser_info/devel/HOL/Regular-Sets/

（这是作者关于他们到底做了什么的论文）。

另一种方法是通过Myhill-Nerode Theorem表征正则表达式： http ://www.dcs.kcl.ac.uk/staff/urbanc/Publications/itp-11.pdf

于 2012-07-26T18:34:28.453 回答