论文标题
Kleene代数的FMP的基本证明
An Elementary Proof of the FMP for Kleene Algebra
论文作者
论文摘要
Kleene代数（KA）是证明两个程序等效的有用工具。由于KA的方程理论是可以决定的，因此它与交互式定理掠夺者很好地整合。这就提出了一个问题：我们可以（不）证明使用KA定律哪些方程式？此外，从某种意义上说，哪种KA模型是完整的，它们确切地满足了可证明的方程式？ Kozen（1994）通过用其语言模型来表征KA来回答这些问题。具体而言，在ka中证明的等效性恰恰是那些具有正则表达式的等效性。 Pratt（1980）观察到KA是完整的W.R.T.关系模型，即其可证明的方程是任何关系解释的方程。由于Palka（2005）引起的鲜为人知的结果是，KA的有限模型是完整的，即可证明的等价与所有有限KAS满足的方程式相吻合。词性隔开性，后者是有限的模型属性（FMP）：任何无法证实的方程都是由有限的KA伪造的。这两个结果都可以使用Kozen的定理来争论，但是含义是相互的：鉴于KA是完整的W.R.T.有限（分别关系）模型，Palka的（分别Pratt的）论点表明，它是完整的W.R.T.语言模型。 我们开始研究KA的不同完整模型以及它们之间的连接。这产生了一种新颖的结果，归因于Palka和Pratt的结果，即Ka是完整的W.R.T.有限的关系模型。接下来，我们对Palka的技术进行了代数旋转，该技术产生了有限模型属性的新基本证明，并扩展了Kozen和Pratt定理。与较早的方法相反，此证明不依赖于自动机的最小性或三表象，而是代表转换自动机涉及的正则表达式。
Kleene Algebra (KA) is a useful tool for proving that two programs are equivalent. Because KA's equational theory is decidable, it integrates well with interactive theorem provers. This raises the question: which equations can we (not) prove using the laws of KA? Moreover, which models of KA are complete, in the sense that they satisfy exactly the provable equations? Kozen (1994) answered these questions by characterizing KA in terms of its language model. Concretely, equivalences provable in KA are exactly those that hold for regular expressions. Pratt (1980) observed that KA is complete w.r.t. relational models, i.e., that its provable equations are those that hold for any relational interpretation. A less known result due to Palka (2005) says that finite models are complete for KA, i.e., that provable equivalences coincide with equations satisfied by all finite KAs. Phrased contrapositively, the latter is a finite model property (FMP): any unprovable equation is falsified by a finite KA. Both results can be argued using Kozen's theorem, but the implication is mutual: given that KA is complete w.r.t. finite (resp. relational) models, Palka's (resp. Pratt's) arguments show that it is complete w.r.t. the language model. We embark on a study of the different complete models of KA, and the connections between them. This yields a novel result subsuming those of Palka and Pratt, namely that KA is complete w.r.t. finite relational models. Next, we put an algebraic spin on Palka's techniques, which yield a new elementary proof of the finite model property, and by extension, of Kozen's and Pratt's theorems. In contrast with earlier approaches, this proof relies not on minimality or bisimilarity of automata, but rather on representing the regular expressions involved in terms of transformation automata.
