Regular Language Representations in the Constructive Type Theory of Coq
Regular Language Representations in the Constructive Type Theory of Coq
复制标题
DOI：
10.1007/s10817-018-9460-x
复制
发表时间：
2018-06-01
期刊：
影响因子：
--
通讯作者：
Smolka, Gert
中科院分区：
文献类型：
--
作者：
Doczkal, Christian;Smolka, Gert
我们探讨了Coq的结构类型理论中的正则语言表征理论。我们涵盖了各种形式的自动机（确定性、非确定性、单向、双向）、正则表达式和逻辑WS 1 S。我们给出所有表示之间的翻译，显示可判定性结果，并提供各种封闭属性的操作。我们的研究结果包括一个建设性的可判定性证明的逻辑WS 1 S，建设性的改进的Myhill-Nerode表征的规律性，和翻译从双向自动机到单向自动机与验证的上限的大小增加。所有的结果都用伴随的约3000条线的Coq开发进行了验证。
We explore the theory of regular language representations in the constructive type theory of Coq. We cover various forms of automata (deterministic, nondeterministic, one-way, two-way), regular expressions, and the logic WS1S. We give translations between all representations, show decidability results, and provide operations for various closure properties. Our results include a constructive decidability proof for the logic WS1S, a constructive refinement of the Myhill-Nerode characterization of regularity, and translations from two-way automata to one-way automata with verified upper bounds for the increase in size. All results are verified with an accompanying Coq development of about 3000 lines.