论文标题
部分特征的逻辑关系和自动分化正确性
Logical Relations for Partial Features and Automatic Differentiation Correctness
论文作者
论文摘要
我们为语义，开放的逻辑关系论证提供了一项简单的技术，该论点涉及具有递归类型的语言，正如我们所展示的那样，它遵循了分类语义中的原则基础。我们演示了如何使用它来简单地证明ML家庭语言上实用的前向模式和反向模式双数字样式自动分化（AD）。关键思想是将其与适当的开放逻辑关系技术结合起来，以推理可区分的部分功能（合适的副本单月份向逻辑关系提升），我们介绍了这一点。
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.
