×

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].

MSC:

68Q42 Grammars and rewriting systems
68Q70 Algebraic theory of languages and automata
03B40 Combinatory logic and lambda calculus
PDFBibTeX XMLCite
Full Text: Link