Technical Report No. 146 - Abstract

Georg Struth
Church-Rosser Proofs in Kleene Algebra and Allegories

We prove Church-Rosser statements in Kleene algebra in the spirit of the point-free style of functional programming. Proofs of Church-Rosser theorems are simple and general, using only algebraic properties of the regular operations. They are fixed point-based, induction-free and often amenable to automata, hence suited to mechanization. In the strip lemma of the $\lambda$-calculus, the term and algebra part are cleanly separated. Relating Kleene algebras with allegories explains Church-Rosser diagrams categorially. Using allegoric techniques, we also prove algebraic variants of Newman's lemma and Church-Rosser statements modulo an equivalence relation, in which the well-foundedness assumptions are derived. Here, point-wise techniques are introduced via tabulations, but still the construction avoids the invention of complex induction orderings and measures. Our results can be read as a case study for the possibilities and limitations of point-free allegorial formal methods.