经典计算概念与 Hasegawa-Thielecke 定理（扩展版）

在 Curry-Howard 对应关系中关于证明与程序之间的关系的精神下，我们定义并研究了具备计算对偶负律的经典逻辑的语法与语义，采用极化效应计算论（polarised effect calculus），即线性经典 L -calculus。为该计算构建语义解释的主要挑战在于容纳 call-by-value 与 call-by-name 评估策略，这导致复合关联性失效。为克服此问题，我们定义了图形态射之间正交性的概念，用于刻画极化与非关联性的对称单母论封闭型 duploid 以及对话 duploid。我们表明，这些结构分别为正交模型提供了直接风格的对应形式：线性效应正交模型用于（线性）call-by-push-value 计算，dialogue chiralities 用于线性 continuations。特别是，我们展示了线性经典 L-calculus 的语法可在任何 dialogue duploid 中解释，实际上它定义了一个语法 dialogue duploid。作为应用，我们通过语义与语法手段，确立了 Hasegawa-Thielecke 定理，即在任何 dialogue duploid 中，中心映射与 thunkable 映射的概念相吻合（特别是对于任意双重否定单子在对称单母论范畴中）。