Compression for Coinductive Infinitary Rewriting: A Generic Approach, with Applications to Cut-Elimination for Non-Wellfounded Proofs

Alexis Saurin; R\'emy Cerda

arxiv: 2510.08420 · v3 · submitted 2025-10-09 · 💻 cs.LO

Compression for Coinductive Infinitary Rewriting: A Generic Approach, with Applications to Cut-Elimination for Non-Wellfounded Proofs

R\'emy Cerda , Alexis Saurin This is my paper

Pith reviewed 2026-05-18 08:14 UTC · model grok-4.3

classification 💻 cs.LO

keywords coinductive rewritingcompressioninfinitary rewritingnon-wellfounded proofscut-eliminationmixed induction-coinductionlinear logicfixed points

0 comments

The pith

A generic coinductive approach establishes compression for infinitary rewriting and cut-elimination in non-wellfounded proofs.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops a unified framework for describing objects that combine inductive and coinductive constructions, such as infinite terms or infinite proof trees. Within this framework, it defines coinductive rewriting and proves it equivalent to the usual notion based on ordinal sequences. The main technical contribution is a characterization of the compression property, which allows reducing any sequence of rewrites to one of length at most the first infinite ordinal, all done in a fully coinductive manner. The authors then apply this to show that cut-elimination in the non-wellfounded proof system for multiplicative-additive linear logic with fixed points satisfies compression.

Core claim

In the generic setting of coinductive rewriting on mixed inductive-coinductive syntactic objects, the compression property holds, meaning every rewriting sequence is equivalent to one of length at most ω. This is established without relying on ordinal-indexed sequences, and it is verified specifically for the cut-elimination relation in μMALL∞.

What carries the argument

The generic presentation of syntactic objects built by mixed induction and coinduction, which supports a coinductive definition of rewriting equivalent to the metric convergence approach.

If this is right

Rewriting sequences of any length can be compressed to equivalent sequences of length at most ω.
This ensures that infinitary rewriting processes can be finitely approximated.
Compression holds for cut-elimination in the μMALL∞ system.
Such compression serves as a key lemma for extending cut-elimination results to similar non-wellfounded systems.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Similar compression results might apply to other non-wellfounded proof systems beyond μMALL∞.
The generic method could simplify proofs in infinitary lambda calculi or other coinductive term rewriting systems.
Future work might explore whether this coinductive compression leads to new decidability results in proof theory.

Load-bearing premise

The generic mixed induction and coinduction presentation accurately captures the structure of standard infinitary terms and non-wellfounded derivation trees.

What would settle it

A specific rewriting sequence in the cut-elimination of μMALL∞ that cannot be equivalently compressed to length at most ω would disprove the claim.

read the original abstract

We introduce a generic presentation of 'syntactic objects built by mixed induction and coinduction' encompassing all standard kinds of infinitary terms, as well as derivation trees in non-wellfounded proof systems. We then define a notion of coinductive rewriting of such objects, which is equivalent to the original presentation of infinitary rewriting relying on metric convergence and ordinal-indexed sequences of rewriting steps. This provides a unified coinductive presentation of e.g. first-order infinitary rewriting, infinitary \lambda-calculi, and cut-elimination in non-wellfounded proofs. We then formulate and study the coinductive counterpart of compression, i.e. the property of an infinitary rewriting system such that all rewriting sequences of any ordinal length can be 'compressed' to equivalent sequences of length at most \omega (which ensures that they can be finitely approximated). We characterise compression in our generic setting for coinductive rewriting, 'factorising' the part of the proof that can be performed at this level of generality. Our proof is fully coinductive, avoiding any detour via rewriting sequences. Finally we focus on the non-wellfounded proof system \muMALL\infty for multiplicative-additive linear logic with fixed points, and we put our results to work in order to prove that compression holds for cut-elimination in this setting, which is a key lemma of several extension of cut-elimination to similar systems.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The generic coinductive framework for compression looks like a clean reusable step for infinitary rewriting and non-wellfounded cut-elimination.

read the letter

The main takeaway is a generic mixed induction-coinduction presentation for infinitary objects that unifies terms and derivation trees, paired with a fully coinductive proof of compression that factors the general case before specializing to muMALL infinity cut-elimination. They define coinductive rewriting and claim it matches the usual metric and ordinal-sequence versions, then characterize compression at that abstract level without routing through sequences. The application shows compression holds for cut-elimination in this logic, which they note is a key lemma for extensions. This factoring approach is the useful part; it lets later work on similar systems plug in without redoing the compression argument each time. The equivalence to prior presentations and the coverage of standard infinitary cases are stated clearly enough in outline to suggest the unification is substantive rather than cosmetic. The coinductive style keeps the argument self-contained and avoids some sequence-based detours that appear in earlier treatments. On the soft spots, the generic presentation needs to be checked against edge cases in infinitary lambda calculi or other systems to confirm it really encompasses everything without extra assumptions. The soundness of the equivalence and the compression characterization rest on the detailed derivations, which the abstract only sketches; any gap there would affect the reusability claim. Nothing in the stated results points to circularity or unfalsifiable steps, but the central claims are load-bearing so they warrant close inspection. This is aimed at people working in infinitary rewriting or non-wellfounded proof theory who want a unified lemma for compression. A reader extending cut-elimination results or looking for coinductive methods would get direct value from the factored proof. It shows clear engagement with the literature and honest use of standard coinductive tools. I would send it to peer review so the generic layer and the muMALL application can be verified in full.

Referee Report

2 major / 2 minor

Summary. The manuscript introduces a generic presentation of syntactic objects constructed via mixed induction and coinduction, encompassing infinitary terms and derivation trees in non-wellfounded proof systems. It defines coinductive rewriting and establishes its equivalence to standard metric-convergence and ordinal-indexed sequence presentations of infinitary rewriting. The authors then characterize the compression property (that any rewriting sequence of ordinal length can be compressed to one of length at most ω) at this generic level via a fully coinductive proof that avoids detours through sequences, and apply the result to establish compression for cut-elimination in the μMALL∞ system.

Significance. If the central claims hold, the work supplies a reusable, factored coinductive proof of compression that can be instantiated across infinitary rewriting systems, including non-wellfounded logics. This directly supports key lemmas needed for cut-elimination extensions in systems such as μMALL∞. The explicit equivalence to metric/ordinal presentations and the avoidance of sequence-based reasoning are technical strengths that could streamline future developments in coinductive proof theory and infinitary term rewriting.

major comments (2)

[Generic compression characterization] The generic characterization of compression (abstract and the section following the equivalence result): the claim that the proof factors cleanly at the generic level and remains fully coinductive is load-bearing for the unification result; the manuscript should supply an explicit statement of the coinductive principle used and confirm that no auxiliary sequence construction is invoked even implicitly when handling arbitrary ordinal lengths.
[Application to μMALL∞] Application to μMALL∞ cut-elimination: while the generic result is invoked to conclude compression, the manuscript must verify that the specific cut and contraction rules of μMALL∞ satisfy the side conditions of the generic compression theorem without additional ad-hoc arguments; otherwise the transfer is not immediate.

minor comments (2)

[Abstract] The abstract states 'several extension of cut-elimination'; this should be corrected to 'several extensions'.
[Generic presentation] Notation for mixed inductive-coinductive objects could be introduced with a small illustrative example (e.g., an infinitary term or a simple derivation tree) before the general definition to improve readability.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the positive evaluation and the insightful comments that help clarify the presentation of our results. We address each major comment below and indicate the revisions we will make to the manuscript.

read point-by-point responses

Referee: [Generic compression characterization] The generic characterization of compression (abstract and the section following the equivalence result): the claim that the proof factors cleanly at the generic level and remains fully coinductive is load-bearing for the unification result; the manuscript should supply an explicit statement of the coinductive principle used and confirm that no auxiliary sequence construction is invoked even implicitly when handling arbitrary ordinal lengths.

Authors: We agree that an explicit statement of the coinductive principle will improve clarity. In the revised manuscript we will insert a new paragraph immediately after the statement of the generic compression theorem. This paragraph will name the principle as the standard coinduction rule for the mixed inductive-coinductive datatypes introduced in Section 3, and will explicitly note that the proof proceeds by coinductive unfolding of the generic rewriting relation. No auxiliary ordinal-indexed sequences or metric-limit constructions are used at any stage; the handling of arbitrary ordinal lengths is encoded directly in the coinductive definition of the relation itself. revision: yes
Referee: [Application to μMALL∞] Application to μMALL∞ cut-elimination: while the generic result is invoked to conclude compression, the manuscript must verify that the specific cut and contraction rules of μMALL∞ satisfy the side conditions of the generic compression theorem without additional ad-hoc arguments; otherwise the transfer is not immediate.

Authors: We appreciate the request for explicit verification. The cut and contraction rules of μMALL∞ are formulated precisely so that they meet the local-finiteness and coinductive-compatibility side conditions of the generic theorem (as these conditions are inherited from the standard definition of the μMALL∞ sequent calculus). In the revised version we will add a short verification subsection right after the invocation of the generic result, listing each side condition and confirming its satisfaction by direct reference to the rule definitions, without introducing any new ad-hoc reasoning. revision: yes

Circularity Check

0 steps flagged

No significant circularity: generic coinductive framework yields independent characterization of compression

full rationale

The paper first defines a generic mixed inductive-coinductive presentation of syntactic objects (encompassing infinitary terms and non-wellfounded derivations) and proves its equivalence to the standard metric/ordinal presentation of infinitary rewriting. It then formulates the coinductive counterpart of compression and provides a fully coinductive proof of the characterization at this generic level, explicitly avoiding detours through sequences. The final specialization to cut-elimination in μMALL∞ applies the generic result directly. No load-bearing step reduces by construction to a fitted parameter, self-citation chain, or renamed input; the equivalence and generic characterization steps supply independent content grounded in standard coinductive principles rather than tautological reductions.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper relies on standard coinductive principles for defining syntactic objects and rewriting; no free parameters, new entities, or ad-hoc axioms are mentioned in the abstract.

axioms (1)

domain assumption Coinductive definitions and principles apply to objects built by mixed induction and coinduction
Invoked when defining the generic syntactic objects and coinductive rewriting in the abstract.

pith-pipeline@v0.9.0 · 5809 in / 1298 out tokens · 33309 ms · 2026-05-18T08:14:43.258832+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/ArithmeticFromLogic.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

We characterise compression in our generic setting for coinductive rewriting, 'factorising' the part of the proof that can be performed at this level of generality. ... Then −→ has the Compression property iff the property Q holds.
IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

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.

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.