Categorical Reduction

我们将直觉线性逻辑的范畴语义解释为一个约简系统。范畴语义是为类型化lambda演算理论提供数学支持的基本机制。实际上，演算和语义在适当的意义上是等价的，这一众所周知的观察已经产生了许多卓有成效的结果。然而，只有当λ演算的约简规则被视为等式规则时，才能实现等价。即，若要使约简规则具有等效性，则应将约简规则视为静态规则。我们推测，如果将约简规则视为动态的，即可操作的，则等效性仍然成立。但是，如果我们坚持使用类型化lambda计算，这种方法将面临困难。因此，我们转向直觉线性逻辑，这是类型化λ演算的改进。我们采用Ristmann等人的语义作为直觉线性逻辑的范畴语义。对语义中出现的交换图引入约简规则。我们观察了范畴语义上的约简规则与直觉线性逻辑上相应的运算之间的联系。针对范畴语义约简系统的适宜性，我们尝试验证Church-Roaser性质和归一化性质。这些性质是预料之中的，因为它们适用于类型论的许多系统。到目前为止，作为部分结果，我们验证了弱归一化性质。直观线性逻辑是在与面向计算模型相同的基础上设计的，以反映实现细节，如显式替换和Lamping图。我们把我们的还原系统和这些进行了比较。

We interprets categorical semantics of the intuitionistic linear logic as a reduction system. The categorical semantics is a basic machinery providing a mathematical support to the theory of typed lambda calculi. In effect, the calculi and the semantics are equivalcot in a suitable sense, and this well-known observation has yielded a number of fruitful results. The equivaleces is, however, achieved only if the reduction rules of the lambda calculus are viewed as equational rules. Namely, the reduction rules should be regarded as static rules if we want to have the equivalence. We conjecture that the equivalence remsins to hold if the reduction rules are regarded to be dynamic, that is, operational. But this approach faces difficulties if we stick to the typed lambda calcules.Therefore we switch to the intuitionistic liner logic, which is a refinement of the typed lambda calculus. We adopt the semantics by Ristmann et al.as the categorical semantics of the intuitionistic linear logic. We introduce reduction rules on the commutative diagrams occurring in the semantics. We observed the connection between the reduction rules on the categorical semantics and the corresponding operations on the intuitionistic linear logic. Toward appropriateness of the reduction system on the categorical semantics, we attempt to verify the Church-Roaser property and the normalization property. These properties are expected since they hold for many systems of the type theory. So far, as a partial result, we verified the weak normalization property. The intuitionistic linear logic is designed on the same basis as the computational model oriented to reflect implementation details, such as the explicit substitution and the Lamping graph. We compared our reduction system to these.