We present a coinductive framework for defining and reasoning about the infinitary analogues of equational logic and term rewriting in a uniform, coinductive way.

The framework lends itself to an elegant and concise definition of the infinitary rewrite relation \( \to^\infty \) in terms of the single step relation \( \to \): \[ {\to^\infty} \,=\, \mu R. \nu S. ( \to \cup \mathrel{\overline{R}} )^* \mathrel{;} \overline{S} \] Here \( \mu \) and \( \nu \) are the least and greatest fixed-point operators, respectively, and \[ \overline{R} \,=\, \{\, (\, f(s_1,\ldots,s_n),\, \,f(t_1,\ldots,t_n) \,) \mid f \in \Sigma,\, s_1\! \mathrel{R} t_1,\ldots,s_n\! \mathrel{R} t_n \,\} \cup \text{Id} \] The setup captures rewrite sequences of arbitrary ordinal length, but it has neither the need for ordinals nor for metric convergence. This makes the framework suitable for formalizations in theorem provers. To wit, we provide the first formalization of the compression lemma in Coq.

This paper is an extended version of A Coinductive Framework for Infinitary Rewriting and Equational Reasoning (RTA 2015). We build on ideas in Infinitary Rewriting Coinductively (TYPES 2012) giving a coinductive perspective on infinitary lambda calculus. We extend these ideas to rewrite sequences beyond length omega by mixing induction and coinduction (least and greatest fixed-points).

} }