상대적 모나드(monads) 및 코모나드(comonads)를 이용한 초점화(focalisation)의 구문론 및 의미론

초점화(focalisation)와 양극화(polarisation)의 논리적 원리는 시퀀트 계산(sequent calculus)을 위한 잘 정의된 항 구문론(term syntaxes)을 설계하는 데 사용될 수 있으며, 이는 효과적인 계산(effectful computation)을 기술하기 위한 메타 언어(meta-languages)로서 역할을 합니다. 의미론 측면에서, 이는 비결합 범주(non-associative categories) 상의 수반(adjunctions)을 통해 기술되는 공리적이고 양극화된 계산 모델의 개념에 대응합니다. 본 논문에서 우리는 일반적인 직관주의 및 선형 설정(intuitionistic and linear setting)에서의 자원 및 효과 양태(resource and effect modalities)라는 특별하고 섬세한 사례를 연구합니다: 즉, 지수 코모나드(exponential comonad) $!$ ($\square$를 정교화함)와 강한 모나드(strong monad) $\lozenge$입니다. 우리 기여의 출발점은 선형 call-by-push-value 모델의 (코)모나드에 대한 $!$ 및 $\lozenge$의 양극화된 구문에 대한 완전성(completeness)이 상대적 (코)모나드(relative (co)monads)로 이동할 때 달성될 수 있다는 점을 주목한 것입니다: 더 정확하게는, $!$에 대해서는 $\downarrow$ (양의 이동 함자, positive shift functor)에 대한 코모나드이며, $\lozenge$에 대해서는 $\uparrow$ (음의 이동 함자, negative shift functor)에 대한 모나드입니다. 상대적 (코)모나드 개념의 이러한 call-by-push-value 수반에 대한 특수화는 최근에 등장했습니다. 그러나 우리가 제시하는 구문론은 상대적 (코)모나드와의 연결을 인지하지 못한 채 증명론적(proof-theoretic) 고려로부터 발생했습니다. 따라서 우리의 첫 번째 언급은 call-by-push-value 수반에 대한 (코)모나드가 이전에 초점화의 맥락에서 증명론적 관점으로부터 동기 부여되었다는 것이며, 초점화는 또한 효과적인 설정에서 이러한 개념들을 위한 메타 언어를 제공합니다. 우리는 이러한 양태(modalities)에 대한 연구를 공리적이고 비결합적인 관점에서 수행합니다. 우리는 비결합 범주 상의 수반 개념을 상기시키고, 이 수반 개념과 상대적 수반(relative adjunction) 개념 사이의 대응 결과(correspondence results)를 확립합니다. 이 대응은 $!$와 $\lozenge$를 모델링하는 데 필요한 대로 수반의 선형-비선형(linear-non-linear) 및 강한(strong) 버전으로 확장됩니다.