We present a coinductive framework for defining infinitary analogues of equational reasoning and rewriting in a uniform way. We define the relation 1=, a hitherto unknown notion of infinitary equational reasoning, and !1, the standard notion of infinitary rewriting as follows: 1= := R. (=E [ R) !1 := μR. S. (!R [ R)  S where μ and  are the least and greatest fixed-point operators, respectively, and where R := { hf(s1, . . . , sn), f(t1, . . . , tn)i | f 2 , s1 R t1, . . . , sn R tn } [ 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 especially suitable for formalizations in theorem provers.
Additional Metadata
THEME Software (theme 1)
Publisher Schloss Dagstuhl - Leibniz Center of Informatics
Persistent URL dx.doi.org/10.4230
Series Leibniz International Proceedings in Informatics
Conference International Conference on Rewriting Techniques and Applications
Citation
Endrullis, J, Hansen, H.H, Hendriks, D, Polonsky, A, & Silva, A.M. (2015). A Coinductive Treatment of Infinitary Term Rewriting and Equational Reasoning. In Proceedings of International Conference on Rewriting Techniques and Applications 2015 (RTA) (pp. 143–159). Schloss Dagstuhl - Leibniz Center of Informatics. doi:10.4230