2013/06/26 by Joerg Endrullis, Helle Hvid Hansen, Endrullis, Joerg +7 · 1 citation
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #cs.LO
paper · pdf · doi:10.48550/arxiv.1306.6224
arxiv created 2014/04/10 · arxiv updated 2014/04/11
We introduce a coinductive definition of infinitary term rewriting. The setup is surprisingly simple, and has in contrast to the usual definitions of infinitary rewriting, neither need for ordinals nor for metric convergence. While the idea of a coinductive treatment of infinitary rewriting is not new, all previous approaches were limited to reductions of length at most omega. The approach presented in this paper is the first to capture the full infinitary term rewriting with reductions of arbitrary ordinal length. Apart from an elegant reformulation of known concepts, our approach gives rise, in a very natural way, to a novel notion of infinitary equational reasoning.