Categorical Reduction

点击翻译按钮获取中文摘要

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.