Search papers, labs, and topics across Lattice.
This paper addresses the challenge of representing variant types in reverse-mode automatic differentiation (AD) by embedding cotangent fibers into a common ambient type, allowing for a denotational account without relying on dependently typed languages. The authors establish that this approach, which utilizes a primal-indexed idempotent selection mechanism, can transition from a constant-family model to its Karoubi completion, thereby providing a more unified framework for handling cotangent spaces. Key results include the demonstration of a bicartesian closed semantics for reverse-mode AD with variants, showing that dependent cotangent families and simply typed ambient cotangents are equivalent in their denotational transformation capabilities.
Embedding cotangent fibers in a common ambient type reveals a surprising equivalence between dependent and simply typed semantics in reverse-mode automatic differentiation.
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 $\kappa$, we prove that the constant-family inclusion extends to an equivalence $\mathrm{Kar}(\mathrm{Copow}*\kappa(\mathcal C)) \simeq \mathrm{Fam}*\kappa(\mathcal C)$ precisely when $\mathcal C$ is Cauchy complete and every $\kappa$-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.
