We present semantic correctness proofs of forward-mode Automatic Differentiation (AD) for languages with sources of partiality such as partial operations, lazy conditionals on real parameters, iteration, and term and type recursion. We first define an AD macro on a standard call-by-value language with some primitive operations for smooth partial functions and constructs for real conditionals and iteration, as a unique structure preserving macro determined by its action on the primitive operations. We define a semantics for the language in terms of diffeological spaces, where the key idea is to make use of a suitable partiality monad. A semantic logical relations argument, constructed through a subsconing construction over diffeological spaces, yields a correctness proof of the defined AD macro. A key insight is that, to reason about differentiation at sum types, we work with relations which form sheaves. Next, we extend our language with term and type recursion. To model this in our semantics, we introduce a new notion of space, suitable for modeling both recursion and differentiation, by equipping a diffeological space with a compatible $\omega$cpo-structure. We demonstrate that our whole development extends to this setting. By making use of a semantic, rather than syntactic, logical relations argument, we circumvent the usual technicalities of logical relations techniques for type recursion.

翻译：本文针对包含偏运算、实数参数上的惰性条件分支、迭代以及项与类型递归等偏性来源的语言，给出了前向模式自动微分（AD）的语义正确性证明。我们首先在一个标准的按值调用语言上定义AD宏，该语言包含光滑偏函数的基本运算、实数条件分支及迭代结构；该AD宏由其作用于基本运算的方式唯一确定为一个保持结构的宏。我们利用微分空间为该语言定义了一种语义，其核心思想是借助合适的偏性单子。通过在微分空间上构建子层构造形成的语义逻辑关系论证，导出了所定义AD宏的正确性证明。一个关键见解是：为了推理和类型上的微分，我们需处理构成层的关系。随后，我们将语言扩展至包含项与类型递归。为在语义中建模此特性，我们引入了一种新的空间概念——通过为微分空间配备兼容的$\omega$cpo结构，使其能同时建模递归与微分。我们证明了整个理论框架可推广至此设定。通过采用语义而非语法的逻辑关系论证，我们规避了类型递归逻辑关系技术中常见的复杂性。