Kleene 代数有限模型性质的初等证明
形式语言与自动机理论
2026-03-11 v4 计算机科学中的逻辑
摘要
Kleene 代数（KA）是证明两个程序等价的实用工具。由于 KA 的等式理论是可判定的，它能很好地与交互式定理证明器集成。这引出一个问题：哪些等式我们可以（无法）用 KA 的定律证明？此外，哪些 KA 模型是完备的，即恰好满足可证等式？Kozen（1994）通过用其语言模型刻画 KA 回答了这些问题。具体而言，KA 中可证的等价恰为那些对正则表达式成立者。Pratt（1980）观察到 KA 关于关系模型是完备的，即其可证等式为任何关系解释下成立者。Palka（2005）一个较少为人知的结果指出，有限模型对 KA 是完备的，即可证等价与所有有限 KA 满足的方程一致。反言之，后者即有限模型性质（FMP）：任何不可证方程被某个有限 KA 证伪。两个结果均可借 Kozen 定理论证，但蕴含是双向的：给定 KA 关于有限（相应为关系）模型完备，Palka（相应为 Pratt）的论证表明其关于语言模型完备。我们着手研究 KA 的不同完备模型及其间联系。这得到涵盖 Palka 与 Pratt 结果的新结果，即 KA 关于有限关系模型是完备的。接着，我们为 Palka 的技术赋予代数视角，得到有限模型性质的新初等证明，并由此扩展至 Kozen 与 Pratt 定理。与早前方法不同，该证明不依赖自动机的最小性或互模拟，而是将所涉正则表达式用变换自动机表示。
引用
@article{arxiv.2212.10931,
title = {An Elementary Proof of the FMP for Kleene Algebra},
author = {Tobias Kappé},
journal= {arXiv preprint arXiv:2212.10931},
year = {2026}
}