计算半效应的逻辑与等变函子的范畴胶合

本文从幺半作用（actegory）逻辑的视角重新审视 Moggi 著名的计算效应演算。我们的研究包含以下步骤。首先，我们对 Moggi 的计算元语言进行证明论重构，并得到一个以模态类型 $\rhd$ 作为细化的类型理论。通过命题即类型范式，其逻辑可被视为通过 Benton 的伴随演算对松弛逻辑的分解。该演算作为一种编程语言，对效应的一种较弱版本进行建模，我们将其称为“半效应”。其次，我们利用 actegory 和等变函子给出其语义。与以往关于效应和 actegory 的研究相比，我们的方法更具一般性，因为模型直接由等变函子给出，后者将 Freyd 范畴（进而强单子）作为特例包含在内。第三，我们证明沿等变函子的范畴胶合是可行的，并导出了 $\rhd$-模态的逻辑谓词。我们还证明，在自然假设下，这种胶合产生的逻辑谓词与 Katsumata 为 Moggi 元语言导出的范畴 $\top\top$-提升所给出的逻辑谓词相一致。