一般文法的闭包性质 -- 形式验证
摘要：用Lean 3证明助手形式化了一般（即0型）文法。我们定义了重写规则和由文法推导出的词汇的基本概念，并使用文法来展示了类型0语言在四种操作下的封闭性：并集、反转、连接和Kleene星运算。现有文献大多集中在图灵机论证上，这可能更难以形式化。对于Kleene星运算，我们无法按照文献进行，因此提出了我们自己基于文法的构造方法。
作者：Martin Dvorak and Jasmin Blanchette
论文ID：2302.06420
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2023-05-24