在2022年9月，经过两轮修订，我提交了我的博士论文的最终版本，题为《解构 Datalog》。Datalog 是一种源自80年代的逻辑编程语言，它通过递归查询扩展了关系代数。它具备简单的语义和高效的实现策略。像 Lisp 和 Velvet Underground 一样，它的影响力超出了它的受欢迎程度；其思想仍在被主流吸收。尽管 Datalog 的功率重量比很高，但它相对有限。一方面，它没有函数或过程：没有办法抽象出重复的代码。作为一个类型 функционал编程的爱好者，我想：这有什么难的呢？我们有 x（自底向上的逻辑编程）；我们有 y（函数式编程）；x + y 是什么？就像孩子玩乐高一样，我开始将两种酷炫的东西结合在一起，创造出一个更大、更酷的东西：Datafun。结果是成功的！不过，过程中也出现了一些复杂情况。如果你想知道整个故事，你只需阅读它。它是一篇相对简短的论文：97 页加上附录。但是主要的结果是：（i）这个疯狂的想法是可行的，（ii）从渐进的角度来看，我们可以让它运行得相当快。拆解 Datalog 并重新组合 我论文的核心思想是，我们可以通过从其语义反向工作，将 Datalog 的特性无缝整合到一个类型函数语言中。以 Datalog 最具代表性的特征——递归查询为例；例如，在图中的可达性：reachable(start)。reachable(Y) :- reachable(X), edge(X,Y)。这找到了可达的最小集合，使得（1）start 是可达的，并且（2）如果 X 是可达的并且有一条到 Y 的边，则 Y 也是可达的。我们可以将这些条件重写为集上的一个单一不等式：reachable ⊇ {start} ∪ {y : x ∈ reachable, (x,y) ∈ edge} 我们可以重写这个公式以提取右侧：reachable ⊇ f(reachable) 其中 f(R) = {start} ∪ {y : x ∈ R, (x,y) ∈ edge} 这需要一个最小前缀点：最小的 R 至少包含 f(R) 对于某个关系上的函数 f。事实上，Datalog 中的所有递归查询都符合这种模式。因此，为了在函数式语言中捕捉递归查询，我们需要（a）一个表达函数在关系上的功能的语言，以及（b）一个最小前缀点操作符 fix。这个操作将我们的查询变为：fix (λR. {start} ∪ {y | x ∈ R, (x,y) ∈ edge}) 在短短几步中，我们将谓词和逻辑转变为集合和函数。第二章详细工作出这个公式。最独特的是，为了捕获 Datalog 的分层条件，确保递归查询是明确定义的，Datafun 需要在其类型系统中跟踪单调性。这是通过组合性工作：两个映射的组合是单调的，如果两个映射都是单调的；否则不是。更技术性地说，非单调性可以在一个随机单调的世界中通过（在范畴理论中）单元共同代或（在类型理论中）必要性方式或（在编译器中）谨慎跟踪哪些变量可以安全地以非单调方式使用来表示。像大多数类型系统一样这是安全的但不完整——类型检查器将一些单调程序拒绝为非单调的——但它处理所有 Datalog 可以处理的东西，甚至可能更多。如何更快（地）找到固定点 一个被省略的重要细节是 fix 的实现：我们如何找到最小集合 R，使得 R ⊇ f(R)。以图的可达性为例：f(R) = {start} ∪ {y | x ∈ R, (x,y) ∈ edge} 原始的方法是迭代 f：R₀ = ∅ = 无 R₁ = f(∅) = {start} R₂ = f(f(∅)) = start 的 1 边内的节点 R₃ = f(f(f(∅))) = start 的 2 边内的节点 ... Rᵢ = fⁱ(∅) = start 的 i-1 边内的节点 ... 直到最终 Rᵢ = Rᵢ₊₁，因为我们找到了最远的可达节点。这是一种极其低效的广度优先搜索，因为它做了冗余工作。考虑计算 f(Rᵢ) 所需的集合理解 {y | x ∈ Rᵢ, (x,y) ∈ edges}。这检查了 Rᵢ 中的每个节点；所以总的工作量至少是每个 Rᵢ 大小的总和。现在观察到序列 Rᵢ 是单调增长的，R₀ ⊆ R₁ ⊆ R₂ ⊆ ...，因为在 start 的 1 边内的节点也在 2 边内，等等。因此，如果我们在早期的迭代中达到了一个节点，我们在后续的每次迭代中都浪费地重新检查它。在一些图中，这会导致二次膨胀（例如，设 edge = {(i, i+1) | i ∈ [1..n]}），每个节点平均检查线性次数！解决方案是每个节点只检查一次。原始的迭代问“我最多在 n 步内能推导出什么？”对于逐步增加 n。而半原始迭代问：“我在 n 步内能推导出什么，而我之前无法推导？”换句话说，它询问原始迭代步骤之间的变化——知识的边界。我们可以通过增量化我们的推导函数 f 来计算这些边界，弄清楚它如何响应变化：给定对其输入的变化，它的输出如何变化——也就是说，给定先前的边界，下一边界是什么？