Struth, Georg Calculating Church-Rosser proofs in Kleene algebra. (English) Zbl 1027.68071 de Swart, Harrie C. M. (ed.), Relational methods in computer science. 6th international conference, RelMiCS 2001 and 1st workshop of COST Action 274 TARSKI, Oisterwijk, The Netherlands, October 16-21, 2001. Revised papers. Berlin: Springer. Lect. Notes Comput. Sci. 2561, 276-290 (2002). Summary: We present simple calculational proofs of Church-Rosser theorems for equational theories, quasiorderings and non-symmetric transitive relations in Kleene algebra. We also calculate the abstract part of two standard proofs of Church-Rosser theorems in the \(\lambda\)-calculus and further central statements of rewriting. Since proofs avoid deduction, in particular induction, and large parts are amenable to automata, the approach is suited for mechanization. Since proofs algebraically reconstruct precisely the usual diagrams, they are also very natural for a human. In all considerations, Kleene algebra is an excellent means of abstraction.For the entire collection see [Zbl 1014.00018]. Cited in 1 ReviewCited in 3 Documents MSC: 68Q42 Grammars and rewriting systems 68Q70 Algebraic theory of languages and automata 03B40 Combinatory logic and lambda calculus Keywords:Kleene algebra; rewriting; \(\lambda\)-calculus; Church-Rosser theorem; formal mathematics PDFBibTeX XMLCite \textit{G. Struth}, Lect. Notes Comput. Sci. 2561, 276--290 (2002; Zbl 1027.68071) Full Text: Link