We establish a formal correspondence between resource calculi an 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 and a structural equivalence. 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 that live in the free multicategorical structures are the same whenever the normal forms of the associated terms are equal. As further application, we obtain syntactic proofs of Mac Lane's coherence theorems for (symmetric) monoidal categories.

翻译：我们建立了资源演算与适当线性多范畴之间的形式对应关系。我们考虑了（对称）可表示多范畴、对称闭多范畴以及自主多范畴的情形。针对所有这些结构，我们证明了对应自由构造中的态射可以通过带类型的资源项（在约简关系和结构等价意义下）来呈现。由于演算的线性性质，我们能够通过组合方法（定义适当的递减度量）证明约简的强归一化性质。由此我们得到一般性的一致性结果：只要相关项的正规形式相等，自由多范畴结构中的态射就相同。作为进一步应用，我们获得了（对称）幺半范畴的Mac Lane一致性定理的语法证明。