# 高阶语言的变化理论 —— 通过静态微分增量化 λ-演算

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

Yufei Cai, Paolo G. Giarrusso, Tillmann Rendel, Klaus Ostermann

*Philipps-Universität Marburg*

*Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '14)*, Edinburgh, United Kingdom, June 2014

原文 DOI：<https://doi.org/10.1145/2594291.2594304>

---

## 译者说明

- 本文是上述论文正文（Abstract、§1–§6、致谢）的中文全译，段落与原文逐段对应，章节编号与原文一致；References 未翻译。
- 版权归原作者与 ACM 所有；本译文仅供学习研究使用。
- **底本**：ACM 正式版 PDF（11 页，经由 Zenodo 存档 `zenodo.org/records/14574026` 获取，DOI 与出版信息一致）。
  另参考 arXiv:1312.0658 的 **LaTeX 源码**还原被 PDF 提取破坏的公式；两版有个别措辞差异（例如 arXiv 版把 §4.5 拆成 "Benchmarks" 与 "Experimental results"），正文一律以 ACM 正式版为准。
- **关于图**：原文的 Figure 1–4 是推理规则/类型规则（TikZ + mathpartir 排版），这类内容用 LaTeX 重排比截图更清晰、可复制、可检索，因此译文中以 LaTeX 逐条给出（`$\frac{\text{前提}}{\text{结论}}$` 形式），并保留原图号。Figure 5（λ-项直方图伪代码）与 Figure 6（bag/map 原语的 Scala 实现）是代码，按原文以代码块给出。只有 **Figure 7（性能结果图）**是从 PDF 裁剪的图像，见 `figures/fig7-performance.png`（矢量版：`figures/DBSP-ILC-矢量图.pdf`）。
- 公式为 LaTeX 记号，配套 `.html` 文件用浏览器打开即自动渲染（首次需联网加载 MathJax）。
- 定义、定理、引理、方程的编号沿用原文；文献引用编号 `[n]` 与原文一致。

### 原文疑似笔误的保留情况（译者注）

以下两处我们判断为原文笔误（PDF 与 arXiv 源码一致），为保持与原文一致**按原样翻译、未擅自改动**，特此标注：

1. §4.4 中 `foldBag` 关于 merge 的方程，原文印作
   $\mathrm{foldBag}\ g\ f\ (\mathrm{merge}\ b_1\ b_2) = \mathrm{foldBag}\ g\ f\ b_1 \oplus \mathrm{foldBag}\ g\ f\ b_1$，
   第二个加数按定义应为 $\mathrm{foldBag}\ g\ f\ b_2$。
2. §3.5 图 4(b) 中变化结构的加法下标写作 $\oplus_{A\to B}$、$\oplus_A$、$\oplus_B$，按上下文（$A$、$B$ 未在全文定义）应为
   $\oplus_{\sigma\to\tau}$、$\oplus_\sigma$、$\oplus_\tau$。

### 与 DBSP 论文的关系（译者附注）

本文提出的 **ILC（Incremental λ-Calculus）** 与同目录 `../dbsp-paper/` 里翻译的 DBSP 论文属于同一条研究脉络：
两者都主张「增量计算 = 求导」，都要求值上存在群/变化结构，都对程序做**静态**变换以得到导数。
ILC 处理的是**高阶**（一等函数、闭包）的简单类型 λ-演算，用「变化结构（change structure）」与「零变化即导数」给出规格，
并用 Agda 机器检验正确性；DBSP 则把同一思想推广到**流**与**任意递归**，并用 ℤ-集合把它落到关系数据库上。
DBSP 论文 §9（相关工作）里提到的 "Picallo 等人 [7]" 指的就是本文作者（Paolo G. Giarrusso 等）的这条工作线。

---

## 目录

- [摘要](#摘要)
- [关键词](#关键词)
- [CCS 分类](#ccs-分类)
- [1 引言](#1-引言)
- [2 变化理论](#2-变化理论)
  - [2.1 变化结构](#2-1-变化结构)
  - [2.2 函数变化](#2-2-函数变化)
  - [2.3 零变化即导数](#2-3-零变化即导数)
- [3 增量化 λ-演算](#3-增量化-λ-演算)
  - [3.1 变化类型与擦除的变化结构](#3-1-变化类型与擦除的变化结构)
  - [3.2 微分](#3-2-微分)
  - [3.3 证明的架构](#3-3-证明的架构)
  - [3.4 指称语义](#3-4-指称语义)
  - [3.5 变化语义](#3-5-变化语义)
  - [3.6 微分的正确性](#3-6-微分的正确性)
  - [3.7 插件](#3-7-插件)
- [4 实践中的微分](#4-实践中的微分)
  - [4.1 微分插件的作用](#4-1-微分插件的作用)
  - [4.2 预测零变化](#4-2-预测零变化)
  - [4.3 自维护性](#4-3-自维护性)
  - [4.4 案例研究](#4-4-案例研究)
  - [4.5 基准测试结果](#4-5-基准测试结果)
- [5 相关工作](#5-相关工作)
  - [5.1 动态方法](#5-1-动态方法)
  - [5.2 静态方法](#5-2-静态方法)
- [6 结论与未来工作](#6-结论与未来工作)
- [致谢](#致谢)

---

**面向高阶语言的变化理论——通过静态微分对 λ-演算做增量化**（A Theory of Changes for Higher-Order Languages — Incrementalizing λ-Calculi by Static Differentiation）

- Yufei Cai、Paolo G. Giarrusso、Tillmann Rendel、Klaus Ostermann
- Philipps-Universität Marburg

> **第 1 页侧栏（ACM 制品徽章）**：Consistent\* Complete\* Well Documented\* Easy to Reuse\* \*Evaluated\* PLDI\* Artifact\* AE
>
> 即：该制品在一致性（consistent）、完整性（complete）、文档完善（well documented）、易于复用（easy to reuse）四方面均获认可，并通过了 PLDI 制品评估（Artifact Evaluation, AE）。

## 摘要

如果一项昂贵计算的结果因输入的微小变化而失效，就应当增量地更新旧结果，而不是重新执行整个计算。我们通过程序的导数来对程序做增量化。导数把程序输入的变化直接映射为程序输出的变化，而无需重新执行原程序。我们给出一项把程序变换为其导数的程序变换，它完全静态、自动，支持一等函数，并且产生的导数可接受标准优化。

我们在一族简单类型 λ-演算上于 Agda 中证明该程序变换是正确的，该族演算以基本类型与原语为参数。一个精确的接口规定了增量化所选原语需要满足什么要求。

我们通过一个案例研究考察性能：我们在 Scala 中实现该程序变换与一个插件，并把一个非平凡程序的性能提升了好几个数量级。

## 关键词

增量计算、一等函数、性能、Agda、形式化

## CCS 分类

**Categories and Subject Descriptors**：D.1.1 [程序设计技术（Programming Techniques）]：应用式（函数式）编程（Applicative (Functional) Programming）；D.3.3 [程序设计语言（Programming Languages）]：语言构造与特性（Language Constructs and Features）；D.3.4 [程序设计语言（Programming Languages）]：处理器——优化（Processors—Optimization）

> **ACM 版权行**：允许出于个人或课堂使用之目的，对本作品的全部或部分内容制作数字或硬拷贝，无需付费，前提是副本不用于营利或商业优势，且副本须保留本声明与首页的完整引用信息。本作品中由作者之外的他人拥有的组成部分，其版权须予以尊重。允许带出处标注的摘要式使用。以其他方式复制、再出版、在服务器上发布或再分发给邮件列表，均须事先获得专门许可和/或付费。许可申请请联系 permissions@acm.org。
>
> PLDI '14，2014 年 6 月 9–11 日，英国爱丁堡。
> 版权由作者所有。出版权授予 ACM。
> ACM 978-1-4503-2784-8/14/06 ... \$15.00
> http://dx.doi.org/10.1145/2594291.2594304

## 1 引言

增量计算在计算机科学中有着悠久的历史 [21]。程序常常需要高效地更新其输出，以反映输入的变化 [23]。增量计算研究并不在更新后的输入上从头重跑这样的程序，而是寻找在常见情形下更廉价的替代方案：即输入变化远小于输入本身的情形。

例如，考虑 `grand_total` 程序，它计算集合（collection）`xs`、`ys` 中所有数字之和。

```
grand_total = λxs. λys. fold (+) 0 (merge xs ys)
output = grand_total {{1, 1}} {{2, 3, 4}} = 11
```

我们用 $\{\!\{\ldots\}\!\}$ 表示多重集（multiset）或 bag，即一种无序集合（类似于集合），其中元素允许出现多次（这一点与集合不同）。现在假设输入 `xs` 从 $\{\!\{1,1\}\!\}$ 变为 $\{\!\{1\}\!\}$，而 `ys` 从 $\{\!\{2,3,4\}\!\}$ 变为 $\{\!\{2,3,4,5\}\!\}$。与其从头重新计算 `output`，我们也可以增量地计算它。如果我们有办法表示输入的变化（例如 `dxs` = $\{\!\{\mathbf{remove}\ 1\}\!\}$、`dys` = $\{\!\{\mathbf{add}\ 5\}\!\}$），就可以通过一个函数 `grand_total′` 来计算新结果：它接受旧输入 `xs` = $\{\!\{1,1\}\!\}$、`ys` = $\{\!\{2,3,4\}\!\}$ 以及变化 `dxs`、`dys`，产生输出的变化。在这个例子中，它算出的变化是 `grand_total′ xs dxs ys dys` = `plus 4`，这个变化随后可用于把原来的输出 11 更新为更新后的结果 15。我们把 `grand_total′` 称为 `grand_total` 的导数（derivative）。它是与 `grand_total` 同一门语言中的函数，接受并产生变化，而这些变化是该语言中普通的一等值。若增大原输入 `xs`、`ys` 的规模，`grand_total xs ys` 的时间复杂度线性增长，而 `grand_total′ xs dxs ys dys` 的时间复杂度只取决于 `dxs`、`dys` 的大小；无论在我们的例子中还是在一般情况下，这个大小都更小。

为了支持自动增量化，本文引入 ILC（incrementalizing λ-calculi）框架。我们定义一个自动的程序变换 $\mathcal{Derive}$，它对程序做微分，即计算程序的导数；$\mathcal{Derive}$ 保证

$$f\,(a \oplus da) \cong (f\,a) \oplus (\mathcal{Derive}(f)\,a\,da). \tag{1}$$

其中 $\cong$ 是指称相等（denotational equality），$da$ 是 $a$ 上的一个变化，$a \oplus da$ 表示用变化 $da$ 更新后的 $a$，也就是 $f$ 的更新后的输入。因此，我们可以通过把左边（从头重新计算输出）替换为右边（利用导数增量地计算输出）来优化程序。

ILC 基于一个以插件（plugin）为参数的简单类型 λ-演算。一个插件定义 (a) 基本类型与原语操作，以及 (b) 每个基本类型的变化表示，以及每个原语的增量版本。换言之，插件规定了原语及各自的导数，而 ILC 能够把这些简单的导数粘连起来，使得使用这些原语的任意简单类型 λ-演算表达式的导数都可以被计算出来。我们的实现与正确性证明都对插件是参数化的，因此支持（并证明其正确）新的插件很容易。

本文作出如下贡献：

- 我们提出一种新的变化与导数的数学理论，它比该领域的其他工作更为一般，因为变化是一等实体，它们与基本值不同，并且也为函数定义了变化（§2）。
- 我们提出第一种针对纯 λ-演算的增量计算方法，它通过源到源变换 $\mathcal{Derive}$ 实现，不需要任何运行时支持。该变换在同一种语言中产生增量程序；原程序的所有优化技术同样适用于增量程序。我们通过在 Agda [6] 中的机器检查形式化，证明我们的增量化变换 $\mathcal{Derive}$ 是正确的（式 (1)）。该证明揭示了 $\mathcal{Derive}$ 的定义思路：我们先构造一个简单类型 λ-演算项的指称语义的导数 $⟦-⟧^{\Delta}$，即其变化语义（change semantics）；然后说明 $\mathcal{Derive}$ 是由 $⟦-⟧^{\Delta}$ 擦除（erasing）为一个简单类型程序而得到的（§3）。
- 虽然我们主要关注变化与导数的理论，我们也进行了一项性能案例研究。我们在 Scala 中实现了求导变换，其插件式架构可以用新的基本类型与原语来扩展。我们定义了一个支持多种集合类型的插件，并用它来增量化一个 MapReduce 编程模型 [16] 的变体。基准测试表明，在这个程序上，增量化可以降低渐近复杂度，把 $O(n)$ 的性能变为 $O(1)$，在真实输入上把运行时间提高 4 个数量级以上（§4）。

我们的 Agda 形式化、Scala 实现与基准测试结果可在 http://inc-lc.github.io/ 获取。本文给出的所有引理与定理都已在 Agda 中证明。在本文中，我们以更易读的形式给出形式化的概览，并略过一些技术细节。

## 2 变化理论

本节引入变化（change）的形式化概念；这个概念已在式 (1) 中非形式地使用过，并且是我们方法的核心。我们先形式地定义变化结构（change structure），再为变化结构之间的函数构造变化结构，最后以一个把函数变化（function change）与导数联系起来的定理作结。

### 2.1 变化结构

考虑一个值的集合，例如自然数集合 $\mathbb{N}$。$v \in \mathbb{N}$ 的一个变化 $dv$ 应当描述 $v$ 与另一个自然数 $v_{new} \in \mathbb{N}$ 之间的差。我们不直接定义变化，而是规定那些必须在变化上定义的运算。它们是：

- 我们可以用一个变化 $dv$ 更新（update）一个基础值 $v$，得到更新后的、或称为*新*（new）的值 $v_{new}$。我们写作 $v_{new} = v \oplus dv$。
- 我们可以计算我们所考虑的集合中任意两个值 $v_{old}$ 与 $v_{new}$ 之间的变化。我们写作 $dv = v_{new} \ominus v_{old}$。

对自然数而言，通常用标准的减法与加法来描述变化。也就是说，对自然数我们可以定义 $v \oplus dv = v + dv$ 以及 $v_{new} \ominus v_{old} = v_{new} - v_{old}$。为了保证 $\oplus$ 与 $\ominus$ 总是有定义，我们需要仔细地定义变化的集合。$\mathbb{N}$ 太小，因为减法并不总产生一个自然数；整数集合 $\mathbb{Z}$ 则太大，因为把一个自然数与一个整数相加并不总产生一个自然数。事实上，我们无法对所有自然数使用同一个包含全部变化的集合。因此我们必须调整要求：对每个基础值 $v$，我们引入 $v$ 的一个变化集合 $\Delta v$，并要求 $v_{new} \ominus v_{old}$ 产生 $\Delta v_{old}$ 中的值，且 $v \oplus dv$ 对 $\Delta v$ 中的 $dv$ 有定义。对自然数 $v$，我们令 $\Delta v = \{\, dv \mid v + dv \ge 0 \,\}$；此时 $\oplus$ 与 $\ominus$ 就总是有定义。

下面的定义总结了到此为止的讨论：

**定义 2.1**（变化结构）：一个元组 $\widehat{V} = (V, \Delta, \oplus, \ominus)$ 是（$V$ 上的）一个变化结构，如果：

(a) $V$ 是一个集合，称为基础集合（base set）。
(b) 给定 $v \in V$，$\Delta v$ 是一个集合，称为变化集合（change set）。
(c) 给定 $v \in V$ 与 $dv \in \Delta v$，有 $v \oplus dv \in V$。
(d) 给定 $u, v \in V$，有 $u \ominus v \in \Delta v$。
(e) 给定 $u, v \in V$，$v \oplus (u \ominus v)$ 等于 $u$。

人们或许会期望再加一条假设：$(v \oplus dv) \ominus v = dv$。它虽然对 $\mathbb{N}$ 的变化结构成立，但一般并不需要。这意味着多个变化可以表示同一对基础值之间的差。贯穿我们的整个理论，我们只讨论基础值的相等，而不讨论变化的相等。

**记号** 我们重载运算符 $\Delta$、$\ominus$ 与 $\oplus$，使它们指代不同变化结构的相应运算；必要时我们会给这些符号加下标以免歧义。对任意 $\widehat{S}$，如上文那样，我们用 $S$ 表示它的第一个分量。我们令 $\oplus$ 左结合，即 $v \oplus dv_1 \oplus dv_2$ 表示 $(v \oplus dv_1) \oplus dv_2$。我们令函数应用的优先级高于 $\oplus$ 与 $\ominus$，即 $f\ a \oplus g\ a\ da$ 表示 $(f\ a) \oplus (g\ a\ da)$。

**例** 我们展示一个带符号重数的多重集（bag）上的变化结构 [15]。多重集是无序的汇集，其中每个元素可以出现整数次。

(a) 令 $S$ 为任意集合。基础集合 $V = \mathrm{Bag}\ S$ 是元素取自 $S$、带符号重数的多重集的集合。多重集 $\{\!\{1, 1, \overline{2}\}\!\}$ 含有两个 $1$ 的正出现与一个 $2$ 的负出现。
(b) 对每个多重集 $v \in V$，令变化集合 $\Delta v = V$。每个多重集都可以是任意其它多重集的变化。多重集 $\{\!\{1, 1, \overline{5}\}\!\}$ 表示两次插入 $1$ 与一次删除 $5$。
(c) 更新运算符是多重集合并：$\oplus = \mathrm{merge}$。两个多重集的合并是重数的逐元素和：

$$\mathrm{merge}\ \{\!\{\overline{1}, 2\}\!\}\ \{\!\{1, 1, \overline{5}\}\!\} = \{\!\{1, 2, \overline{5}\}\!\}.$$

(d) 令 $\mathrm{negate}$ 为对重数取负：

$$\mathrm{negate}\ \{\!\{1, 1, \overline{5}\}\!\} = \{\!\{\overline{1}, \overline{1}, 5\}\!\}.$$

要计算两个多重集的差，就把一个多重集与取负后的多重集合并：

$$u \ominus v = \mathrm{merge}\ u\ (\mathrm{negate}\ v).$$

(e) 给定上述 $\oplus$ 与 $\ominus$ 的定义，不难证明对所有多重集 $u, v \in V$ 有 $v \oplus (u \ominus v) = u$。

我们刚才描述的变化结构可以简洁地写作 $\widehat{\mathrm{Bag}}\ S = (\mathrm{Bag}\ S,\ (\lambda v.\ \mathrm{Bag}\ S),\ \mathrm{merge},\ (\lambda x\, y.\ \mathrm{merge}\ x\ (\mathrm{negate}\ y)))$。

这个变化结构是一般构造的一个实例：我们可以从任意的阿贝尔群构造出一个变化结构。阿贝尔群是一个元组 $(G, \boxplus, \boxminus, e)$，其中 $\boxplus$ 是一个可交换且可结合的二元运算，$e$ 是它的单位元，而 $\boxminus$ 产生 $G$ 中元素 $g$ 的逆元，使得 $(\boxminus g) \boxplus g = g \boxplus (\boxminus g) = e$。例如，整数（与自然数不同）构成阿贝尔群 $(\mathbb{Z}, +, -, 0)$（其中 $-$ 表示一元负号）。每个阿贝尔群 $(G, \boxplus, \boxminus, e)$ 都诱导出一个变化结构，即 $(G, \lambda g.\ G, \boxplus, \lambda g\, h.\ g \boxplus (\boxminus h))$，其中任意 $g \in G$ 的变化集合都是整个 $G$。不过，正如自然数的例子所说明的，变化结构更加一般。若 $\varnothing$ 表示空多重集，则 $(\mathrm{Bag}\ S, \mathrm{merge}, \mathrm{negate}, \varnothing)$ 是一个阿贝尔群，它诱导出我们刚才看到的变化结构。

整数上的阿贝尔群也在整数上诱导出一个变化结构，即 $\widehat{\mathbb{Z}} = (\mathbb{Z}, (\lambda v.\ \mathbb{Z}), +, -)$。

**零变化与导数** 一种特别重要的变化是一个值的零变化（nil change）：

**定义 2.2**（零变化）：给定变化结构 $\widehat{V}$ 与值 $v \in V$，变化 $v \ominus v$ 就是 $v$ 的零变化。

$$\mathbf{0}_v = v \ominus v$$

值的零变化确实不改变它。

**引理 2.3**（$\mathbf{0}$ 的行为）：给定变化结构 $\widehat{V}$ 与值 $v \in V$，有 $v \oplus \mathbf{0}_v = v$。

在定义了变化结构之后，我们可以重新陈述式 (1) 中导数的定义。

**定义 2.4**（导数）：给定变化结构 $\widehat{A}$ 与 $\widehat{B}$，以及这些变化结构的变化集合上的一个函数 $f \in A \to B$，若对所有的值 $a \in A$ 与相应的变化 $da \in \Delta_A a$ 都有

$$f\ (a \oplus da) = f\ a \oplus f'\ a\ da,$$

则称二元函数 $f'$ 是 $f$ 的*导数*（derivative）。

把一个导数作用于一个值及其零变化，得到的是一个零变化。

**引理 2.5**（导数在 $\mathbf{0}$ 上的行为）：给定变化结构 $\widehat{A}$ 与 $\widehat{B}$、函数 $f \in A \to B$、$A$ 中的元素 $a$，以及 $f$ 的导数 $f'$，我们有 $f'\ a\ \mathbf{0}_a = \mathbf{0}_{(f\ a)}$。

**例** 令 $f : \mathrm{Bag}\ S \to \mathrm{Bag}\ S$ 为把一切都映射到空多重集的常函数。它的导数 $f' : \mathrm{Bag}\ S \to \mathrm{Bag}\ S \to \mathrm{Bag}\ S$ 必须忽略它的两个参数，并且在所有情形下都产生空多重集。

令 $id : \mathrm{Bag}\ S \to \mathrm{Bag}\ S$ 为多重集之间的恒等函数。它的导数 $id'$ 定义为 $id'\ v\ dv = dv$。

### 2.2 函数变化

允许值发生变化是有用的，但我们还需要让函数也能发生变化。要理解原因，请考虑柯里化函数 `grand_total`：它把 `xs` 映射为一个“知道 `xs` 的值”的函数值（闭包）。它的导数 `grand_total′` 应当满足

$$\texttt{grand\_total}\ (xs \oplus dxs) = \texttt{grand\_total}\ xs \oplus \texttt{grand\_total}'\ xs\ dxs.$$

也就是说，`grand_total′` 必须把 `xs` 及其变化映射为一个闭包的变化；用这个变化更新该闭包所得到的结果，必须与 `grand_total (xs ⊕ dxs)` 相同，也就是一个知道 `xs ⊕ dxs` 的值的闭包。类似地，既然 λ-演算的函数也可以把其它函数作为参数，导数就可以把函数变化作为参数。

本节我们将说明：在假定 $A$ 与 $B$ 的变化结构已给定的前提下，如何为函数 $f \in A \to B$ 构造变化结构。

**定义** 如前所述，$f$ 的导数计算的是当 $a$ 变为 $a \oplus da$ 时 $f\ a$ 的变化。然而 $f$ 本身也可以变化：正如我们将在 §3.2 看到的，要增量化一次函数应用 $f\ a$，我们需要计算 $(f \oplus df)\ (a \oplus da) \ominus f\ a$ 而不重新运行 $(f \oplus df)\ (a \oplus da)$。我们用函数变化来计算这个差，而之所以精确地在函数上定义变化结构，正是为了使这件事成为可能。函数变化 $df$ 必须是一个满足 $f\ a \oplus df\ a\ da = (f \oplus df)\ (a \oplus da)$ 的函数（定理 2.9）！然而 $f \oplus df$ 目前还无法定义，于是我们施加一项要求（性质 2.6b），稍后我们将说明它与定理 2.9 等价。

**定义 2.6**：给定变化结构 $\widehat{A}$ 与 $\widehat{B}$ 以及 $f \in A \to B$，集合 $\Delta_{A \to B} f$ 包含所有满足下列条件的二元函数 $df$：

(a) $df\ a\ da \in \Delta_B (f\ a)$，且
(b) $f\ a \oplus df\ a\ da = f\ (a \oplus da) \oplus df\ (a \oplus da)\ \mathbf{0}_{(a \oplus da)}$

其中 $a \in A$ 取遍所有值，$da \in \Delta_A a$ 取遍相应的变化。

**例** 设 $f \in \mathrm{Bag}\ S \to \mathrm{Bag}\ S$，并考虑变化集合 $\Delta_{A \to B} f$ 的一个成员 $df$。条件 (a) 说明 $df$ 应把一个多重集与一个多重集变化映射为另一个多重集变化。条件 (b) 要求 $df$ 模仿 $f$ 的增量式行为。合起来，它们把我们视为对 $f$ 的恰当增量调整编码了下来。

特别地，同一类型的不同函数可以有不同变化集合。考虑两个类型为 $\mathrm{Bag}\ S \to \mathrm{Bag}\ S$ 的函数。

$$f\ x = \varnothing \qquad\qquad id\ x = x$$

集合 $\Delta_{\mathrm{Bag}\ S \to \mathrm{Bag}\ S} f$ 包含对 $f$ 的“变化”，即所有满足 (b) 的二元多重集函数 $df$：$df\ a\ da = df\ (a \oplus da)\ \mathbf{0}_{(a \oplus da)} = df\ (\mathrm{merge}\ a\ da)\ \varnothing$。这样的二元函数包括 $\mathrm{merge}$ 以及所有常函数。

集合 $\Delta_{\mathrm{Bag}\ S \to \mathrm{Bag}\ S} id$ 包含对 $id$ 的变化，即所有满足 (b) 的二元多重集函数 $did$：$id\ a \oplus did\ a\ da = id\ (a \oplus da) \oplus did\ (a \oplus da)\ \mathbf{0}_{(a \oplus da)}$，它化简为 $\mathrm{merge}\ a\ (did\ a\ da) = \mathrm{merge}\ (\mathrm{merge}\ a\ da)\ (did\ (\mathrm{merge}\ a\ da)\ \varnothing)$。$\mathrm{merge}$ 与任何常函数都不是 $id$ 的变化，但函数 $did\ a\ da = \mathrm{merge}\ da\ \{\!\{1, 2\}\!\}$ 是。

函数上的变化结构运算现在可以类似一条分配律来定义。

**定义 2.7**（函数变化上的运算）：给定变化结构 $\widehat{A}$ 与 $\widehat{B}$，运算 $\oplus_{A \to B}$ 与 $\ominus_{A \to B}$ 定义如下。

$$(f \oplus_{A \to B} df)\ v = f\ v \oplus_B df\ v\ \mathbf{0}_v$$

$$(f_2 \ominus_{A \to B} f_1)\ v\ dv = f_2\ (v \oplus_A dv) \ominus_B f_1\ v$$

所有这些定义都是经过仔细设置的，以确保我们实际上把变化结构提升到了函数空间上。

**定理 2.8** 给定变化结构 $\widehat{A}$ 与 $\widehat{B}$，元组 $(A \to B, \Delta_{A \to B}, \oplus_{A \to B}, \ominus_{A \to B})$ 是一个变化结构，我们把它记作 $\widehat{A} \to \widehat{B}$。

在定义了这个变化结构之后，我们就可以谈论 $f \oplus df$。于是我们可以重新陈述性质 2.6b，以说明函数变化 $df$ 对输入变化 $da$ 的响应方式与 $f$ 的增量版本相同，也就是说，$df\ a\ da$ 计算的是从 $f\ a$ 到 $(f \oplus df)\ (a \oplus da)$ 的变化：

**定理 2.9**（增量化）：给定变化结构 $\widehat{A}$ 与 $\widehat{B}$、函数 $f \in A \to B$、值 $a \in A$，以及相应的变化 $df \in \Delta_{A \to B} f$ 与 $da \in \Delta_A a$，我们有

$$(f \oplus df)\ (a \oplus da) = f\ a \oplus df\ a\ da.$$

例如，把

$$\mathbf{app} = \lambda f.\ \lambda x.\ f\ x$$

对输入变化 $df$、$dx$ 增量化，就等于在原来的第二个参数 $x_{old}$ 与变化 $dx$ 上调用 $df$。换句话说，把 $\mathbf{app}$ 增量化得到 $\lambda f.\ \lambda df.\ \lambda x.\ \lambda dx.\ df\ x\ dx$。

**理解函数变化** 为了理解函数变化，我们可以把它们分解为两个正交的概念。借助一个函数变化 $df$，我们可以一次计算出 $df\ a_{old}\ da$，即 $(f \oplus df)\ (a \oplus da)$ 与 $f\ a$ 之间的差，即使函数与其参数都在变化。但这两个变化的效果可以分别描述。我们可以用 $f$ 的导数 $f'$ 来刻画 $a$ 的变化：$f\ (a \oplus da) \ominus f\ a = f'\ a\ da$。我们可以用两个函数的逐点差 $\nabla f = \lambda a.\ (f \oplus df)\ a \ominus f\ a$ 来刻画 $f$ 的变化；特别地，$(f \oplus df)\ (a \oplus da) \ominus f\ (a \oplus da) = \nabla f\ (a \oplus da)$。再借助增量化定理，我们就可以说明函数变化不过是一个导数与一个逐点变化的组合：

$$\mathit{fold}\ a_{old} \oplus df\ a_{old}\ da = \mathit{fold}\ a_{old} \oplus f'\ a_{old}\ da \oplus \nabla f\ a_{new}$$

我们也可以从一个函数变化计算出一个逐点变化：

$$f\ a \oplus df\ a\ \mathbf{0}_a = f\ a \oplus \nabla f\ a$$

**图 1**：我们的基础演算。（原图见 PDF 第 4 页）

**（a）语法。** 基本类型、类型、类型上下文、常量与项的语法如下。

| 语法范畴 | 产生式 |
|---|---|
| 基本类型 | $\iota ::= \ldots$ |
| 类型 | $\sigma, \tau ::= \iota \mid \tau \to \tau$ |
| 类型上下文 | $\Gamma ::= \varepsilon \mid \Gamma, x : \tau$ |
| 常量 | $c ::= \ldots$ |
| 项 | $s, t ::= c \mid \lambda x.\ t \mid t\ t \mid x$ |

**（b）类型规则。** 常量、变量、λ-抽象与应用的类型规则如下。

$$\frac{\ldots}{\vdash c : \tau}\;\mathrm{Const}$$

$$\Gamma_1, x : \tau, \Gamma_2 \vdash x : \tau \qquad \mathrm{Lookup}$$

$$\frac{\Gamma, x : \sigma \vdash t : \tau}{\Gamma \vdash \lambda x.\ t : \sigma \to \tau}\;\mathrm{Lam}$$

$$\frac{\Gamma \vdash s : \sigma \to \tau \qquad \Gamma \vdash t : \sigma}{\Gamma \vdash s\ t : \tau}\;\mathrm{App}$$

ILC 基于函数变化而不是逐点变化，因为函数变化接收到的信息严格多于逐点变化，因而更易于优化。

### 2.3 零变化即导数

定理 2.9 告诉我们一个增量程序可以采取的形式。如果 $df$ 根本没有改变 $f$，即如果 $f \oplus df = f$，那么定理 2.9 就变成

$$f\ (a \oplus da) = f\ a \oplus df\ a\ da.$$

它说明：在给定对 $f$ 的输入 $a$ 的一个变化 $da$ 的情况下，$df$ 计算的是 $f$ 的输出上的变化。换句话说，一个函数的零变化正好就是它的导数（见定义 2.4）：

**定理 2.10**（零变化即导数）：给定变化结构 $\widehat{A}$ 与 $\widehat{B}$ 以及函数 $f \in A \to B$，变化 $\mathbf{0}_f$ 就是 $f$ 的导数 $f'$。

本节中，我们发展变化理论，是为了形式地定义什么是导数（定义 2.4），并且认识到：为了求一个函数的导数，我们只需找出它的零变化（定理 2.10）。接下来，我们希望提供一种完全自动的方法，用于找出给定函数的零变化。

## 3 增量化 λ-演算

本节我们展示如何增量化简单类型 λ-演算中的任意程序。为此，我们定义源到源的变换 $\mathrm{Derive}$。利用我们稍后（在 §3.4）定义的指称语义 $⟦ - ⟧$，我们可以刻画 $\mathrm{Derive}$ 的预期行为：为保证式 (1) 成立，对任意闭项 $f : A \to B$，$⟦ \mathrm{Derive}(f) ⟧$ 必须是 $⟦ f ⟧$ 的导数。我们将重载“导数”一词，简单地说 $\mathrm{Derive}(f)$ 就是 $f$ 的导数。

把任意函数的导数定义为下式是容易的：

$$f'\ x\ dx = f\ (x \oplus dx) \ominus f\ x.$$

我们可以按同样的策略实现 $\mathrm{Derive}$。然而，由此得到的增量程序并不会比重新计算更快。对任意数学函数我们无法做得更好，因为它们是我们无法完全检视的无穷对象。因此，我们诉诸于对按图 1 定义的简单类型 λ-演算做源到源变换。本节我们关注所有插件接口实例所共有的那些特性的增量化，即函数类型与相关的语法形式：λ-抽象、应用与变量引用。

基本类型与原始常量的集合，以及原始常量的类型规则，被有意地不加指定，而只由插件定义——它们是扩展点。

定义不同的插件使我们能够试验不同的基本类型集合、相关原语与增量化策略。我们在 §3.7 中汇总对插件的要求：满足这些要求就足以保证正确的增量化。我们在案例研究（§4.4）中展示一个示例插件。

### 3.1 变化类型与擦除的变化结构

我们在上一节发展变化结构理论，是为了指导 $\mathrm{Derive}$ 的实现。由定理 2.10，$\mathrm{Derive}$ 只需找出程序自身的零变化，因为零变化*就是*导数。然而，变化结构理论不能直接应用于简单类型 λ-演算，因为变化结构的精确实现需要依赖类型。例如，我们无法把变化集合 $\Delta\tau\,v$ 精确地描述为一个非依赖类型，因为它依赖于我们计划用这些变化去更新的那个值。

为了绕开我们对象语言的这一局限，我们使用一种把依赖类型擦除为简单类型的形式。在图 2 与图 4(a) 中，我们把变化类型 $\Delta\tau$ 定义为对变化集合 $\Delta\tau\,v$（图 4(b)）的近似描述。特别地，$\Delta\tau\,v$ 中的所有变化都对应类型为 $\Delta\tau$ 的项的值，但反过来不一定成立。例如，在 §2.1 描述的自然数的变化结构中，我们会有 $\Delta\mathbf{Nat} = \mathbf{Int}$，尽管并非每个整数都是每个自然数的变化。对于基本类型 $\iota$，$\Delta\iota$ 及其关联的 $\oplus$ 与 $\ominus$ 算子必须由插件开发者提供。对于函数类型，擦除的变化结构由图 3 给出。把变化结构所有成分中的依赖类型都擦除，我们就得到*擦除的变化结构*，它把变化结构表示为简单类型 λ-项，其中 $\oplus$ 与 $\ominus$ 是 λ-项的族。

**图 2**：简单类型上的擦除的变化结构。（原图见 PDF 第 4 页）

| 记号 | 类型 | 含义 |
|---|---|---|
| $\Delta$ | $* \to *$ | 变化的类型 |
| $\oplus$ | $\tau \to \Delta\tau \to \tau$ | 用一个变化更新一个值 |
| $\ominus$ | $\tau \to \tau \to \Delta\tau$ | 两个值之间的变化 |

**图 3**：函数类型的擦除的变化结构。（原图见 PDF 第 4 页）

$$\Delta(\sigma \to \tau) = \sigma \to \Delta\sigma \to \Delta\tau$$

$$\ominus_{\sigma \to \tau} = \lambda g\, f\, x\, dx.\ (g\,(x \oplus dx)) \ominus (f\, x)$$

$$\oplus_{\sigma \to \tau} = \lambda f\, df\, x.\ (f\, x) \oplus (df\, x\, (x \ominus x))$$

**图 4**：简单类型 λ-演算的标准行为与微分行为。左列把微分定义为源到源的变换；右列定义简单类型 λ-演算的标准语义；中列通过一个微分语义把这两者连接起来，该语义把 λ-项映到其标准语义的导数。（原图见 PDF 第 6 页）

图 4(a) 变化类型：

$$\Delta\iota = \ldots \qquad\qquad \Delta(\sigma \to \tau) = \sigma \to \Delta\sigma \to \Delta\tau$$

图 4(b) 变化值：

$$\Delta\iota\,v = \ldots \subseteq ⟦ \Delta\iota ⟧$$

$$\Delta(\sigma \to \tau)\,f = \{\, df \in (x : ⟦ \sigma ⟧) \to \Delta\sigma\,x \to \Delta\tau\,(f\,x) \mid (f \oplus_{A \to B} df)\,(a \oplus_A da) = f\,a \oplus_B df\,a\,da \,\}$$

图 4(d) 变化上下文：

$$\Delta\varepsilon = \varepsilon \qquad\qquad \Delta(\Gamma, x : \tau) = \Delta\Gamma,\ dx : \Delta\tau$$

图 4(g) 微分（求导）：

$$\mathrm{Derive}(c) = \ldots$$

$$\mathrm{Derive}(\lambda x.\ t) = \lambda x\, dx.\ \mathrm{Derive}(t)$$

$$\mathrm{Derive}(s\, t) = \mathrm{Derive}(s)\, t\, \mathrm{Derive}(t)$$

$$\mathrm{Derive}(x) = dx$$

擦除的变化结构本身并不是变化结构。不过，我们将说明变化结构与擦除的变化结构具有“几乎相同”的行为（§3.6）。因此我们将能够应用我们的变化理论。

### 3.2 微分

当 $f$ 是函数类型的闭项时，$\mathrm{Derive}(f)$ 应当是其导数，即其零变化。由于 $\mathrm{Derive}$ 在开项上递归，我们需要一个更一般的刻画。我们要求：若 $\Gamma \vdash t : \tau$，则 $\mathrm{Derive}(t)$ 表示 $t$ 的变化（类型为 $\Delta\tau$），且该变化以 $t$ 的自由变量取值的变化为参照。作为一个特例，当 $t$ 是闭项时，没有自由变量可以变化；因此 $t$ 的变化将如所愿地是 $t$ 的零变化。

下面的类型规则给出 $\mathrm{Derive}$ 的静态语义：

$$\frac{\Gamma \vdash t : \tau}{\Gamma, \Delta\Gamma \vdash \mathrm{Derive}(t) : \Delta\tau}\;\mathrm{Derive}$$

我们看到，$\mathrm{Derive}(t)$ 既能访问 $t$ 中的自由变量（来自 $\Gamma$），也能访问它们的变化（来自 $\Delta\Gamma$，定义于图 4(d)）。例如，若良类型的项 $t$ 含有自由变量 $x$，则 $\Gamma$ 含有某个 $\tau$ 的假设 $x : \tau$，而 $\Delta\Gamma$ 含有相应的假设 $dx : \Delta\tau$。因此，$\mathrm{Derive}(t)$ 可以通过使用 $dx$ 访问 $x$ 的变化。为简单起见，我们假设原程序中不含以 $d$ 开头的变量名。$\mathrm{Derive}$ 的定义将保证：若原项是闭的，则 $dx$ 这类变量都被绑定。

我们来分析 $\mathrm{Derive}(u)$ 的定义（图 4(g)）的各个情形：

- 若 $u = x$，则 $\mathrm{Derive}(x)$ 必须是 $x$ 的变化，即 $dx$。
- 若 $u = \lambda x.\ t$，则 $\mathrm{Derive}(t)$ 是在给定其自由变量变化的情形下 $u$ 的变化。$u$ 的变化于是就是 $t$ 作为基础输入 $x$ 及其变化 $dx$ 的函数、相对于其它开变量的变化所发生的变化。因此，我们只需绑定 $dx$，定义 $\mathrm{Derive}(\lambda x.\ t) = \lambda x.\ \lambda dx.\ \mathrm{Derive}(t)$。
- 若 $u = s\, t$，则 $\mathrm{Derive}(s)$ 是 $s$ 作为其基础输入与变化的函数的变化。因此，我们只需把 $\mathrm{Derive}(s)$ 应用于实际的基础输入 $t$ 与变化 $\mathrm{Derive}(t)$，得到 $\mathrm{Derive}(s\, t) = \mathrm{Derive}(s)\, t\, \mathrm{Derive}(t)$。
- 若 $t = c$：由于 $c$ 是闭项，其变化是零变化，从而是（由定理 2.10）$c$ 的导数。我们可以通过令 $\mathrm{Derive}(c) = c \ominus c = \mathbf{0}_c = c'$ 成立来为常量获得正确的导数。该定义对函数型常量效率低下；因此插件必须为其定义的原语提供导数。

这看起来可能简单得具有欺骗性。但 λ-演算只实现值的绑定，把“真正的工作”留给原语；同样，λ-演算的微分只实现变化的绑定，把“真正的工作”留给原语的导数。不过，我们对 λ-演算的支持允许把原语*粘*在一起。

**例** 我们把这个变换应用于 §1 中定义的 `grand_total` 程序。

```
grand_total = λxs. λys. fold (+) 0 (merge xs ys)

Derive(grand_total) =
  λxs. λdxs. λys. λdys.
    fold′ (+) (+′) 0 0′
      (merge xs ys)
      (merge′ xs dxs ys dys)
```

名字 `fold′`、`merge′`、`+′`、`0′` 分别表示相应原语的导数。变量 `dxs` 与 `dys` 依照 `xs` 与 `ys` 系统地命名，用来表示它们的变化。正如我们将在 §3.7 看到的，

```
merge′ = λu. λdu. λv. λdv. merge du dv,
```

所以 `grand_total` 的导数 β-等价于

```
λxs. λdxs. λys. λdys.
  fold′ (+) (+′) 0 0′
    (merge xs ys) (merge dxs dys).
```

这个导数效率低下，因为它不必要地重新计算了 `merge xs ys`。但我们仍需内联 `fold` 与其它原语的导数才能完成求导。我们将在 §4.3 完成求导过程，并说明如何避免这种浪费。

我们现在已经从 $\mathrm{Derive}$ 的刻画（式 (1)）与其类型出发，非形式地推导出了 $\mathrm{Derive}$ 的定义（图 4(g)）。但严格说来，$\mathrm{Derive}$ 是一个定义。因此在本节余下部分，我们必须证明 $\mathrm{Derive}$ 满足式 (1)。

### 3.3 证明的架构

$\mathrm{Derive}(t)$ 是借助变化类型定义的。正如 §3.1 所讨论的，变化类型对其成员施加的限制比相应的变化结构更少——它们包含“垃圾”（例如对自然数 3 而言的变化 $-5$）。我们无法约束 $\mathrm{Derive}(t)$ 在这类垃圾上的行为；直接的正确性证明会失败。为避免这个问题，我们的证明定义了一个改用变化结构的 $\mathrm{Derive}$ 版本。

为此，我们首先给出简单类型 λ-演算的标准指称语义 $⟦ - ⟧$。利用我们的变化理论，我们把变化结构关联到各个论域上。我们定义一个非标准的指称语义 $⟦ - ⟧^{\Delta}$，它类比于 $\mathrm{Derive}$，但在变化结构的元素上运作，从而无需处理垃圾。于是我们可以证明 $⟦ t ⟧^{\Delta}$ 是 $⟦ t ⟧$ 的导数：这是我们的关键结果。

最后，我们定义变化集合与和变化类型相关联的论域之间的对应关系，并说明：每当 $⟦ t ⟧^{\Delta}$ 在某个输入上具有某种行为时，$⟦ \mathrm{Derive}(t) ⟧$ 在对应输入上具有相应的行为。我们的正确性性质作为推论随之成立。

### 3.4 指称语义

为了证明增量化保持项的含义，我们为对象语言定义一种指称语义。我们首先在插件所提供的基本类型域的基础上，为每个类型关联一个域。由于我们的演算是强规范化的且所有函数都是全函数，我们可以避免用域理论来建模部分性：我们的域就是集合。同样，我们可以用函数作为函数类型的域。

**定义 3.1**（域）：类型 $\tau$ 的域 $⟦\tau⟧$ 按图 4(c) 定义。

有了这种域的构造，我们现在可以为项定义求值函数。常量上的求值函数必须由插件提供。一般地，求值函数 $⟦ t⟧$ 在给定 $t$ 中所有自由变量的值的情况下，计算良类型项 $t$ 的值。自由变量的值由环境提供。

**定义 3.2**（环境）：环境 $\rho$ 为自由变量的名字指派值。

$$
\rho ::= \varepsilon \mid \rho, x = v
$$

我们用 $⟦\Gamma⟧$ 表示这样的环境的集合：它们为 $\Gamma$ 中绑定的名字指派值（见图 4(f)）。

**定义 3.3**（求值）：给定 $\Gamma \vdash t : \tau$，$t$ 的含义由图 4(i) 中类型为 $⟦\Gamma⟧ \to ⟦\tau⟧$ 的函数 $⟦ t⟧$ 定义。

这就是简单类型 λ-演算的标准语义。现在我们可以说明，相对这一语义对简单类型 λ-演算做增量化意味着什么。

**图 4**：简单类型 λ-演算的标准行为与微分行为。左栏把微分定义为一个源到源的变换。右栏定义简单类型 λ-演算的标准语义。中栏通过一个微分语义把这两者连接起来，该语义把 λ-项映射到其标准语义的导数。（原图为 3 栏 × 3 行的网格，子图编号为 (a)–(i)；下文按左、中、右三栏依次列出。原图见 PDF 第 6 页）

**左栏：微分（源到源的变换）**

(a) 变化类型

$$
\begin{aligned}
\Delta\iota &= \ldots\\
\Delta(\sigma \to \tau) &= \sigma \to \Delta\sigma \to \Delta\tau
\end{aligned}
$$

(d) 变化上下文

$$
\begin{aligned}
\Delta\varepsilon &= \varepsilon\\
\Delta(\Gamma, x{:}\tau) &= \Delta\Gamma, dx : \Delta\tau
\end{aligned}
$$

(g) 微分

$$
\begin{aligned}
\mathcal{Derive}(c) &= \ldots\\
\mathcal{Derive}(\lambda x.\, t) &= \lambda x\, dx.\ \mathcal{Derive}(t)\\
\mathcal{Derive}(s\ t) &= \big(\mathcal{Derive}(s)\ t\big)\ \mathcal{Derive}(t)\\
\mathcal{Derive}(x) &= dx
\end{aligned}
$$

**中栏：变化值、变化环境与微分求值（变化语义）**

(b) 变化值，其中 $dv, df \in \Delta\tau\, v$

$$
\begin{aligned}
\Delta\iota\, v &= \ldots \subseteq ⟦ \Delta\iota ⟧\\
\Delta(\sigma \to \tau)\, f &= \Big\{\, df \in (x : ⟦\sigma⟧) \to \Delta\sigma\, x \to \Delta\tau\, (f\, x) \;\Big|\; \\
&\qquad (f \oplus_{A \to B} df)\ (a \oplus_A da) = (f\, a) \oplus_B (df\, a\ da) \,\Big\}
\end{aligned}
$$

(e) 变化环境，其中 $d\rho \in \Delta\Gamma\, \rho$；$\rho \in ⟦\Gamma⟧$

$$
\begin{aligned}
\Delta\varepsilon\, \emptyset &= \{\emptyset\}\\
\Delta(\Gamma, x{:}\tau)\, (\rho, x{=}v) &= \big\{\, (d\rho, dx{=}dv) \mid d\rho \in \Delta\Gamma\, \rho \;\wedge\; dv \in \Delta\tau\, v \,\big\}
\end{aligned}
$$

(h) 微分求值，其中 $⟦ t⟧^{\Delta} \rho\, d\rho$

$$
\begin{aligned}
⟦ c ⟧^{\Delta} \rho\, d\rho &= \ldots\\
⟦ \lambda x.\, t ⟧^{\Delta} \rho\, d\rho &= \lambda v\, dv.\ ⟦ t ⟧^{\Delta}\, (\rho, x{=}v)\ (d\rho, dx{=}dv)\\
⟦ s\ t ⟧^{\Delta} \rho\, d\rho &= \Big(\big(⟦ s ⟧^{\Delta} \rho\, d\rho\big)\ \big(⟦ t ⟧ \rho\big)\Big)\ \big(⟦ t ⟧^{\Delta} \rho\, d\rho\big)\\
⟦ x ⟧^{\Delta} \rho\, d\rho &= \mathit{lookup}\ dx\ \text{in}\ d\rho
\end{aligned}
$$

**右栏：标准值、标准环境与标准求值**

(c) 标准值，其中 $v, f \in ⟦\tau⟧$

$$
\begin{aligned}
⟦\iota⟧ &= \ldots\\
⟦\sigma \to \tau⟧ &= ⟦\sigma⟧ \to ⟦\tau⟧
\end{aligned}
$$

(f) 标准环境，其中 $\rho \in ⟦\Gamma⟧$

$$
\begin{aligned}
⟦\varepsilon⟧ &= \{\emptyset\}\\
⟦\Gamma, x{:}\tau⟧ &= \big\{\, (\rho, x{=}v) \mid \rho \in ⟦\Gamma⟧ \;\wedge\; v \in ⟦\tau⟧ \,\big\}
\end{aligned}
$$

(i) 标准求值，其中 $⟦ t⟧\, \rho$

$$
\begin{aligned}
⟦ c ⟧ \rho &= \ldots\\
⟦ \lambda x.\, t ⟧ \rho &= \lambda v.\ ⟦ t ⟧\, (\rho, x{=}v)\\
⟦ s\ t ⟧ \rho &= \big(⟦ s ⟧ \rho\big)\ \big(⟦ t ⟧ \rho\big)\\
⟦ x ⟧ \rho &= \mathit{lookup}\ x\ \text{in}\ \rho
\end{aligned}
$$

### 3.5 变化语义

微分的非形式化规定是：把程序输入的变化映射为程序输出的变化。为了用变化结构和对象语言的指称语义来形式化这一规定，我们现在为对象语言定义一种计算变化的非标准指称语义。求值函数 $⟦ t⟧^{\Delta}$ 在同时给定 $t$ 中所有自由变量的值和变化的情况下，计算良类型项 $t$ 的值如何变化。在没有任何自由变量发生变化的特殊情形下，$⟦ t⟧^{\Delta}$ 计算的是零变化。由定理 2.10 可知，这正是 $⟦ t⟧$ 的导数——它把 $⟦ t⟧$ 的输入变化映射为其输出变化，符合要求。

首先，我们为所有 $\tau$ 在 $⟦\tau⟧$ 上定义变化结构。这些变化结构的载体 $\Delta\tau$ 将充当变化语义的非标准域。插件在基本类型 $\iota$ 上提供一个变化结构 $\widehat{C}_{\iota}$，使得 $\forall v.\, \Delta\iota\, v \subseteq ⟦\Delta\iota⟧$。

**定义 3.4**（变化）：给定类型 $\tau$，我们按 $\tau$ 的结构归纳地为 $⟦\tau⟧$ 定义一个变化结构 $\widehat{C}_{\tau}$。若 $\tau$ 是基本类型 $\iota$，则结果 $\widehat{C}_{\iota}$ 由插件提供。否则我们使用定理 2.8 中的构造，定义

$$
\widehat{C}_{\sigma \to \tau} = \widehat{C}_{\sigma} \to \widehat{C}_{\tau}
$$

为了讨论 $⟦ t⟧$ 的导数，我们需要在它的域（即环境集合）上有一个变化结构。由于环境是（异质的）值列表，我们可以把变化结构上的运算逐点提升为环境上的变化结构。

**定义 3.5**（变化环境）：给定上下文 $\Gamma$，我们在相应的环境 $⟦\Gamma⟧$ 上定义变化结构 $\widehat{C}_{\Gamma}$，并在图 4(e) 中定义变化环境 $\Delta\Gamma\, \rho$。

运算 $\oplus_{\rho}$ 与 $\ominus_{\rho}$ 定义如下。

$$
\begin{aligned}
\varepsilon \oplus \varepsilon &= \varepsilon\\
(\rho, x{=}v) \oplus (d\rho, dx{=}dv) &= (\rho \oplus d\rho),\ x = (v \oplus dv)\\[2pt]
\varepsilon \ominus \varepsilon &= \varepsilon\\
(\rho_2, x{=}v_2) \ominus (\rho_1, x{=}v_1) &= (\rho_2 \ominus \rho_1),\ x = (v_2 \ominus v_1)
\end{aligned}
$$

定义 2.1 中的性质直接由底层变化结构 $\widehat{C}_{\tau}$ 的相应性质得到。

至此，我们可以定义项的变化语义，并证明 $⟦ t⟧^{\Delta}$ 是 $⟦ t⟧$ 的导数。对每个常量 $c$，插件提供 $⟦ c⟧^{\Delta}$，即 $⟦ c⟧$ 的导数。

**定义 3.6**（变化语义）：函数 $⟦ t⟧^{\Delta}$ 定义于图 4(h)。

**引理 3.7**：给定 $\Gamma \vdash t : \tau$，$⟦ t⟧^{\Delta}$ 是 $⟦ t⟧$ 的导数。

### 3.6 微分的正确性

现在我们可以证明 $⟦\mathcal{Derive}(t)⟧$ 的行为与 $⟦ t⟧^{\Delta}$ 的行为一致。由此我们得到引言中提到的正确性定理的证明。

擦除（erasure）这一逻辑关系（logical relation）[19, 第 8 章] 刻画了这样一个想法：变化结构中的一个元素，在我们从中抹去所有依赖类型的痕迹之后，几乎保持不变。

**定义 3.8**（擦除）：令 $dv \in \Delta\tau\, v$ 且 $dv' \in ⟦\Delta\tau⟧$。我们说 $dv$ 擦除为 $dv'$，记作 $dv \sim^{v}_{\tau} dv'$，如果下列之一成立：

(a) $\tau$ 是基本类型，且 $dv = dv'$。

(b) $\tau = \sigma_0 \to \sigma_1$，且对所有 $w$、$dw$、$dw'$，只要 $dw \sim^{w}_{\sigma_0} dw'$，就有 $(dv\ w\ dw) \sim^{v\,w}_{\sigma_1} (dv'\ w\ dw')$。

有时我们也会说 $dv \in \Delta\tau\, v$ 擦除为一个闭项 $dt : \Delta t$，此时我们指的是 $dv$ 擦除为 $(⟦ dt⟧\, \emptyset)$。[^1]

下面的引理精确说明我们所说的“几乎相同”是什么意思。

**引理 3.9**：假设 $dv \sim^{v}_{\tau} dv'$。若 $\oplus'$ 是 $\tau$ 的变化结构上更新算子 $\oplus$ 的擦除版本（3.1 节），则 $v \oplus dv = v \oplus' dv'$。

结果表明，$⟦ t⟧^{\Delta}$ 与 $\mathcal{Derive}(t)$“几乎相同”。对闭项，我们用下面的引理精确表述：

**引理 3.10**：若 $(t : \tau)$ 是闭项，则 $(⟦ t⟧^{\Delta}\, \emptyset\, \emptyset)$ 擦除为 $\mathcal{Derive}(t)$。

限于篇幅，我们省略引理 3.10 的一个更一般的版本：它对开项也成立，但需要在环境上定义擦除。主要的正确性定理是引理 3.7、3.9 与 3.10 的推论。

**定理 3.11**（微分的正确性）：令 $f : \sigma \to \tau$ 是函数类型的闭项。对每个闭的基本项 $s : \sigma$，以及每个闭的变化项 $ds : \Delta\sigma$，只要存在某个变化 $dv \in \Delta\sigma\, ⟦ s⟧$ 擦除为 $ds$，就有

$$
f\ (s \oplus ds) \;\cong\; (f\ s) \oplus \big(\mathcal{Derive}(f)\ s\ ds\big)
$$

其中 $\cong$ 是指称相等（$a \cong b$ 当且仅当 $⟦ a⟧ = ⟦ b⟧$）。

定理 3.11 是对等式 (1) 的更精确的重新表述。要求 $dv$ 存在，保证了 $ds$ 求值得到一个变化，而不是 $⟦\Delta\sigma⟧$ 中的垃圾。

### 3.7 插件

我们的正确性证明与微分框架（它是我们实现的基础）都对插件是参数化的。实例化微分框架需要一个微分插件；为它实例化正确性证明则需要一个证明插件，其中包含额外的定义与引理。

为了能够执行并微分 λ-项，微分插件必须提供：

- 基本类型，以及每个基本类型 $\iota$ 在 $\iota$ 上的擦除变化结构，如图 2 所规定；
- 原语，以及每个原语 $c$ 的项 $\mathcal{Derive}(c)$。

**示例**：以数字的多重集作为基本类型，并使用由 $\widehat{\mathit{Bag}}\ S$（定义于 2.1 节）擦除而来的变化结构，`merge` 的导数很容易写出：

$$
\mathcal{Derive}(\mathit{merge}) = \lambda u.\, \lambda du.\, \lambda v.\, \lambda dv.\, \mathit{merge}\ du\ dv
$$

换言之，两个多重集之 `merge` 的变化，就是各自变化之 `merge`。

对每个基本类型 $\iota$，证明插件必须提供：

- 一个语义域 $⟦\iota⟧$；
- 一个变化结构 $\widehat{C}_{\iota}$，使得 $\forall v.\, \Delta\iota\, v \subseteq ⟦\Delta\iota⟧$；
- 一个证明，说明 $\widehat{C}_{\iota}$ 擦除为微分插件中相应的擦除变化结构。

对每个原语 $c : \tau$，证明插件必须提供：

- 它在域 $⟦\tau⟧$ 中的值 $⟦ c⟧$；
- 它在 $\tau$ 的变化集中的导数 $(⟦ c⟧^{\Delta}\, \emptyset\, \emptyset)$[^1]；
- 一个证明，说明 $(⟦ c⟧^{\Delta}\, \emptyset\, \emptyset)$ 擦除为项 $\mathcal{Derive}(c)$。

为表明证明插件的接口是可以实现的，我们写了一个小的证明插件，包含整数与整数的多重集。为表明微分插件是切实可行的，我们实现了该变换以及一个微分插件，它能够对非平凡的程序做增量化。这将在下一节介绍。

[^1]: 为对一个闭项 $t$ 求值，我们不需要任何环境条目，因此空环境 $\emptyset$ 就足够了：$(⟦ t⟧\, \emptyset)$ 是 $t$ 在空环境中的值，$(⟦ t⟧^{\Delta}\, \emptyset\, \emptyset)$ 是 $t$ 在变化语义下、使用空环境和空变化环境时的值。

## 4 实践中的微分

在实践中，成功的增量化同时要求导数正确且高效。导数的正确性由前面各节的理论推导以及微分插件与证明插件的接口来保证，而导数的性能则必须来自对微分插件的精心设计与实现。

### 4.1 微分插件的作用

我们方法的用户需要：(1) 选定自己需要的基本类型与原语；(2) 为这些基本类型与原语实现合适的微分插件；(3) 用这些原语重写他们程序（的相关部分）；(4) 安排他们的程序以变化、而不是以更新后的输入作为输入来调用。

正如 3.2 节所讨论的，微分支持抽象、应用与变量；但由于基本类型上的计算是由针对这些类型的原语完成的，原语的高效导数对良好性能至关重要。

要使这样的导数高效，变化类型也必须有高效的实现，并且能够精确描述发生了什么变化。第 1 节中 sum 的高效导数之所以可能，只是因为多重集变化可以描述删除与插入，而整数变化可以描述加性差值。

对于许多可以设想的基本类型，我们不必从零开始设计微分插件。相反，我们可以复用一阶与领域特定场景下关于增量化的既有研究成果。例如，我们复用 Gluche 等人 [12] 的方法来支持增量式的多重集与映射。通过把一个领域特定的增量化结果包装进一个微分插件，我们使它能够用于高阶通用编程语言的语境中，并与该语言其他基本类型的其他微分插件协同工作。

对于没有已知增量化策略的基本类型，微分插件与证明插件的精确接口可以指导实现工作。这些接口也可以构成一个能良好协作的微分插件库的基础。

用我们的语言重写整个程序会是一个过分的要求。相反，我们把对象语言作为一个 EDSL 嵌入到某个更具表达力的元语言（在我们的案例研究中是 Scala）中，从而使嵌入的程序被具体化（reified）。可以设法让这种嵌入语言看起来与元语言相似 [22]。为了增量化计算中的某一部分，我们把它用嵌入的对象语言写出来，对嵌入的程序调用 Derive，可选地优化所得的程序，最后调用它们。元语言照例也充当对象语言的宏系统。这使我们能够模拟多态集合，例如 $(\mathrm{Bag}\ \iota)$，尽管对象语言是简单类型的；在技术上讲，我们的插件向对象语言暴露了一族基本类型。

### 4.2 预测零变化

处理所有输入上的变化会在增量程序中引入过多的开销 [2]。这通常也是不必要的；例如第 1 节中 fold 的函数参数不会变化，因为它是程序的一个闭子项，所以 fold 会收到它的一个零变化。一个（保守的）静态分析可以检测出在运行时保证为零的变化。我们于是可以特化接收这一变化的导数，使它们无需在运行时检查该变化。

在我们的案例研究中，我们实现了一个简单的静态分析，它检测并传播关于闭项的信息。这个分析本身并不有趣，由于篇幅所限我们省略其细节。

### 4.3 自维护性

在数据库中，自维护视图（self-maintainable view）[13] 是一个仅凭输入变化就能更新其结果、而不查看实际输入的函数。以此类推，如果一个导数不使用基参数、只使用它们的变化，我们就称它是**自维护的**（self-maintainable）。自维护的导数描述了高效的增量计算：由于它们不使用其基础输入，它们的运行时间不必依赖于输入规模。

**例子**：$\mathrm{Derive}(\mathrm{merge}) = \lambda x\ dx\ y\ dy.\ \mathrm{merge}\ dx\ dy$ 在 2.1 节所述的变化结构 $\widehat{\mathrm{Bag}\ S}$ 下是自维护的，因为该导数不使用基础输入 $x$ 与 $y$。其他导数只在特定上下文中才是自维护的。逐元素函数应用 $(\mathrm{map}\ f\ xs)$ 的导数在 $f$ 的变化始终为零时会忽略多重集 $xs$ 的原始值，因为此时底层的原语 foldBag 是自维护的（如下一节所讨论）。我们利用这一点，为 foldBag 实现了一个特化的导数。

我们在 3.2 节中已经看到，$\mathit{grand\_total}'$ 会不必要地重新计算 $\mathrm{merge}\ xs\ ys$。然而该结果是 fold′ 的一个基础输入。在下一节中，我们将用一个（同样基于 foldBag 的）自维护导数替换 fold′，从而避免这一重新计算。

为了保守地预测一个导数是否将会是自维护的（从而高效），可以检查该程序是否只使用了（有条件地）自维护的原语，例如 merge（总是自维护）或 $\mathrm{map}\ f$（仅当 $df$ 为零变化时，而当 $f$ 是闭项时这一点是有保证的）。

为了避免为自维护的导数（它们从不需要基参数）重新计算基参数，我们目前采用惰性求值。由于我们也可以改用死代码消除 [7] 的标准技术，惰性对我们的方法并不是核心。一个重要的限制是，非自维护的导数可能需要昂贵的计算来提供其基参数，而这些计算可能开销很大。由于这些值在运行基础程序时也会被计算出来，人们可以通过记忆化或静态缓存的扩展来复用先前计算出的值（如 5.2.2 节所讨论）。我们把实现这些优化留作未来工作。因此，只有当大多数导数是自维护的时，我们当前的实现才能给出好的结果。

### 4.4 案例研究

我们在一个非平凡的、现实的程序上进行案例研究，以证明 ILC 能够加速它。我们采用词频统计例子 [16] 的基于 MapReduce 的骨架。我们定义了一个合适的微分插件，把程序改写为使用它，并展示增量计算比重新计算更快。我们按照相应证明插件的要求来设计和实现该微分插件，尽管我们并没有（例如在 Agda 中）形式化该证明插件。由于篇幅所限，我们聚焦于对我们的例子及其性能至关重要的基本类型，即集合。该插件还用通常的引入与消去形式实现了元组、标签联合、布尔与整数，但对它们的导数只有很少的优化。

wordcount 接收一个从文档 ID 到文档的映射，产生一个从输入中出现的词到其出现次数的映射，即一个直方图：

$$\mathit{wordcount} : \mathrm{Map}\ \mathrm{ID}\ \mathrm{Document} \to \mathrm{Map}\ \mathrm{Word}\ \mathrm{Int}$$

为简单起见，我们不建模字符串，而是把文档建模为词的多重集、把文档 ID 建模为整数。因此，我们所实现的是：

$$\mathit{histogram} : \mathrm{Map}\ \mathrm{Int}\ (\mathrm{Bag}\ a) \to \mathrm{Map}\ a\ \mathrm{Int}$$

我们用整数来建模词（$a = \mathrm{Int}$），但参数化地对待它们。除此之外，我们直接把 Lämmel 的代码适配到我们的语言。图 5 给出了该 λ-项 histogram。

**图 5**：带 Haskell 风格语法糖的 λ-项 histogram。additiveGroupOnIntegers 是第 2.1 节所述整数上的群。（原图见 PDF 第 8 页）

图 6 给出了图 5 中所用原语的一个简化 Scala 实现。作为多重集的原语，我们提供若干构造子与一个折叠操作，遵循 Gluche 等人 [12]。多重集的构造子是 ∅（构造空多重集）、singleton（构造含一个元素的多重集）、merge（构造两个多重集的合并）与 negate（$\mathrm{negate}\ b$ 构造一个与 $b$ 元素相同但重数取负的多重集）；除 singleton 外，它们都表示阿贝尔群运算。与通常的 ADT 构造子不同，同一个多重集可以用不同的方式构造，而这些方式按定义阿贝尔群的等式是等价的；例如，由于 merge 可交换，$\mathrm{merge}\ x\ y = \mathrm{merge}\ y\ x$。多重集上的折叠会以任意方式通过构造子表示该多重集，然后以参数替换构造子；为保证结果良定义，fold 的参数应当遵循同样的等式，即它们应当构成一个阿贝尔群；例如，二元算子应当可交换。因此，折叠算子 foldBag 可以被定义为接收一个函数（对应于 singleton）与一个阿贝尔群（对应其余构造子）。foldBag 于是由如下方程定义：

$$\begin{aligned}
&\mathrm{foldBag} : \mathrm{Group}\ \tau \to (\sigma \to \tau) \to \mathrm{Bag}\ \sigma \to \tau\\
&\mathrm{foldBag}\ g@(\_, \oplus, \ominus, e)\ f\ \varnothing = e\\
&\mathrm{foldBag}\ g@(\_, \oplus, \ominus, e)\ f\ (\mathrm{merge}\ b_1\ b_2) = \mathrm{foldBag}\ g\ f\ b_1 \oplus \mathrm{foldBag}\ g\ f\ b_1\\
&\mathrm{foldBag}\ g@(\_, \oplus, \ominus, e)\ f\ (\mathrm{negate}\ b) = \ominus\, (\mathrm{foldBag}\ g\ f\ b)\\
&\mathrm{foldBag}\ g@(\_, \oplus, \ominus, e)\ f\ (\mathrm{singleton}\ v) = f\ v
\end{aligned}$$

若 $g$ 是一个群，这些方程精确地确定了 $\mathrm{foldBag}\ g$ [12]。此外，前三个方程意味着 $\mathrm{foldBag}\ g\ f$ 是多重集上的阿贝尔群与群 $g$ 之间的一个阿贝尔群同态（因为这些方程与该定义相吻合）。图 6 给出了按上述规定实现的 foldBag。此外，所有解构多重集的函数都可以用带合适参数的 foldBag 表达。例如，我们可以用 $\mathrm{foldBag}\ \mathrm{gZ}\ (\lambda x.\ x)$ 对一个整数多重集的元素求和，其中 $\mathrm{gZ}$ 是 2.1 节所定义的整数上的阿贝尔群。foldBag 的用户可以定义不同的阿贝尔群来指定不同的运算（例如，对浮点数做乘法）。

```scala
// Abelian groups
abstract class Group[A] {
  def merge(value₁: A, value₂: A): A
  def inverse(value: A): A
  def zero: A
}

// Bags
type Bag[A] = collection.immutable.HashMap[A, Int]

def groupOnBags[A] = new Group[Bag[A]] {
  def merge(bag₁: Bag[A], bag₂: Bag[A]) = …
  def inverse(bag: Bag[A]) = bag.map({
    case (value, count) ⇒ (value, -count)
  })
  def zero = collection.immutable.HashMap()
}

def foldBag[A, B](group: Group[B], f: A ⇒ B, bag: Bag[A]): B =
  bag.flatMap {
    case (x, c) if c ≥ 0 ⇒ Seq.fill(c)(f(x))
    case (x, c) if c < 0 ⇒ Seq.fill(-c)(group.inverse(f(x)))
  }.fold(group.zero)(group.merge)

// Maps
type Map[K, A] = collection.immutable.HashMap[K, A]

def groupOnMaps[K, A](group: Group[A]) = new Group[Map[K, A]] {
  def merge(dict₁: Map[K, A], dict₂: Map[K, A]): Map[K, A] =
    dict₁.merged(dict₂)({
      case ((k, v₁), (_, v₂)) ⇒ (k, group.merge(v₁, v₂))
    }).filter({
      case (k, v) ⇒ v ≠ group.zero
    })

  def inverse(dict: Map[K, A]): Map[K, A] = dict.map({
    case (k, v) ⇒ (k, group.inverse(v))
  })

  def zero = collection.immutable.HashMap()
}

// The general map fold
def foldMapGen[K, A, B](zero: B, merge: (B, B) ⇒ B)
  (f: (K, A) ⇒ B, dict: Map[K, A]): B =
    dict.map(Function.tupled(f)).fold(zero)(merge)

// By using foldMap instead of foldMapGen, the user promises that
// f k is a homomorphism from groupA to groupB for each k : K.
def foldMap[K, A, B](groupA: Group[A], groupB: Group[B])
  (f: (K, A) ⇒ B, dict: Map[K, A]): B =
    foldMapGen(groupB.zero, groupB.merge)(f, dict)
```

**图 6**：bags 与 maps 的原语的一个 Scala 实现。在代码中，我们分别把 ⊕、⊖ 与 $e$ 称作 merge、inverse 与 zero。我们还省略了相对标准的那些原语。（原图见 PDF 第 9 页）

若 $g$ 与 $f$ 不发生变化，$\mathrm{foldBag}\ g\ f$ 有一个自维护的导数。由上面的方程，

$$\begin{aligned}
&\mathrm{foldBag}\ g\ f\ (b \oplus db)\\
=\;& \mathrm{foldBag}\ g\ f\ (\mathrm{merge}\ b\ db)\\
=\;& \mathrm{foldBag}\ g\ f\ b \oplus \mathrm{foldBag}\ g\ f\ db\\
=\;& \mathrm{foldBag}\ g\ f\ b \oplus \mathrm{GroupChange}\ g\ (\mathrm{foldBag}\ g\ f\ db)
\end{aligned}$$

我们马上就会描述 $\mathrm{GroupChange}$ 这个变化构造子。在那之前我们注意到，作为推论，$\mathrm{foldBag}\ g\ f$ 的导数是

$$\lambda b\ db.\ \mathrm{GroupChange}\ g\ (\mathrm{foldBag}\ g\ f\ db)\text{，}$$

并且我们可以看到它不使用 $b$：正如所期望的，它是自维护的。为使 foldMap 的导数成为自维护的，还需要附加的限制。这些限制要求图 5 中 mapReduce 上的那个前置条件。foldMapGen 具有相同的实现但没有这些限制；因此，它的导数不是自维护的，但它有更广的适用性。篇幅所限，我们无法给出更多细节。

为了定义 $\mathrm{GroupChange}$，我们需要 $\tau$ 上一个合适的擦除的变化结构，使得 $\oplus$ 将等价于 $\bullet$。由于 $\tau$ 上可能有多个群，我们**允许变化指定一个群**，并让 $\oplus$ 委托给 $\bullet$：

$$\begin{aligned}
\Delta\tau &= \mathrm{Replace}\ \tau \mid \mathrm{GroupChange}\ (\mathrm{AbelianGroup}\ \tau)\ \tau\\
v \oplus (\mathrm{Replace}\ u) &= u\\
v \oplus (\mathrm{GroupChange}\ (\bullet, \mathrm{inverse}, \mathrm{zero})\ dv) &= v \bullet dv\\
v \ominus u &= \mathrm{Replace}\ v
\end{aligned}$$

也就是说，两个值之间的变化要么就是那个新值（它替换旧值，并触发重新计算），要么是它们的差值（用阿贝尔群运算计算，如同 2.1 节中群的变化结构那样）。$\ominus$ 算子并不知道该用哪个群，因此它不利用群结构。然而，foldBag 现在能够生成一个群变化了。

我们改用 foldBag 重写 $\mathit{grand\_total}$，以利用基于群的变化。

$$\begin{aligned}
\mathrm{id} &= \lambda x.\ x\\
G^{+} &= (\mathbb{Z}, +, -, 0)\\
\mathit{grand\_total} &= \lambda xs.\ \lambda ys.\ \mathrm{foldBag}\ G^{+}\ \mathrm{id}\ (\mathrm{merge}\ xs\ ys)
\end{aligned}$$

$$\begin{aligned}
&\mathrm{Derive}(\mathit{grand\_total}) =\\
&\quad \lambda xs.\ \lambda dxs.\ \lambda ys.\ \lambda dys.\ \mathrm{foldBag}'\ G^{+}\ G^{+}{}'\ \mathrm{id}\ \mathrm{id}'\ (\mathrm{merge}\ xs\ ys)\ (\mathrm{merge}'\ xs\ dxs\ ys\ dys)
\end{aligned}$$

现在可以写出 foldBag 的导数了。

（若静态分析检测到 $dG$ 与 $df$ 是零变化）

$$\mathrm{foldBag}' = \mathrm{Derive}(\mathrm{foldBag}) = \lambda G.\ \lambda dG.\ \lambda f.\ \lambda df.\ \lambda zs.\ \lambda dzs.\ \mathrm{GroupChange}\ G\ (\mathrm{foldBag}\ G\ f\ dzs)$$

由 3.7 节我们知道

$$\mathrm{merge}' = \lambda u.\ \lambda du.\ \lambda v.\ \lambda dv.\ \mathrm{merge}\ du\ dv\text{。}$$

内联 $\mathrm{foldBag}'$ 与 $\mathrm{merge}'$ 就得到与 $\mathit{grand\_total}$ 的导数 β-等价的一个更可读的项：

$$\mathrm{Derive}(\mathit{grand\_total}) = \lambda xs.\ \lambda dxs.\ \lambda ys.\ \lambda dys.\ \mathrm{foldBag}\ G^{+}\ \mathrm{id}\ (\mathrm{merge}\ dxs\ dys)\text{。}$$

### 4.5 基准测试结果

我们的结果（图 7）表明，我们的程序对输入变化的反应基本上是常数时间，这与预期相符，因此比重新计算快若干个数量级。常数因子足够小，因此在现实的输入规模上，加速比是明显的。

由于篇幅所限，关于基准测试结果与输入的细节可以在我们论文的扩展版（附录 A）中获得。

<img src="figures/fig7-performance.png" alt="Figure 7：性能结果（对数-对数坐标）" style="width:532px;max-width:100%" />

**图 7**：性能结果（对数-对数坐标），横轴为输入规模，纵轴为运行时间（ms）。置信区间由误差条（whiskers）表示；大多数误差条太小而不可见。（原图见 PDF 第 10 页）

从这些评估中可以得到两个重要的教训：

- 正如 §4.3 所预料的，要获得良好性能，我们当前的实现需要某种形式的死代码消除（dead code elimination），例如惰性求值（laziness）。
- 增量化会显著增大代码体积。分析并应对这一增长留待未来工作。

## 5 相关工作

已有的增量计算工作可以分为两组：静态增量化与动态增量化。静态方法静态地分析程序并生成它的一个增量版本。动态方法在程序运行时建立动态依赖图，并沿这些图传播变化。

两者之间的权衡在于：静态方法有潜力更快，因为运行时不需要依赖跟踪；而动态方法能够支持表达能力更强的编程语言。ILC 是一种静态方法，但与其他静态方法相比，它支持表达能力更强的语言。在本节余下部分，我们分析与最密切相关的前人工作的关系。Ramalingam 与 Reps [21]、Gupta 与 Mumick [13] 以及 Acar 等 [3] 讨论了更多的相关工作。

### 5.1 动态方法

最先进的动态增量化方法之一是自调整计算（self-adjusting computation），它已被应用于 Standard ML 以及 C 的大部分子集 [2, 14]。在这种方法中，程序在增强的运行时环境中对原始输入执行，该环境在动态依赖图（dynamic dependence graph）[3] 中跟踪值之间的依赖关系；中间结果被记忆化。随后，对输入的变化沿依赖图从被改变的输入传播到结果，更新中间结果与最终结果；这一处理通常比重新计算更高效。

然而，建立动态依赖图会在运行时带来很大的常数因子开销，在已报告的实验中为 2 到 30 倍 [4, 5]，并且会影响程序在其基础输入上的首次运行。Acar 等 [5] 展示了如何在自调整计算的背景下支持高层数据类型；然而，该方法在首次运行期间仍然需要昂贵的运行时簿记（bookkeeping）。我们的方法与其他静态方法一样，使用标准的运行时环境，在基础计算期间没有开销，但在处理变化时可能效率较低。当初始输入相对于其变化很大时，这样做是划算的。

Chen 等 [9] 为纯函数式程序开发了一种静态变换，但这种变换只是提供了一个更好的接口，以便用更少的样板代码使用运行时支持，并没有降低这一性能开销。因此，它仍然是一种动态方法，不同于本文提出的变换。

自调整计算的另一个性质是：只有当程序具有合适的计算结构时，增量化才是高效的。例如，用左折叠或右折叠对多重集（bag）的元素做折叠的程序不会有高效的增量行为；相反，折叠必须呈平衡树的形状。一般来说，只有当增量计算是稳定的（stable）[1] 时，它才会变得高效。因此，可能需要改造（massage）程序以使其高效。我们的方法论不同：由于我们并不打算增量化用标准编程语言编写的任意程序，我们可以选择具有高效导数的原语，从而要求程序员使用它们。

函数式响应式编程（functional reactive programming）[10] 也可以被看作一种动态的增量计算方法；Maier 与 Odersky 的近期工作 [18] 致力于通过让集合上的操作增量化，来加快对输入变化的反应。Willis 等 [24] 使用动态技术来增量化 JQL 查询。

### 5.2 静态方法

静态方法在编译期分析程序，并产生一个增量版本，该版本根据不断变化的输入高效地更新原程序的输出。

静态方法有潜力比动态方法更高效，因为运行时不需要簿记。此外，计算出的增量版本通常可以用标准编译技术（例如常量折叠或内联）来优化。然而，它们都不支持一等函数；有些方法还有进一步的限制。

我们的目标是把静态增量化应用于表达能力更强的语言；特别地，ILC 支持一等函数，以及一个开放的、带有关联原语操作的基本类型集合。

#### 5.2.1 有限差分

Paige 与 Koenig [20] 给出了一个带固定原语集合的一阶语言的导数。Blakeley 等 [8] 把这些思想应用于一类关系查询。数据库社区把这项工作扩展到了关系数据上的查询，例如代数差分（algebraic differencing）[13]，它启发了我们的工作与术语。然而，这些工作大多不适用于嵌套集合或代数数据类型，而只适用于关系（扁平）数据，并且此前没有任何方法能处理一等函数。增量支持通常是针对整个语言整体地（monolithically）设计的，而不是逐块地（piecewise）设计的。改进了代数差分，Koch [15] 通过一种可组合的查询变换保证了渐近加速，并在现实的基准测试中带来了巨大的加速，不过仍然针对一阶数据库语言。

Gluche 等 [12] 的工作考虑了更一般（非关系）的数据类型；我们对多重集（bag）的支持以及对群的使用受到了他们工作的启发，但他们的架构仍然相当受限：他们缺少对函数变化的支持，并把增量化限制在自维护视图（self-maintainable views）上，且没有暗示任何可能的解决方案。

#### 5.2.2 静态记忆化

Liu 的工作 [17] 允许增量化一个一阶基础程序 $f(x_{\mathrm{old}})$，在已知 $x_{\mathrm{new}}$ 与 $x_{\mathrm{old}}$ 之间关系的情况下计算 $f(x_{\mathrm{new}})$。为此，他们把 $f(x_{\mathrm{new}})$ 变换为一个增量程序，该程序复用计算基础程序 $f(x_{\mathrm{old}})$ 时产生的中间结果。为此，(i) 首先把基础程序变换为保存它的所有中间结果，然后 (ii) 把增量程序变换为复用这些中间结果，最后 (iii) 从基础程序中剪除不需要的中间结果。然而，为了复用中间结果，增量程序常常必须用某种等式推理（equational reasoning）重排为一个等价程序，使部分结果字面上出现。例如，如果基础程序 $f$ 使用左折叠对整数列表 $x_{\mathrm{old}}$ 的元素求和、从表头开始访问它们，而 $x_{\mathrm{new}}$ 在列表前面添加一个新元素 $h$，那么 $f(x_{\mathrm{new}})$ 在任何时刻都不会重新计算出相同的结果。但由于加法在整数上是可交换的，我们可以把 $f(x_{\mathrm{new}})$ 重写为 $f(x_{\mathrm{old}}) + h$。作者的 CACHET 系统会尝试自动进行这类重写，但不保证成功。类似地，CACHET 会尝试合成任何能由基础程序廉价计算出的额外结果，以帮助增量程序变得更高效。

由于很难完全自动化这类推理，我们把等式推理移到插件设计阶段。插件提供通用的高阶原语，插件作者已经为这些原语设计了高效的导数（在设计阶段使用等式推理）。然后，微分算法计算用户程序的增量版本，而不需要用户进一步干预。把 ILC 与某种形式的静态缓存结合起来，以使那些非自维护的导数的计算更高效，将会是有用的。我们计划在未来工作中这样做。

## 6 结论与未来工作

我们提出了 ILC，一种把一阶程序上的增量计算提升到高阶程序上的增量计算的方法。我们给出了针对 ILC 的一个形式化的、经过机器检验（machine-checked）的正确性证明，以及一项初步的实验评估，其形式包括一个实现、一个针对映射（maps）与多重集（bags）的示例插件，以及一个被成功且高效地增量化的非平凡例子。

我们的工作开辟了若干未来工作方向。我们当前的实现在非自维护（non-self-maintainable）的导数上效率不高。然而，正如 §4.3 所讨论的，我们将研究如何对中间结果进行记忆化，以解决这一局限。我们的下一步将是开发具有高效非自维护原语的语言插件。

未来工作的另一个方向是增加对代数数据类型（包括递归类型）、多态、子类型（subtyping）、一般递归以及其他集合类型的支持。虽然对代数数据类型的支持可以涵盖对特定集合的支持，但许多集合具有额外的代数性质，能够实现更快的增量化（例如多重集（bag））。即使是（代数性质较少的）列表，也能从专门的支持中受益 [18]。

此外，我们打算在 SQUOPT 项目 [11] 的背景下应用 ILC 来优化针对集合的查询，该项目也是本工作的一个动机；特别地，SQUOPT 能够自动把查询重写为使用数据库风格索引的形式，而 ILC 使得在输入数据发生变化时更新这些索引成为可能。

最后，我们打算进行一项全面而彻底的实验评估，以证明 ILC 能够对大规模的实际程序进行增量化。

## 致谢

我们感谢 Ingo Maier、Erik Ernst、Tiark Rompf 及其他 ECOOP 2013 参会者、Sebastian Erdweg、Christoph Koch 以及 PLDI ’14 的匿名审稿人，感谢他们有益的讨论和/或对先前草稿的评论。本工作由欧洲研究理事会（European Research Council）资助，基金号为 #203099 “ScalPL”。