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 λ-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 ω(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.

翻译：本文引入了一种“由归纳与余归纳混合构建的语法对象”的通用表示，该表示涵盖了所有标准类型的无穷项以及非良基证明系统中的推导树。随后，我们定义了此类对象的余归纳重写概念，该概念等价于依赖度量收敛和序数索引重写步骤序列的原始无穷重写表示。这为诸如一阶无穷重写、无穷λ演算以及非良基证明中的切消等提供了统一的余归纳表示。接着，我们提出并研究了压缩的余归纳对应物，即无穷重写系统的一种性质：所有任意序数长度的重写序列均可被“压缩”为长度至多为ω的等价序列（这确保了它们可以被有限逼近）。我们在余归纳重写的通用设定中刻画了压缩性质，将证明中可在这一通用层面完成的部分“分解”出来。我们的证明完全采用余归纳方法，避免了通过重写序列的任何迂回路径。最后，我们聚焦于带不动点的乘加性线性逻辑的非良基证明系统 \muMALL\infty，并应用我们的结果证明了在此设定下切消满足压缩性质，这是将切消扩展到若干类似系统的关键引理。