无限重写的共归纳处理
A Coinductive Treatment of Infinitary Rewriting
摘要：
我们引入了无穷项重写的共归纳定义。设置是令人惊讶的简单，并在对比通常定义的无穷重写，既不需要序数也不度量收敛。虽然无穷重写的共归纳处理的想法并不新鲜，但所有以前的方法都限于最多Ω的长度减少。本文提出的方法是第一次捕捉到完整的无穷项重写任意序数长度的减少。除了一个优雅的重新表述已知的概念，我们的方法产生了，在一个非常自然的方式，一个新的概念，无限的等式推理。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
