The logical principles of focalisation and polarisation can be used to design well-behaved term syntaxes for sequent calculus, which play a role as meta-languages for describing effectful computation. On the semantics side, this corresponds to an axiomatic and polarised notion of model of computation stated in terms of adjunctions over non-associative categories. In this paper, we study the special and delicate cases of resource and effect modalities in a general intuitionistic and linear setting: an exponential comonad $!$ (refining $\square$) and a strong monad $\lozenge$. The starting point of our contribution is noticing that the completeness for a polarised syntax for $!$ and $\lozenge$ with respect to (co)monads in linear call-by-push-value models can be achieved if we move to relative (co)monads: more precisely, comonads relative to $\downarrow$ (the positive shift functor) for $!$ and monads relative to $\uparrow$ (the negative shift functor) for $\lozenge$. These specialisations of the concept of relative (co)monad to call-by-push-value adjunctions recently appeared. Yet the syntax we present arose from proof-theoretic consideration, without the link with relative (co)monads being noticed at the time. Our first remark is thus that (co)monads relative to a call-by-push-value adjunction have been motivated previously from a proof-theoretic perspective in the context of focalisation, which also provides a meta-language for these concepts in an effectful setting. We carry out the study of these modalities from the axiomatic, non-associative point of view. We recall the notion of adjunction over non-associative categories, and establish correspondence results between this notion of adjunction and that of relative adjunction. This correspondence is then extended to linear-non-linear and strong versions of adjunctions as needed to model $!$ and $\lozenge$.

翻译：焦点化与极化逻辑原则可用于设计良构的相继式演算项语法，这些语法作为描述带效应计算的无语言发挥作用。从语义学角度来看，这对应于基于非结合范畴上的伴随来表述的模型之公理化与极化概念。本文在广义的直观与线性背景下研究资源和效应模态的特殊且敏感的情况：指数余单子$!$（对$\square$的细化）及强单子$\lozenge$。我们贡献的出发点在于注意到：若转向相对（余）单子——具体而言，对于$!$是相对于$\downarrow$（正向移位函子）的余单子，对于$\lozenge$是相对于$\uparrow$（反向移位函子）的单子——则可实现$!$和$\lozenge$相对于线性按名调用-传值模型中（余）单子的极化语法的完备性。这些相对（余）单子概念向按名调用-传值伴随的特殊化最近才出现。然而，我们所提出的语法源于证明论考量，当时并未注意到它与相对（余）单子的联系。因此，我们的首要发现是：在焦点化背景下，从证明论视角出发，已有对相对于按名调用-传值伴随的（余）单子的动机阐述，这同时也为带效应环境中的这些概念提供了元语言。我们从公理化的非结合视角出发对这些模态展开研究。我们回顾了非结合范畴上的伴随概念，并在该伴随概念与相对伴随概念之间建立对应关系。随后，该对应被扩展到线性-非线性及强伴随版本，以适应对$!$和$\lozenge$建模的需求。