自由生成的范畴结构与自动微分，博士论文（引言与结论）
Freely Generated Categorical Structures and Automatic Differentiation, PhD Thesis (Introduction and Conclusion)
浏览论文内容
中文总结 AI 辅助
本博士论文将编程语言视为自由生成的范畴结构，以自动微分为核心应用，研究前向与反向模式微分，并推动自由分配范畴等数学结果，实现理论与实践的双向互动。
中文摘要 AI 辅助
本版本包含我的博士论文《自由生成的范畴结构与自动微分》的引言和结论，以及其英文和荷兰语摘要。完整论文由引言章节、六篇合作研究论文和结论章节组成，这些内容是在乌得勒支大学攻读博士学位期间，在加布里埃尔·凯勒和马泰斯·瓦卡尔的指导下完成的。研究论文可单独获取，此处不再复制。引言部分阐述了论文的研究范围，解释了六篇论文的贡献及其相互联系，并介绍了我们方法的范畴学基础。核心思想是：将编程语言视为自由生成的范畴结构，为构造保持结构的程序变换并证明其正确性提供了原则性框架。自动微分提供了核心应用：我们研究了具有表达力的类型化语言的前向和反向模式微分，包括高阶函数、递归类型、迭代和偏序性。这些变换的语义需求也推动了关于自由分配范畴和余分配范畴、笛卡尔闭性以及格罗滕迪克构造的独立数学结果。结论部分将这些贡献汇聚在一起，讨论了它们的局限性，并概述了未来的研究方向。整个论文在理论与实践之间建立了对话：范畴语义指导了可靠且实用的程序变换的构造，而计算的需求则催生了新的范畴结构和结果。
英文摘要
This version contains the introduction and conclusion of my PhD thesis, "Freely Generated Categorical Structures and Automatic Differentiation", together with its English and Dutch summaries. The full thesis consists of an introductory chapter, six joint research papers, and a concluding chapter, developed during my PhD studies at Utrecht University under the supervision of Gabriele Keller and Matthijs Vákár. The research papers are available separately and are not reproduced here. The introduction presents the scope of the thesis, explains the contributions of the six papers and their connections, and introduces the categorical foundations of our approach. The guiding idea is that programming languages, viewed as freely generated categorical structures, provide a principled setting for constructing structure-preserving program transformations and proving their correctness. Automatic differentiation supplies the central application: we study forward- and reverse-mode differentiation for expressive typed languages, including higher-order functions, recursive types, iteration and partiality. The semantic requirements of these transformations also motivate independent mathematical results on free distributive and extensive categories, cartesian closedness, and Grothendieck constructions. The conclusion brings these contributions together, discusses their limitations, and outlines further directions. Throughout, the thesis develops a dialogue between theory and practice: categorical semantics guides the construction of reliable and practically useful program transformations, while the demands of computation lead to new categorical structures and results.
发表机构
- Utrecht University（乌得勒支大学）
- Department of Information and Computing Sciences Utrecht University（乌得勒支大学信息与计算科学系）
机构由 AI 辅助整理，请以论文原文为准。
