基于微分空间与范畴粘合的自动微分正确性证明

该论文为自动微分（AD）给出语义正确性证明，将高阶语言上前向模式 AD 刻画为在选定基本运算导数后唯一的结构保持宏，并基于微分空间（diffeological spaces）建立可微编程的丰富语义。作者证明该语义可解释其语言，并用微分空间上的粘合构造给出 AD 正确性的优雅语义证明，本质上是一种逻辑关系论证。最后通过基于 continuation 的方法说明该分析可扩展到其他 AD 方法。