Multiplexor categories and models of soft linear logic

• Main Author: Redmond, Brian F
• Format: Others
• Language: en
• Published: University of Ottawa (Canada) 2013
• Subjects: Mathematics.
• Online Access: http://hdl.handle.net/10393/29528; http://dx.doi.org/10.20381/ruor-19794

This thesis furthers our semantical understanding of polynomial time complexity by clarifying the semantical status of Lafont's soft linear logic, a logical system complete for polynomial time computation. We shall see that soft linear logic is ideal for this purpose because it possesses a very natural and simple mathematical interpretation. To begin, we introduce the notion of a multiplexor category, which is the categorical interpretation of soft linear logic. We show that a multiplexor category provides a denotational semantics for soft linear logic and that the exponential operator can be interpreted canonically as a certain type of limit. This leads to a large class of models and motivates us to introduce a new class of AJM games which we shall call noetherian. Such games may be infinite, but do not have infinite length plays (i.e. there are no infinite increasing chains of plays in their game trees), hence total strategies will naturally compose. Motivated by notions in complexity theory, we are led to introduce a finitary version of soft linear logic and a corresponding notion of finitary multiplexor category. One of the main results in this thesis is a categorical method for constructing a multiplexor category from a finitary one, called the S-construction, which leads to a stratified view of soft linear logic. This interpretation is inspired by the characterization of PTIME by uniformly polynomial circuits in complexity theory. Our construction has many applications. First, we use it to give a realizability model and a new proof that any algorithm representable in soft linear logic is polytime. Next, we utilize the S-construction to obtain a stratified finite game model of soft linear logic and prove a full-completeness result. Finally, we use it to give an alternative description of a model that has recently appeared in the literature. We also note that the stratified interpretation allows for placing polynomial depth restrictions on the length of plays in our game model. Again, this is consistent with our circuit analogy. We feel that this work provides an important first step towards a truly semantic perspective on PTIME complexity.