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一致性定理的语法证明。