We give a simple, direct and reusable logical relations technique for languages with recursive features and partially defined differentiable functions. We demonstrate it by working out the case of Automatic Differentiation (AD) correctness: namely, we present a proof of the dual numbers style AD macro correctness for realistic functional languages in the ML-family. We also show how this macro provides us with correct forward- and \textit{reverse-mode} AD. The starting point is to interpret a functional programming language in a suitable freely generated categorical structure. In this setting, by the universal property of the syntactic categorical structure, the dual numbers AD macro and the basic $\omega$-cpo semantics arise as structure preserving functors. The proof follows, then, by a novel logical relations argument. The key to much of our contribution is a powerful monadic logical relations technique for term recursion and recursive types. It provides us with a semantic correctness proof based on a simple approach for denotational semantics, making use only of the very basic concrete model of $\omega$-cpos.

翻译：我们提出了一种简单、直接且可重用的逻辑关系技术，适用于具有递归特征和部分可微函数的语言。我们通过自动微分（AD）正确性的实例进行演示：具体而言，我们为ML家族中现实函数式语言的二元数风格AD宏正确性给出了证明。我们还展示了该宏如何提供正确的前向模式和反向模式AD。出发点是在适当自由生成的范畴结构中解释函数式编程语言。在此设定下，通过语法范畴结构的泛性质，二元数AD宏与基本的$\omega$-cpo语义作为保结构函子出现。随后，通过一种新颖的逻辑关系论证完成证明。我们贡献的关键在于一种针对项递归和递归类型的强大单子逻辑关系技术。该技术基于简单的指称语义方法（仅利用$\omega$-cpos这一基础具体模型）提供了语义正确性证明。