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.
翻译:在范畴可实现性中,通常由应用结构构造出装配体范畴与适度集范畴。这些范畴拥有与应用结构之结构相对应的结构。文献中,诱导笛卡尔闭范畴、对称幺半闭范畴等范畴结构的应用结构类别已被广泛研究。本文通过识别产生闭多范畴、闭范畴、双闭幺半范畴以及(非对称)幺半闭范畴的应用结构类别,拓展了这些带有结构的范畴与应用结构之间的对应关系。这些应用结构是平面的,因其通过组合完备性对应于适当的平面λ演算。这些新对应关系是紧密的:我们证明,当装配体范畴具有上述结构之一时,基底应用结构便属于相应类别。此外,通过将Abramsky、Haghverdi与Scott的线性组合代数推广至平面设定,我们引入平面线性组合代数,该代数在非对称乘法直觉线性逻辑上为线性指数模态与交换模态提供了范畴模型。