A Coinductive Framework for Infinitary Rewriting and Equational Reasoning
Jörg Endrullis, Helle Hvid Hansen, Dimitri Hendriks, Andrew T. Polonsky, Alexandra Soares da Silva · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2015
We present a coinductive framework for defining infinitary analogues of equational reasoning and rewriting in a uniform way. 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.