A Coinductive Framework for Infinitary Rewriting and Equational Reasoning (Extended Version)

TL;DR

This paper introduces a coinductive framework for defining and reasoning about infinitary rewriting and equational reasoning, avoiding the need for ordinals or metrics, thus facilitating formalization in theorem provers.

Contribution

It provides a uniform coinductive approach to infinitary rewriting and equational reasoning, capturing sequences of arbitrary ordinal length without complex convergence requirements.

Findings

Defines the relations =^infty and ->^infty using fixed points.

Captures infinite rewrite sequences of arbitrary ordinal length.

Suitable for formalization in theorem provers.

Abstract

We present a coinductive framework for defining infinitary analogues of equational reasoning and rewriting in a uniform way. We define the relation =^infty, notion of infinitary equational reasoning, and ->^infty, the standard notion of infinitary rewriting as follows: =^infty := nu R. ( <-_root + ->_root + lift(R) )^* ->^infty := mu R. nu S. ( ->_root + lift(R) )^* ; lift(S) where lift(R) := { (f(s_1,...,s_n), f(t_1,...,t_n)) | s_1 R t_1,...,s_n R t_n } + id , and where mu is the least fixed point operator and nu is the greatest fixed point operator. 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.