Simply Typed Reverse-Mode Automatic Differentiation with Variants: Denotational Correctness via Idempotent Completion
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2607.14453
curl -X POST /api/v1/records/arxiv/2607.14453/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2607.14453/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'