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.