关于Bisimilarity下Milner的正则表达式证明系统的共归重新表述
摘要：在这篇论文中，Milner（1984）将正则表达式的操作语义定义为有限状态过程。为了在这个过程语义下公理化正则表达式的bisimilarity，他采用了Salomaa的证明系统，该系统对于语言语义下的正则表达式相等是完备的。除了大多数等式公理之外，Milner的系统Mil还继承了Salomaa系统中用于解决单个不动点方程的非代数规则。识别出了过程语义的独特性质，使得Salomaa的证明策略不适用，Milner将系统Mil的完备性作为一个未解决的问题。 为了解决这个问题，我们采用了一种证明论方法，刻画了不动点规则在系统Mil的纯等式部分Mil$^-$中添加的推导能力。我们通过一个共归规则来实现这一点，该规则允许由满足分层循环存在和消除属性（LLEE）的空步骤的有限过程图组成的循环推导，并且有两个Mil$^-$可证明的解。在Mil中以这个规则来替代固定点规则的基础上，我们定义了共归重述cMil作为Mil$^-$的一个扩展。为了展示cMil和Mil在定理上是等价的，我们开发了从Mil到cMil的有效证明转换，以及从cMil到Mil的转换。由于cMil位于Milner系统Mil的双模拟和证明之间，它可能成为证明Mil完备性的概念起点。 本文扩展了我们在CALCO 2022会议文集中的贡献。在这里，我们通过将证明转换框架化为可导出的和可接受的规则的消除，将共归证明与过程图解的共代数形式相联系。
作者：Clemens Grabmayer
论文ID：2203.09501
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-29