Coq中Kleene代数的判定
Deciding Kleene Algebras in Coq
摘要：
在Coq证明助手中给出了判定Kleene代数方程理论的自反策略。这种策略依赖于有效的有限自动机算法的仔细实现，以便它即时解决休闲方程并适当地扩展到更大的表达式。证明了决策过程的正确性和完备性：正确性是建立在w.r.t.通过形式化Kozen的初始性定理的任何模型;当给定的方程不成立时返回一个反例。正确性证明是具有挑战性的：它既涉及对底层自动机算法的精确分析，又涉及大量的代数推理。特别是，我们必须正式的理论矩阵的Kleene代数。我们建立在最近增加的第一次typeclasses在Coq，以有效地工作与所涉及的代数结构。
英文摘要：
We present a reflexive tactic for deciding the equational theory of Kleene algebras in the Coq proof assistant. This tactic relies on a careful implementation of efficient finite automata algorithms, so that it solves casual equations instantaneously and properly scales to larger expressions. The decision procedure is proved correct and complete: correctness is established w.r.t. any model by formalising Kozen's initiality theorem; a counter-example is returned when the given equation does not hold. The correctness proof is challenging: it involves both a precise analysis of the underlying automata algorithms and a lot of algebraic reasoning. In particular, we have to formalise the theory of matrices over a Kleene algebra. We build on the recent addition of firstorder typeclasses in Coq in order to work efficiently with the involved algebraic structures.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
