We present a simple technique for semantic, open logical relations arguments about languages with recursive types, which, as we show, follows from a principled foundation in categorical semantics. We demonstrate how it can be used to give a very straightforward proof of correctness of practical forward- and reverse-mode dual numbers style automatic differentiation (AD) on ML-family languages. The key idea is to combine it with a suitable open logical relations technique for reasoning about differentiable partial functions (a suitable lifting of the partiality monad to logical relations), which we introduce.

翻译：我们提出了一种简单的方法,用语义和开放的逻辑关系来论证具有递归性类型的语言,正如我们所显示的那样,这些逻辑关系源自绝对语义的原则基础。我们展示了如何利用它来非常直接地证明实际的前式和反式双数字风格的对多语言-家庭语言的自动区分。关键的想法是将其与适当的开放逻辑关系技术结合起来,以推理不同部分功能(适当将偏向性调和逻辑关系调和),我们引入了这种功能。