We establish a formal correspondence between resource calculi and appropriate linear multicategories. We consider the cases of (symmetric) representable, symmetric closed and autonomous multicategories. For all these structures, we prove that morphisms of the corresponding free constructions can be presented by means of typed resource terms, up to a reduction relation. Thanks to the linearity of the calculi, we can prove strong normalization of the reduction by combinatorial methods, defining appropriate decreasing measures. From this, we achieve a general coherence result: morphisms who live in the free multicategorical structures are the same whenever the normal forms of the associated class of terms are equal. As an application, we obtain syntactic proofs of Mac Lane's coherence theorems for (symmetric) monoidal categories.
翻译:我们建立了资源演算与相应线性多范畴之间的形式对应关系。我们考虑了(对称)可表示多范畴、对称闭多范畴和自洽多范畴的情形。针对所有这些结构,我们证明了相应自由构造中的态射可以通过带类型的资源项,在归约关系下呈现。由于演算的线性性质,我们能够通过组合方法定义适当的递减度量,从而证明归约的强规范化。由此我们得到一个一般的相干性结果:只要关联项类的范式相等,自由多范畴结构中的态射就相同。作为应用,我们获得了(对称)幺半范畴的Mac Lane相干定理的语法证明。