共析性无限性重写的压缩：一种通用方法及其在非良根证明中的消除剪枝应用

我们提出了'由混合归纳与共析构成的语法对象'的通用表述，涵盖所有标准的无限项，以及非良根证明系统中的派生树。随后我们定义了此类对象的共析性重写概念，其等效于依赖度量收敛和序数索引重写步骤序列的原始无限性重写表述。这提供了对例如首次阶数无限性重写、无限$\lambda$演算，以及非良根证明中消除剪枝的统一共析表述。我们随后提出并研究了共析压缩的对手，即无限性重写系统的性质，使得任意长度序数重写序列都可以'压缩'为最多$\omega$长度的等效序列（这确保了它们可以有限近似）。我们在通用共析重写设置下对压缩进行特征化，'分解'可在此层次普遍性完成的证明部分。我们的证明完全为共析，避免通过重写序列的中间环节。最后我们聚焦于包含固定点的乘法-加法线性逻辑的非良根证明系统$\mu$MALL$\infty$，并将我们的成果应用于证明该设置下消除剪枝的压缩成立，这是多个类似系统消除剪枝扩展的关键引理。