Dafny中正则表达式的良态（共）代数语义
Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny
AI总结：
该研究使用验证感知编程语言Dafny，首次形式化验证了正则表达式的归纳指称语义与共归纳操作语义在逐点互模拟下等价的良态性质，并以共代数语言给出各步解释，为相关理论推广提供蓝本。
摘要：
正则表达式通常通过其指称语义来理解，即通过形式语言——正则语言来定义。这种观点本质上是归纳性的：若两个基元以相同方式构造，则二者等价。另一种方式是通过操作语义来理解正则表达式，即通过确定性有限自动机来定义。这种观点本质上是共归纳性的：若两个基元以相同方式解构，则二者等价。Kleene的著名定理表明这两种观点是等价的：正则语言恰好是确定性有限自动机所接受的形式语言。本文中，我们使用验证感知编程语言Dafny，首次形式化验证了此前仅通过手工证明确立的结论：正则表达式的这两种语义是良态的，即在逐点互模拟意义下二者实际上是同一的。在形式化的每一步中，我们都提出了一种共代数语言下的解释。我们发现Dafny因其归纳和共归纳特性特别适合该任务，希望我们的方法能为未来推广到其他理论提供蓝本。
英文摘要：
Regular expressions are commonly understood in terms of their denotational semantics, that is, through formal languages -- the regular languages. This view is inductive in nature: two primitives are equivalent if they are constructed in the same way. Alternatively, regular expressions can be understood in terms of their operational semantics, that is, through deterministic finite automata. This view is coinductive in nature: two primitives are equivalent if they are deconstructed in the same way. It is implied by Kleene's famous theorem that both views are equivalent: regular languages are precisely the formal languages accepted by deterministic finite automata. In this paper, we use Dafny, a verification-aware programming language, to formally verify, for the first time, what has been previously established only through proofs-by-hand: the two semantics of regular expressions are well-behaved, in the sense that they are in fact one and the same, up to pointwise bisimilarity. At each step of our formalisation, we propose an interpretation in the language of Coalgebra. We found that Dafny is particularly well suited for the task due to its inductive and coinductive features and hope our approach serves as a blueprint for future generalisations to other theories.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
