自动微分在ML语言中的应用：通过逻辑关系确保正确性
摘要：使用递归特征和部分定义的可微函数的语言，我们提供了一种简单、直接和可重用的逻辑关系技术。我们通过对自动微分（AD）正确性的案例进行详细研究来证明这一点，即我们在ML语言家族中为现实的函数式语言呈现了双重数样式AD宏的正确性证明。我们还展示了这个宏如何为我们提供正确的正向和反向模式AD。 出发点是在一个合适的自由生成的范畴结构中解释一个函数式编程语言。在这个设置中，通过语法范畴结构的通用性质，双重数AD宏和基本的ω-cpo语义作为结构保持函子出现。然后，证明通过一种新颖的逻辑关系论证来完成。 我们贡献的关键部分是一种强大的用于术语递归和递归类型的单子逻辑关系技术。它为我们提供了一个基于简单的指示语义方法的语义正确性证明，仅使用基本的ω-cpo的具体模型。
作者：Fernando Lucatelli Nunes and Matthijs V''ak''ar
论文ID：2210.07724
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-06-21