线性多类别结构的归一化协调性
摘要：资源计算与适当的线性多范畴之间建立了一种形式上的对应关系。我们考虑了（对称的）可表示、对称闭合和自治多范畴的情况。对于所有这些结构，我们证明了相应的自由构造的态射可以通过类型资源术语表示，直到约化关系和结构等价。由于计算的线性性质，我们可以通过组合方法定义适当的递减度量来证明约化的强归一化。由此，我们实现了一个普遍的一致性结果：只要相关术语的正规形式相等，就在自由多范畴结构中存在的态射是相同的。作为进一步的应用，我们为（对称的）幺半范畴获得了Mac Lane的一致性定理的语法证明。
作者：Federico Olimpieri
论文ID：2302.05755
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-28