Freely Generated Categorical Structures and Automatic Differentiation, PhD Thesis (Introduction and Conclusion)

About this version

• The six research papers in Chapters 2–7 are not reproduced in this version and are available separately.The original chapter numbering is retained: the introduction is Chapter 1 and the conclusion Chapter 8.Source: About this version · p. 3
• The author reports a leading role in mathematical development and manuscript preparation, especially formulating and proving main results, in close collaboration with the named coauthors.Chapters 2, 3, 5, and 7 are joint work with Matthijs Vákár; Chapter 4 with Gordon Plotkin and Matthijs Vákár; and Chapter 6 with Rui Prezado and Matthijs Vákár.Source: About this version · p. 3

Papers in the full thesis

• Chapters 2–4 list “Automatic differentiation for ML-family languages: Correctness via logical relations”, “CHAD for expressive total languages”, and “Unraveling the iterative CHAD”.Source: Papers in the full thesis · p. 3
• Chapters 5–7 list “Free Doubly-Infinitary Distributive Categories are Cartesian Closed” [25], “Free extensivity via distributivity” [27], and “Monoidal closure of Grothendieck constructions via Σ-tractable monoidal structures and Dialectica formulas”.Source: Papers in the full thesis · p. 3

Introduction

• The thesis seeks compile-time automatic differentiation for expressive languages, with a precise semantics and proofs that transformed programs compute derivatives.Universal properties determine transformations from their action on primitives; correctness also depends on correct primitive derivatives and a semantic argument relating the transformed program to differentiation.Source: Introduction · p. 7

1.1 Reverse-mode Automatic Differentiation

• The central challenge is to formulate correct, compositional forward- and reverse-mode transformations for expressive languages with inductive types, recursion, and non-termination.The thesis argues that categorical semantics provides a suitable framework, building on dual-number AD [14], Elliott’s account [10], and CHAD [40].Source: §1.1 · p. 8

1.2 Categorical Semantics of Programming Languages

• Categorical methods guide structure-preserving transformations and correctness proofs, while AD exposes limits in existing frameworks and prompts richer categorical theories.The thesis also investigates free constructions and indexed models.Source: §1.2 · p. 9

1.3 Functoriality

• Because differentiation respects identities and composition through the chain rule, the thesis frames it as a functor that preserves relevant categorical structure.CHAD represents each manifold by its underlying set paired with a family of cotangent spaces; its morphisms carry the corresponding co-derivatives.Source: §1.3 · pp. 9–10

1.3.1 Structure-preserving functoriality

• Differentiation must preserve the categorical structure of the language, not merely identities and composition.The thesis illustrates this with products: cotangent spaces of products decompose as direct sums, and the cotangent space of the one-point manifold is zero.Source: §1.3.1 · pp. 10–11

1.3.2 Forward CHAD and dual numbers

• Forward CHAD and dual numbers agree on first-order types and at real inputs and outputs, but CHAD’s total-elements functor does not preserve exponentials.The agreement extends to programs using higher-order constructs internally; the exponential comparison omits functions such as v ↦ v^2, so higher-order values are organised differently.Source: §1.3.2 · pp. 11–12

1.4 Expressiveness

• Classical manifold categories lack variant types, and neither Man nor VMan is cartesian closed; VMan also lacks general partiality, unbounded iteration, and coinductive types.The thesis presents expressiveness as a central challenge: functional languages require higher-order functions, recursion, iteration, and recursive types, while classical differentiation does not accommodate non-termination.Source: §1.4 · pp. 12–14
• Recursive functions and types often occur together, but objects solving recursive domain equations and supporting recursively specified morphisms may not exist in VMan, limiting its adequacy for realistic languages.The thesis therefore motivates moving beyond concrete categories when modelling standard programming-language constructs.Source: §1.4 · p. 15

1.5 Freely generated categorical structures

• Treating languages modulo βη as freely generated categorical structures lets universal properties specify transformations and semantic models with logical relations establish their agreement with differentiation.This approach avoids committing to one concrete extension of VMan while supporting richer language features and compatibility with standard models where applicable.Source: §1.5 · pp. 15–16

1.6 AD from universal properties

• AD is characterized as a structure-preserving transformation uniquely extended from primitive operations, with correctness established using semantic models and categorical logical relations.The framework covers forward- and reverse-mode AD, including CHAD for total higher-order languages with rich data types and Iterative CHAD for first-order languages with partial operations and while-loops.Source: §1.6 · p. 16

1.7 Free extensivity and distributivity

• The thesis introduces the Dist pseudomonad for doubly-infinitary distributive categories and proves that their free completions are cartesian closed, so function types arise from freeness.This distributivity is strictly stronger than ordinary infinitary distributivity; the result was motivated by programming-language semantics but also contributes to two-dimensional monad theory.Source: §1.7 · p. 17, §1.10 · p. 20

1.8 Grothendieck constructions

• Indexed cotractability, suitable Π-types, and base-category hypotheses provide a uniform construction of internal homs and cartesian or monoidal closed total categories from indexed categories.These Grothendieck-construction results address structure needed by CHAD and contribute independently to fibred category theory.Source: §1.8 · p. 18

1.9 Extensivity and related contributions

• Extensive indexed categories make coproducts lift through Grothendieck constructions, while iteration-extensive indexed categories relate loop substitution to parameterised initial algebras.Σ-tractable coproduct structures generalize extensivity's decomposition of morphisms and clarify coproducts' interaction with exponentials; together these results connect coproducts, iteration, lifting, and monoidal closure.Source: §1.9 · pp. 18–19

1.10 Contributions and Thesis Outline

• The thesis develops dual-numbers AD for ML-family languages with recursive types, CHAD for expressive total languages [21], and iterative CHAD for partial programs with while-loops [26].The accounts provide semantic correctness results; iterative CHAD additionally preserves the program's domain of definition and computes its reverse-mode derivative wherever defined.Source: §1.10 · pp. 19–20
• A canonical pseudodistributive law between free coproduct and suitable-limit completions yields a pseudomonad for natural classes of extensive categories; free doubly-infinitary lextensive categories are cartesian closed [27].The result extends the distributivity work [25] and establishes structural compatibility between sum types and function types.Source: §1.10 · p. 21
• Chapter 7 studies preservation of exponentials through Grothendieck constructions and introduces left Kan extensivity as a uniform mechanism for computing their colimits.The notion refines how coproducts behave under fibred colimit formation.Source: §1.10 · p. 21
• Indexed cotractability, suitable Π-types, and base-category hypotheses provide sufficient conditions for monoidal closure through a Dialectica-inspired formula.Σ-tractable coproducts unify and extend cocartesian coclosed structures, biproducts, and extensive coproducts.Source: §1.10 · pp. 21–22
• Challenges from AD and CHAD motivated this work, which extends the theory of extensive indexed categories and clarifies exponentials in Grothendieck constructions.The investigation began with the need to understand how closure and extensivity are transported through Grothendieck constructions.Source: §1.10 · pp. 21–22
• Universal properties provide a common framework for the transformations, while categorical logical relations and semantic comparisons establish their correctness.The development contributes to automatic differentiation for expressive languages and to free and fibred categorical structures, suggesting a broader programme of structure-preserving transformations.Source: §1.10 · p. 22

Conclusion and Future Work

• Automatic differentiation provides the setting for examining the interaction between categorical semantics and program transformation.Source: Conclusion and Future Work · p. 23
• The framework accounts compositionally for linear transformations, higher-order functions, recursive types, sums, iteration, and partiality.Source: Conclusion and Future Work · p. 23
• Treating languages as freely generated categorical structures lets the thesis define AD on primitives and organize correctness proofs through universal properties and categorical logical relations.Source: Conclusion and Future Work · p. 23
• Questions about free completions and Grothendieck constructions led to results of independent categorical interest.Source: Conclusion and Future Work · p. 23

From Foundations to Homomorphic AD

• Dual-numbers AD is a structure-preserving morphism between ML-family source and extended target languages with recursive types, with correctness proved using categorical logical relations.The proof accommodates recursive types, partial primitives, and differentiability/local properties.Source: From Foundations to Homomorphic AD · p. 23
• CHAD extends forward- and reverse-mode AD to total languages with tuples, variants, inductive and coinductive types, and higher-order functions.Its dependent target semantics uses extensive indexed categories to model sums in the Grothendieck construction; correctness uses universal properties and logical relations.Source: From Foundations to Homomorphic AD · p. 23
• Iterative CHAD extends the first-order CHAD fragment to general iteration and non-termination through iteration-extensive indexed categories.Folds yield fibred iteration, while iterative folders express target-language operations; the homomorphic extension proves domain preservation and derivative correctness.Source: From Foundations to Homomorphic AD · pp. 23–24

From AD to Foundations

• Free doubly-infinitary distributive categories are cartesian closed, while free doubly-infinitary lextensive completions are cartesian closed as well.In the free infinitary lextensive case, objects with finitely many connected components are exponentiable.Source: From AD to Foundations · p. 24
• Extensive indexed categories clarify coproducts, iteration, and parameterised initial algebras and terminal coalgebras within Grothendieck constructions.Source: From AD to Foundations · p. 24
• Indexed Σ-cotractability, suitable Π-types, and base-category hypotheses give sufficient conditions for monoidal closure of the total category.Left Kan extensivity describes how colimits lift to Grothendieck constructions.Source: From AD to Foundations · p. 24
• The foundational results arose from challenges in principled AD macros and contribute independently to extensive categories, fibred category theory, and two-dimensional universal algebra.Source: From AD to Foundations · p. 24

Limitations

• Categorical semantics yields concrete AD macros whose derivative correctness is established by semantic proofs.The work addresses reverse-mode AD for the expressive programming languages studied.Source: Limitations · p. 24
• Remaining implementation frontiers include efficiency challenges, defunctionalisation, and how CHAD might further exploit parallelism.The thesis proposes studying operational aspects, categorical semantics of defunctionalisation, and structured approaches to parallelism.Source: Limitations · p. 24
• The open question is whether categorical reasoning that secured correctness can also provide a systematic roadmap to efficiency, optimisation, and implementation.Source: Limitations · p. 25

Finite probability and effects

• Finite-support probabilistic CHAD accounts for differentiable weights and compositional monadic operations and handlers, proving correctness for handled programs with real-valued outputs.Continuous probability and more general combinations of effects remain for future work.Source: Recent Developments · p. 25

Simply typed dependent CHAD

• Dependent CHAD has a simply typed presentation for products, variants, and higher-order functions, with primal-indexed idempotents representing variant cotangent fibres inside ordinary types.Its ambient transformation preserves composition but maps identities to idempotents; in the Cauchy completion its interpretation is an ordinary functor.Source: Recent Developments · p. 25

Two strands

• The research agenda combines advances in program transformations and differentiable programming with a broader categorical toolkit for programming-language semantics.The thesis identifies these as complementary strands of further research.Source: Future Work · p. 25

Program transformations and differentiable programming

• Extending CHAD to ML-family languages includes developing recursion and recursive types in an indexed target or a suitable simply typed presentation.This direction builds on the thesis’s CHAD account.Source: Future Work · p. 25
• Higher-order reverse-mode differentiation would extend the homomorphic approach beyond first derivatives to principled higher-order derivatives.Source: Future Work · p. 26
• The idempotent-completion account of variants could extend to richer language fragments and inform semantic comparisons for defunctionalisation, closure conversion, and sharing.Source: Future Work · p. 26
• The finite-probability and discrete-output account could extend to richer probabilistic languages and combinations of algebraic effects and handlers while retaining compositional semantics and correctness proofs.Source: Future Work · p. 26

Categorical toolkit for semantics and transformations

• A broader categorical toolkit could systematise presentations of categorical structures, especially coherence and comparisons between alternative models of the same language constructs.Source: Future Work · p. 26
• Value-indexed semantic data may support uniform, structure-preserving transformations beyond differentiation, though their applications and implementation remain future work.Source: Future Work · p. 26

Closing

• The thesis derives compositional AD transformations for expressive languages, and its CHAD account helped form the foundation for an efficient implementation.The implementation is by Smeding and Vákár.Source: Closing · p. 26
• The requirements of AD also led to independent results on free completions, extensivity, and Grothendieck constructions.Source: Closing · p. 26
• The thesis advocates developing categorical models, correctness proofs, and efficient implementations together, with explicit correctness guarantees for practically useful transformations.Source: Closing · p. 26

Overview

• The thesis develops categorical semantics around the practical problem of structure-preserving AD transformations, whose compositionality and correctness are established using categorical logical relations.The syntax modulo its standard βη equations is treated as a freely generated categorical structure, so structure-preserving transformations arise from its universal properties.Source: Samenvatting · pp. 31–32

Mathematical results

• The categorical tools developed for CHAD extend to results on distributive and extensive categories and clarify the structure of Grothendieck constructions.Source: Samenvatting · p. 32

Automatic Differentiation for ML-family Languages

• For ML-family languages with recursive types, forward- and reverse-mode AD use dual numbers and are proved correct with a reusable logical-relations framework.The AD macro is formulated as a structure-preserving morphism between source- and target-language syntactic models.Source: Samenvatting · p. 32

CHAD for Expressive Total Languages

• CHAD handles total languages with sums, products, inductive and coinductive types, and function types, using extensive indexed categories to treat sums.The account integrates inductive and coinductive types into dependent type semantics and uses logical-relations techniques for correctness.Source: Samenvatting · pp. 32–33

Unraveling the Iterative CHAD

• Iterative CHAD extends the transformation to first-order languages with iteration and nontermination using iteration-extensive indexed categories.These structures provide categorical foundations for certain colimits and iteration in the corresponding Grothendieck constructions.Source: Samenvatting · pp. 32–33

Free Doubly-Infinitary Distributive Categories

• Free doubly-infinitary distributive categories, where arbitrary small products distribute over arbitrary small coproducts, are cartesian closed.Source: Samenvatting · p. 33

Free Extensivity via Distributivity

• Free doubly-infinitary lex-extensive categories are cartesian closed, and in free infinitely lex-extensive categories objects with finitely many connected components are exponentiable.Source: Samenvatting · p. 33

Grothendieck constructions

• The thesis studies Grothendieck constructions through left-Kan-extensivity and Σ-(co)tractable monoidal structures, deriving conditions for colimits and monoidal closure.Source: §7 · p. 34

• The thesis treats programming-language syntax modulo βη-equations as a freely generated categorical structure, so structure-preserving transformations arise from universal properties.The categorical approach is developed alongside implementation challenges and correctness proofs.Source: Summary · p. 35
• Forward-mode AD for recursive higher-order languages is defined as a functor mapping each primitive to code for its value and derivative action, with correctness proved using logical relations.The correctness method covers recursive types and partial primitives.Source: Summary · p. 35
• CHAD extends the homomorphic approach to reverse-mode AD for total languages with products, sums, inductive and coinductive types, and functions.Its semantics uses total categories associated with indexed categories and extensive indexed categories for disjoint sums.Source: Summary · pp. 35–36
• For partial first-order languages with general iteration, iteration-extensive indexed categories relate loop substitution to parameterised initial algebras, while iterative folders provide target-language operations.This supports unbounded loops and a correctness proof for the extended transformation.Source: Summary · p. 36
• The thesis’s AD work also leads to foundational results in fibred category theory and in the theory of distributive and extensive categories.Source: Summary · p. 36

Automatic Differentiation for ML-family Languages

• Forward- and reverse-mode AD for ML-family languages with recursive types is formulated as a structure-preserving morphism and proved correct using logical relations.The paper introduces a reusable logical-relations framework for recursive types and languages with effects.Source: §1 · p. 36

CHAD for Expressive Total Languages

• CHAD is developed for total languages with sums, products, inductive, coinductive, and function types, using extensive indexed categories and categorical logical-relations techniques.Source: §1 · p. 36

Unraveling the Iterative CHAD

• CHAD is extended to first-order languages with iteration and non-termination through iteration-extensive indexed categories and iterative folders for target-language operations.Source: §1 · p. 37

Free Doubly-Infinitary Distributive Categories

• Doubly-infinitary distributive categories allow arbitrary small products to distribute over arbitrary small coproducts, and their free categories are cartesian closed [25].Source: §1 · p. 37

Free Extensivity via Distributivity

• Pseudodistributive laws yield notions of extensive categories; freely generated doubly-infinitary lextensive categories are cartesian closed [27].In freely generated infinitary lextensive categories, objects with finitely many connected components are exponentiable.Source: §1 · p. 37

Monoidal Closure of Grothendieck Constructions

• Left-Kan extensivity provides a framework for colimits in Grothendieck constructions, while Σ-(co)tractable monoidal structures give sufficient conditions for closed monoidal structures.Source: §7 · p. 38