因果演算：在计算中分离产生、存在和解释
The Because-Calculus: Separating Production, Existence, and Interpretation in Computation
浏览论文内容
中文总结 AI 辅助
研究处理演算中可恢复与不可恢复效果操作混合的问题，因果演算用对偶效果行等分离注册与证明，拒绝空绑定子句，证明合并定理，还建立了演算的进展、归约等性质。
中文摘要 AI 辅助
处理演算通过单一的do结构将可恢复和不可恢复的效果操作混在一起，仅通过结果类型注释来区分。这种混合并不损害类型安全性——进展和保存属性成立——但它允许为不可恢复的操作进行恢复绑定，从而创建了在因果演算中在编译时消除的空绑定。因果演算使用对偶效果行和层级索引类型在结构上分离注册（不可恢复，返回void）和证明（可恢复，不返回void），并通过恢复子约束在编译时拒绝此类子句。我们证明了合并定理：将存在、替换和全称函子的伴随三元组合并为单个效果操作是不忠实的——从因果演算到处理演算的擦除将被拒绝的子句映射为被接受的子句。四个动作对应于四个自然变换；范畴语义将每个判断映射到一个范畴论构造。我们为完整的演算建立了进展、主体归约和塔进展。
英文摘要
Handler calculus conflates resumable and non-resumable effect operations through a single do construct, distinguished only by result type annotation. This conflation does not compromise type safety -- progress and preservation hold -- but it permits resumption bindings for non-resumable operations, creating vacuous bindings that the because-calculus eliminates at compile-time. The because-calculus structurally separates registration (non-resumable, void-returning) from attestation (resumable, non-void-returning) using dual effect rows and level-indexed typing, rejecting such clauses at compile-time via the Resumption Subconstraint. We prove the Conflation Theorem: collapsing the adjoint triple of existential, substitution, and universal functors into a single effect operation is non-faithful -- the erasure from the because-calculus to handler calculus maps rejected clauses to accepted ones. Four movements correspond to four natural transformations; categorical semantics maps each judgment to a category-theoretic construct. We establish progress, subject reduction, and tower progress for the full calculus.
