Compression for Coinductive Infinitary Rewriting: A Generic Approach, with Applications to Cut-Elimination for Non-Wellfounded Proofs
Rémy Cerda, Alexis Saurin
TL;DR
The paper addresses Compression in infinitary rewriting for non-wellfounded derivations and introduces a generic coinductive framework that unifies topological and coinductive perspectives. It presents a universal Compression lemma with a system-agnostic characterisation that isolates the essential conditions for compression, then instantiates it for left-linear first-order rewriting and for abc-infinitary λ-calculus. The framework is subsequently applied to μMALL∞, demonstrating compression of cut-elimination sequences and providing a coinductive approach to non-wellfounded proofs in logics with fixed points. Overall, the work offers a modular foundation for compression across a broad range of infinitary rewriting systems and supports coinductive cut-elimination procedures in non-wellfounded proof theory.
Abstract
Infinitary rewriting, i.e. rewriting featuring possibly infinite terms and sequences of reduction, is a convenient framework for describing the dynamics of non-terminating but productive rewriting systems. In its original definition based on metric convergence of ordinal-indexed sequences of rewriting steps, a highly desirable property of an infinitary rewriting system is Compression, i.e. the fact that rewriting sequences of arbitrary ordinal length can always be 'compressed' to equivalent sequences of length at most ω. Since then, the standard examples of infinitary rewriting systems have been given another equivalent presentation based on coinduction. In this work, we extend this presentation to the rewriting of arbitrary non-wellfounded derivations and we investigate compression in this setting. We design a generic proof of compression, relying on a characterisation factorising most of the proof and identifying the key property a compressible infinitary rewriting system should enjoy. As running examples, we discuss first-order rewriting and infinitary λ-calculi. For the latter, compression can in particular be seen as a justification of its coinductive presentation in the literature. As a more advanced example, we also address compression of cut-elimination sequences in the non-wellfounded proof system μMALL{\infty} for multiplicative-additive linear logics with fixed points, which is a key lemma of several cut-elimination results for similar proof systems.