将增量λ演算演化为前向自动微分模型（AD）

A unified treatment of structural definitions on syntax for capture-avoiding substitution, context application, named substitution, partial differentiation, and so on

We introduce a category-theoreticabstraction of a syntax with auxiliary functions, called an admissiblemonad morphism. Relying on an abstract form of structural recursion,we then design generic tools to construct admissible monad morphismsfrom basic data. These tools automate ubiquitous standard patternslike (1) defining auxiliary functions in successive, potentiallydependent layers, and (2) proving properties of auxiliary functions byinduction on syntax. We cover significant examples from theliterature, including the standard lambda-calculus withcapture-avoiding substitution, a lambda-calculu…

高阶语言的变化理论--用静态微分增量化λ演算

A Theory of Changes for Higher-Order Languages - Incrementalizing λ-Calculi by Static Differentiation

如果一个昂贵的计算的结果被输入的一个小变化所无效，旧的结果应该被增量地更新，而不是重新执行整个计算。我们通过它们的衍生物来增加程序。派生程序将程序输入的变化直接映射到程序输出的变化，而不需要重新执行原始程序。我们提出了一个程序转换程序的衍生物，这是完全静态和自动的，支持一流的功能，并产生衍生物服从标准优化。我们证明了在Agda中对于一族简单类型的λ演算的程序转换是正确的，这些演算由基类型和原语参数化。一个精确的接口指定了增量化所选原语所需的内容。我们调查性能的案例研究：我们在Scala实现的程序转换，一个插件，并提高性能的一个重要的程序的数量级。

DeCo: 一种支持泛型数据类型的增量函数式编程核心演算

DeCo: A Core Calculus for Incremental Functional Programming with Generic Data Types

本文提出DeCo核心演算，通过静态增量泛化用户自定义数据类型上的领域特定操作，实现更细粒度的增量计算，并证明其正确性。

关于资源λ演算测试的鉴别力

On the discriminating power of tests in resource lambda-calculus

自发现以来，差分线性逻辑（DLL）启发了许多领域。在指称语义中，DLL的范畴模型已经比较普遍，其中最简单的是Rel，即集合和关系的范畴。在证明论中，这自然产生了完全和完整的DLL差分证明网。反过来，这些工具可以自然地转化为它们的直觉对应物。通过采取共同克莱斯利类别相关联的！comonad，Rel变成MRel，一个包含微分概念的\Lcalcul模型。证明网可以很自然地用于将\Lcalcul扩展为具有资源的λ演算，一种包含线性和微分概念的演算。当然，MRel是一个有资源的\Lcalcul模型，它已经被证明是足够的，但是它是完全抽象的吗？这是布恰雷利、卡拉罗、埃哈德和曼佐内托的一个强有力的猜想。然而，在本文中，我们展示了一个反例。此外，为了更直观地了解反例的本质并寻求更大的普遍性，我们将使用Bucciarelli等人也引入的资源\Lcalcul的扩展，其中$\Minf$是完全抽象的，即测试。

Functorial String Diagrams for Reverse-Mode Automatic Differentiation

We enhance the calculus of string diagrams for monoidal categories with hierarchical features in order to capture closed monoidal (and cartesian closed) structure. Using this new syntax we formulate an automatic differentiation algorithm for (applied) simply typed lambda calculus in the style of [Pearlmutter and Siskind 2008] and we prove for the first time its soundness. To give an efficient yet principled implementation of the AD algorithm we define a sound and complete representation of hierarchical string diagrams as a class of hierarchical hypergraphs we call hypernets.

Combinatory Adjoints and Differentiation

We develop a compositional approach for automatic and symbolic differentiation based on categorical constructions in functional analysis where derivatives are linear functions on abstract vectors rather than being limited to scalars, vectors, matrices or tensors represented as multi-dimensional arrays. We show that both symbolic and automatic differentiation can be performed using a differential calculus for generating linear functions representing Fréchet derivatives based on rules for primitive, constant, linear and bilinear functions as well as their sequential and parallel composition. Lin…