解构 Datalog：从逻辑编程到类型化函数式语言的融合

背景

2022年9月，经过两轮修订，我提交了博士论文的最终版本，题为《解构 Datalog》（Deconstructing Datalog）。Datalog 是一门源自 20 世纪 80 年代的逻辑编程语言，它在关系代数基础上增加了递归查询功能。Datalog 拥有简洁的语义和高效的实现策略。正如 Lisp 和 The Velvet Underground（地下丝绒乐队）一样，Datalog 的影响力远超其流行度；其核心思想仍在不断被主流技术所吸收。

尽管 Datalog 具有极高的“功率重量比”（即功能强大且概念简洁），但它也存在明显的局限性。首先，它没有函数或过程：无法抽象出重复的代码。作为一名类型化函数式编程的爱好者，我不禁思考：将两者结合有多难？我们拥有 x（自下而上的逻辑编程）；我们拥有 y（函数式编程）；那么 x + y 会是什么？

就像孩子玩乐高积木一样，我决定将两个酷炫的东西强行组合在一起，制造出一个更大、更酷的东西：Datafun。

结果证明，这行得通！当然，过程中也出现了一些复杂情况。如果你想了解完整的故事，请阅读这篇论文。这是一篇篇幅适中的博士论文：正文 97 页，加上附录。主要成果包括：(i) 这个看似疯狂的想法是可行的；(ii) 从渐近复杂度的角度来看，我们可以让它运行得相当快。

核心内容

博士论文的核心思想是：我们可以通过逆向推导其语义，将 Datalog 的特性无缝集成到类型化函数式语言中。

从谓词到集合与函数

以 Datalog 最显著的特性——递归查询为例，例如图中的可达性查询：

reachable(start).
reachable(Y) :- reachable(X), edge(X,Y).

这段代码旨在找到满足以下条件的最小集合 reachable：(1) start 是可达的；(2) 如果 X 是可达的，且存在一条从 X 到 Y 的边，那么 Y 也是可达的。

我们可以将这些条件重写为关于集合的单个不等式：

$$ reachable \supseteq {start} \cup {y : x \in reachable, (x,y) \in edge} $$

进一步提取右侧因子：

$$ reachable \supseteq f(reachable) $$

其中 $f(R) = {start} \cup {y : x \in R, (x,y) \in edge}$。

这实际上是在寻找一个最小前缀点（least prefix point）：即满足 $R \supseteq f(R)$ 的最小集合 $R$。事实上，Datalog 中的所有递归查询都符合这一模式。因此，要在函数式语言中捕捉递归查询，我们需要：(a) 一个用于表达关系上函数的强大语言；(b) 一个最小前缀点算子 fix。

这样，我们的查询就变成了：

$$ fix (\lambda R. {start} \cup {y | x \in R, (x,y) \in edge}) $$

短短几步，我们就将“谓词与逻辑”转化为了“集合与函数”。

单调性与类型系统

论文第二章详细阐述了这一配方。最独特的部分在于，为了捕捉 Datalog 的分层条件（stratification condition，确保递归查询定义良好），Datafun 需要在类型系统中跟踪单调性（monotonicity）。

这种跟踪是组合式的：如果两个映射都是单调的，那么它们的组合也是单调的；否则不是。从更技术性的角度来看，在非单调的世界中，非单调性可以通过以下方式表示：

• 在范畴论中：单Monad（monoidal comonad）
• 在类型理论中：必然模态（necessity modality）
• 在编译器中：仔细跟踪哪些变量可以安全地以非单调方式使用。

像大多数类型系统一样，这是安全的但不完备的——类型检查器可能会将某些单调程序错误地拒绝为非单调程序。但它能够处理 Datalog 所能处理的所有内容，甚至更多。

如何更快地寻找不动点

上述内容省略了一个重要细节：fix 的实现，即如何找到满足 $R \supseteq f(R)$ 的最小集合 $R$。

以图可达性为例： $$ f(R) = {start} \cup {y | x \in R, (x,y) \in edge} $$

朴素迭代法（Naïve approach）是反复应用 $f$：

• $R_0 = \emptyset$
• $R_1 = f(\emptyset) = {start}$
• $R_2 = f(f(\emptyset)) = $ 距离 start 1 条边内的节点
• ...
• $R_i = f^i(\emptyset) = $ 距离 start $i-1$ 条边内的节点

直到 $R_i = R_{i+1}$，即找到了最远的可达节点。

这种方法极其低效，因为它做了大量冗余工作。为了计算 $f(R_i)$，集合推导式 ${y | x \in R_i, (x,y) \in edges}$ 会检查 $R_i$ 中的每个节点。由于序列 $R_i$ 是单调递增的（$R_0 \subseteq R_1 \subseteq R_2 \dots$），如果在早期迭代中已经到达某个节点，后续迭代中会浪费性地重新检查它。在某些图结构（如链式图）中，这会导致二次方的复杂度爆炸，每个节点平均被检查线性次。

解决方案：只检查每个节点一次。

• 朴素迭代问的是：“在最多 $n$ 步内我能推导出什么？”（$n$ 逐渐增加）。
• 半朴素迭代（Seminaïve iteration）问的是：“在 $n$ 步内我能推导出什么，而这些是我之前无法推导出的？”

换句话说，它关注的是朴素迭代步骤之间的变化量——即“知识的前沿”（frontiers of knowledge）。

我们可以通过对推导函数 $f$ 进行增量计算（incrementalizing）来计算这些前沿：给定输入的变化，输出如何变化？即给定上一个前沿，下一个前沿是什么？

这可以通过对程序取离散导数来实现，这一概念在之前的增量 $\lambda$ 演算（incremental $\lambda$-calculus）工作中得到了精确描述。论文第三章展示了如何将这一工作应用于 Datafun，使其针对单调（递增）变化进行增量计算。

关键要点

• Datalog 的局限与 Datafun 的诞生：Datalog 缺乏函数抽象能力。作者通过结合自下而上的逻辑编程（Datalog）和函数式编程，创造了 Datafun，旨在保留 Datalog 递归查询优势的同时引入函数式抽象。
• 语义转换：Datalog 的递归查询可以通过“集合包含不等式”和“最小前缀点算子 fix”来重新表述，从而将逻辑谓词转化为函数式语言中的集合运算。
• 单调性类型系统：Datafun 的核心创新在于其类型系统能够跟踪函数的单调性。这是确保递归查询定义良好（分层条件）的关键。非单调性通过范畴论中的 comonad 或类型论中的模态来处理。
• 增量计算优化：朴素的不动点迭代会导致冗余计算（二次复杂度）。通过引入“半朴素迭代”和离散导数概念，Datafun 实现了增量计算，仅关注每一步的变化量（知识前沿），从而显著提高了效率。
• 论文结构：
  • 第二章：详细阐述将 Datalog 特性集成到类型化函数式语言的配方，重点在于单调性类型系统。
  • 第三章：展示如何应用增量 $\lambda$ 演算理论，对 Datafun 进行针对单调变化的增量计算优化。

意义与影响

这篇博士论文不仅解决了一个具体的工程问题（如何高效实现带有函数抽象的逻辑编程），更在理论层面弥合了逻辑编程与函数式编程之间的鸿沟。