Categorical Realizability for Non-symmetric Closed Structures

TL;DR

This paper explores the connections between applicative structures and various non-symmetric closed categorical structures, expanding the categorical realizability framework to include new classes of applicative structures and their corresponding categories.

Contribution

It identifies classes of applicative structures that induce non-symmetric closed categories, extending the existing theory and introducing planar linear combinatory algebras for linear logic models.

Findings

Characterization of applicative structures for non-symmetric closed categories

Introduction of planar linear combinatory algebras

Tight correspondence between categories and applicative structures

Abstract

In categorical realizability, it is common to construct categories of assemblies and categories of modest sets from applicative structures. These categories have structures corresponding to the structures of applicative structures. In the literature, classes of applicative structures inducing categorical structures such as Cartesian closed categories and symmetric monoidal closed categories have been widely studied. In this paper, we expand these correspondences between categories with structure and applicative structures by identifying the classes of applicative structures giving rise to closed multicategories, closed categories, monoidal bi-closed categories as well as (non-symmetric) monoidal closed categories. These applicative structures are planar in that they correspond to appropriate planar lambda calculi by combinatory completeness. These new correspondences are tight: we show that, when a category of assemblies has one of the structures listed above, the based applicative structure is in the corresponding class. In addition, we introduce planar linear combinatory algebras by adopting linear combinatory algebras of Abramsky, Hagjverdi and Scott to our planar setting, that give rise to categorical models of the linear exponential modality and the exchange modality on the non-symmetric multiplicative intuitionistic linear logic.