Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic

TL;DR

This paper introduces a coinductive framework for infinitary equational logic and rewriting that handles sequences of any ordinal length without relying on ordinals or metrics, facilitating formalization.

Contribution

It provides a uniform, coinductive approach to infinitary rewriting and equational logic, avoiding the complexities of ordinal and metric-based methods.

Findings

Framework captures rewrite sequences of arbitrary ordinal length

No need for ordinals or metric convergence in the framework

Suitable for formalizations in theorem provers

Abstract

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 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.