eau*_*bin 12
带有依赖类型的认证编程有一个关于创建经过验证的正则表达式匹配器的部分.Coq Contribs有一个可能有用的自动机贡献.Jan-Oliver Kaiser将Coq中正则表达式,有限自动机和Myhill-Nerode特征描述等同于他的单身汉论文.
Moreira,Pereira&de Sousa,关于Coq中Kleene代数的机械化,给出了Coq中 retimxps的Antimirov导数的一个很好的验证结构.从这种结构中读取CFA并计算正则表达式的交集非常容易.
我不确定为什么要将Coq与依赖类型编程分开:Coq本质上是在具有归纳类型的多态依赖类型lambda演算中编程(即CIC,归纳结构的演算).
我从来没有听说过依赖类型语言的正则表达式的形式化,我也没有听说过类似于带有回溯的正则表达式的Antimirov类导数,但是Becchi和Crowley,扩展有限自动机以有效匹配Perl兼容的正则表达式提供有限状态自动机的概念,匹配类似Perl的正则表达式语言.这可能在不久的将来对正规商有吸引力.
当正则表达式允许反向引用时,正则表达式匹配是NP难的.
[...] 3-CNF-SAT是NP完整的.如果有一个有效的(多项式时间)算法来计算正则表达式是否匹配某个字符串,我们可以用它来快速计算3-CNF-SAT问题的解决方案,并且,通过扩展,可以解决背包问题,旅行商问题等等
我不知道有什么开发可以自己处理正则表达式。
但是，由于NFA是匹配那些正则表达式的标准方法，因此有限自动机非常重要，已经在NuPRL中进行了研究。看看：罗伯特·L·康斯特勃，保罗·杰克逊，帕维尔·纳乌莫夫，胡安·乌里韦。 建构形式化的自动机理论。
如果您有兴趣通过代数学习这些正式语言，尤其是。开发有限半群理论，也有若干的代数库中各种定理证明开发了你能想到使用，有一个在有限的设置特别有效。
证明助手 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
| 归档时间： |
|
| 查看次数： |
2700 次 |
| 最近记录： |