关于带假设Kleene代数完备性的工具
计算机科学中的逻辑
2024-08-07 v5
摘要
在Kleene代数的文献中,已提出若干变体,它们施加由理论指定的附加结构,例如带测试的Kleene代数(KAT)和近期的带观测的Kleene代数(KAO),或对某些常数作出特定假设,如NetKAT中那样。这些变体中有许多契合带假设的Kleene代数所提供的统一视角,后者带有一个由给定假设集构造的正则语言模型。对于KAT,该模型对应于将表达式解释为守卫串语言的熟悉语义。因此一个相关的问题是:带给定假设集的Kleene代数相对于其正则语言模型是否完备。本文中,我们重访、组合并扩展关于该问题的已有结果,以获得以模块化方式证明完备性的工具。我们通过给出KAT、KAO和NetKAT完备性的新的模块化证明来展示这些工具,并证明了KAT若干新变体的完备性:KAT扩展以全关系常数、KAT扩展以逆运算,以及测试仅形成分配格的KAT版本。
引用
@article{arxiv.2210.13020,
title = {On Tools for Completeness of Kleene Algebra with Hypotheses},
author = {Damien Pous and Jurriaan Rot and Jana Wagemaker},
journal= {arXiv preprint arXiv:2210.13020},
year = {2024}
}