Backpropagation in the Simply Typed Lambda-Calculus with Linear Negation
Backpropagation in the Simply Typed Lambda-Calculus with Linear Negation
复制标题
DOI：
10.1145/3371132
复制
发表时间：
2020-01-01
影响因子：
1.8
通讯作者：
Pagani, Michele
中科院分区：
文献类型：
--
作者：
Brunel, Alois;Mazza, Damiano;Pagani, Michele
反向传播是一种经典的自动微分算法，用于计算一类简单的一阶程序（称为计算图）所指定的函数的梯度。它是几个领域的基本工具，最著名的是机器学习，它是有效训练（深度）神经网络的关键。近年来，一个被称为可微规划的研究领域得到了迅速发展，其目的是借助具有控制流算子和高阶组合子（如map和fold）的实际编程语言，更加综合和模块化地表达计算图。在本文中，我们将反向传播算法推广到这种编程语言的一个典型例子：我们定义了一个组合程序变换，从简单类型的λ -演算到带有线性否定概念的自身增广，并证明了它以与一阶反向传播相同的效率计算源程序的梯度。这种转换是完全不受影响的，因此提供了对反向传播动力学的纯逻辑理解。
Backpropagation is a classic automatic differentiation algorithm computing the gradient of functions specified by a certain class of simple, first-order programs, called computational graphs. It is a fundamental tool in several fields, most notably machine learning, where it is the key for efficiently training (deep) neural networks. Recent years have witnessed the quick growth of a research field called differentiable programming, the aim of which is to express computational graphs more synthetically and modularly by resorting to actual programming languages endowed with control flow operators and higher-order combinators, such as map and fold. In this paper, we extend the backpropagation algorithm to a paradigmatic example of such a programming language: we define a compositional program transformation from the simply-typed lambda-calculus to itself augmented with a notion of linear negation, and prove that this computes the gradient of the source program with the same efficiency as first-order backpropagation. The transformation is completely effect-free and thus provides a purely logical understanding of the dynamics of backpropagation.