Semantics for Computational Structures -From Viewpoint of Duality and Noncommutativity-

我们研究由极化线性逻辑引起的计算的语义结构。利用对偶极性的两个逆变范畴之间的模和附加关系，构造了一个范畴模型来模拟计算。为了模拟二阶逻辑的可计算性，我们将极性的拓扑结构容纳到（非极化）代数语义中。利用拓扑语义，我们解决了线性逻辑在其极化片段上的二阶守恒定理。为了建立这两种计算语义和可计算语义之间的关系，我们给出了极化逻辑的一个索引系统，并用该系统表征了一个指称完备性。

We investigate semantcal structures of computations arising from polarized linear logic. A categorical model is constructed to model computations by employing modules and adjunction between two contravariant categories of dual polarities. To model computability for the second order logic, we accommodate a topological structure for the polarities to a (non-polarized) algebraic semantics. Using the topological semantics, we solve a second order conservation theorem of linear logic over its polarized fragment. To make a relationship between these two kind of semantics of computations and of computability, we present an indexed system for polarized logic and characterize a denotational completeness in terms of the system.