具有变体的简单类型反向模式自动微分：通过幂等完备实现指称正确性
Simply Typed Reverse-Mode Automatic Differentiation with Variants: Denotational Correctness via Idempotent Completion
AI总结：
研究反向模式自动微分中变体类型带来的问题，通过将余切纤维嵌入公共环境类型，利用幂等元选择有效纤维，证明相关等价关系并构造余积，获得双笛卡尔闭语义，表明依赖余切族和简单类型环境余切是等价表示。
AI中文摘要：
反向模式自动微分通常有一个指称解释，其中每个源类型有一个单一的余切类型。变体类型阻碍了这种简单类型的表示，因为有效的余切空间取决于运行时选择的分支。现有的正确性结果因此使用原语索引的余切空间族，其自然内部语言是依赖类型的。我们表明相同的依赖性可以在普通的非依赖目标中表示。每个源类型的余切纤维嵌入到一个公共的环境类型中，并且一个原语索引的幂等元选择有效的纤维。语义上，这相当于从常量族模型过渡到其卡鲁比完备。对于一个范畴$\mathcal C$和一个正则无限基数$\kappa$，我们证明当$\mathcal C$是柯西完备的且每个$\kappa$-小族都有一个公共的收缩宿主时，常量族包含扩展为一个等价关系$\mathrm{Kar}(\mathrm{Copow}*\kappa(\mathcal C)) \simeq \mathrm{Fam}*\kappa(\mathcal C)$。我们还明确构造了所得的余积。应用这个定理，我们仅使用普通目标类型、投影器和反向传播器就获得了具有变体的反向模式自动微分的双笛卡尔闭语义。拆分生成的幂等元可恢复已建立的依赖语义。因此，依赖余切族和配备投影器的简单类型环境余切是同一指称变换的等价表示。
英文摘要：
Reverse-mode automatic differentiation is commonly given a denotational account in which each source type has a single cotangent type. Variant types obstruct this simply typed representation because the valid cotangent space depends on the branch selected at run time. Existing correctness results therefore use primal-indexed families of cotangent spaces, whose natural internal language is dependently typed. We show that the same dependency can be represented in an ordinary nondependent target. The cotangent fibres of each source type are embedded in a common ambient type, and a primal-indexed idempotent selects the valid fibre. Semantically, this amounts to passing from the constant-family model to its Karoubi completion. For a category $\mathcal C$ and a regular infinite cardinal $κ$, we prove that the constant-family inclusion extends to an equivalence $\mathrm{Kar}(\mathrm{Copow}*κ(\mathcal C)) \simeq \mathrm{Fam}*κ(\mathcal C)$ precisely when $\mathcal C$ is Cauchy complete and every $κ$-small family admits a common retract host. We also construct the resulting coproducts explicitly. Applying this theorem, we obtain a bicartesian closed semantics for reverse-mode automatic differentiation with variants using only ordinary target types, projectors, and backpropagators. Splitting the generated idempotents recovers the established dependent semantics. Thus dependent cotangent families and simply typed ambient cotangents equipped with projectors are equivalent presentations of the same denotational transformation.
