Grabmayer and Fokkink recently presented a finite and complete axiomatization for 1-free process terms over the binary Kleene star under bismilarity equivalence (proceedings of LICS 2020, preprint available). A different and considerably simpler proof is detailed in this paper. This result, albeit still somewhat technical, only relies on induction and normal forms and is therefore also much closer to a potential rewriting algorithm. In addition, a complete verification in the Coq proof assistant of all results in this work is provided, but correctness does not depend upon any computer-assisted methodology.
翻译：Grabmayer和Fokkink最近介绍了一种有限和完整的对二元Kleene恒星在两种等同之下(LICS 2020的进度,可提供预印本)的无1个进程条件的完整分解(有限和完整),本文详细介绍了一种不同和相当简单的证据,这一结果尽管仍然是技术性的,但仅依赖于上岗和正常形式,因此也更接近于可能的重写算法。此外,在Coq验证助理中,对这项工作的所有结果进行了全面核实,但正确性并不取决于任何计算机辅助方法。
相关内容
微信扫码咨询专知VIP会员