查询语言求值顺序与非终止性问题

背景

在编程语言与数据库的交汇处，如何结合函数式编程与关系查询（如 Datalog 或 SQL）一直是一个活跃的研究方向。作者此前提出的 Datafun 便是尝试之一，而本文介绍的 λFS（有限函数式编程）则是其最新成果——它不仅融合了函数式与关系式编程，还扩展到了张量代数。然而，当引入递归时，一个核心难题浮现：非终止性（nontermination）。传统上，处理非终止性需要域论（domain theory），但域论在过去几十年中已不再流行，且作者坦言自己未曾深入研究。更深层次的问题是，一旦涉及非终止性或任何副作用，求值顺序（evaluation order）就成了关键——这在关系型语言中比在纯函数式语言中影响更为复杂。本文正是围绕 λFS 引入递归时遇到的求值顺序与终止性矛盾展开讨论。

核心内容

λFS 的基本思想

在 λFS 中，关系 R 被看作一个有限布尔函数：R(x) 为真当且仅当 x 属于 R，否则为假。该函数是“有限”的，因为只有有限多个输入 x 使得 R(x) 为真——这些输入构成其支持集（support）。论文给出了一个类型系统来确保函数具有有限支持。在运行时，有限布尔函数通过哈希表或平衡树（类似数据库中的表）来实现其支持集。

这一思想可以推广到任何具有“默认值”的陪域：函数的支持集是那些输出非默认值的输入。例如，布尔型以 false 为默认值，整数以 0 为默认值。有限函数便表示为键-值表，键为支持集元素，其他键隐式映射到默认值。非布尔型的有限映射自然出现在聚合操作的结果中，而张量代数本质上就是基于非布尔型（通常是实数值）有限映射的关系代数。

非终止性与求值顺序问题

在演讲中，作者提到递归是 λFS 的未来工作。与会者 Atsushi Igarashi 问及困难所在。主要难点在于递归允许非终止性。非终止性的语义通常依赖域论，但作者对此不太熟悉，且域论已经不再流行。更麻烦的是，一旦引入非终止性或任何效应，就必须考虑求值顺序。即使在无类型 lambda 演算中（其求值是合流的），按名调用和按值调用在不同程序上终止性也不同。而在关系型语言中，“求值顺序”的含义比函数式语言更广。

考虑以下例子：

• => 表示有限函数（表），-> 表示任意函数（过程或闭包）。
• 查询 Q 是表 R 和 S 的交集，再经黑盒谓词 test 过滤。

核心问题是：按何种顺序求值？我们可以从左到右：对 R 中每个 x，若 test(x) 通过，再检查 x 是否在 S 中。也可以先检查 x 是否在 S 中再调用 test，或如果 S 远小于 R，则遍历 S 而不是 R。

标准的关系哲学把求值顺序看作实现细节，由查询规划器决定。然而，这个顺序可能影响 Q 是否终止，因为不同顺序会用不同参数调用 test。例如：

• R := {"hello", "world"}
• S := {"hello", "alice"}
• test(x) := x == "hello" or loop-forever()
• Q(x) := R(x) and test(x) and S(x)

从左到右执行会先调用 test("hello")（成功），然后调用 test("world")（永远循环）。但如果先取 R 和 S 的交集再调用 test，则只会测试 "hello"，从而终止。

这个问题在 λFS 中已存在，但也出现在任何支持用户定义函数的 SQL 或 Datalog 引擎中。它暴露了数据库与编程语言（PL）假设之间的张力：

• 数据库视角：查询引擎可自由选择执行策略以优化性能。
• PL 视角：我们希望能组合式地推理程序行为，特别是关于终止或执行时间。

λFS 试图桥接两者，却陷入了尴尬的中间地带：必须偏向某一方，或找到某种折中方案。作者尚未找到最佳答案，但给出了三个可能的方向。

三种可能的前进方向

1. 从左到右求值：简单且可预测的成本模型

最简单的策略是固定从左到右求值。这是最典型的 PL 方法：避免查询规划，将性能负担完全交给程序员。这使得查询的执行时间易于预测和推理——正如作者的朋友 Rob Simmons 在 Finite Choice Logic Programming (FCLP) 中指出的那样，这正是 Dusa（FCLP 的实现）的成本模型。

在这种方法中，n 项合取转化为至多 n 层嵌套循环。例如：

• R(x) and S(y) → 两层循环：对于 R 中的每个 x，对于 S 中的每个 y，输出 (x,y)。
• R(x) and S(x) → 当 S(x) 的变量已经被绑定时，生成一个测试：对于 R 中的每个 x，如果 x 不在 S 中则跳过。

如果某个合取项的部分变量已接地，则需要索引。例如 R(x,y) and S(y,z) 需要按 y 对 S 建立索引。

若所有合取项都是有限映射的应用，成本模型很简单：统计前缀触发次数（prefix firings）。即对于每个前缀，计算满足它的自由变量赋值有多少个。对于黑盒谓词 test(x)，其所有参数必须由前面的合取项接地；我们为前面合取项的每次触发计算 test(x) 的成本。

这直接回答了终止性问题：谓词只在其前面合取项满足的那些值上被调用。巧合的是，从左到右的接地要求恰好与有限函数式编程论文中的类型系统相匹配。

作者欣赏这种方法的简单性和可预测性，但也承认其缺点：将性能责任交给了程序员，而且对于某些查询（如循环查询 edge(x,y) and edge(y,z) and edge(x,z)）无法获得可接受的性能。

2. 非确定求值顺序：允许声明式优化

前面已经看到 R(x) and test(x) and S(x) 有三种合理的求值顺序。为什么非要预先承诺？典型的数据库方法是通过不指定求值顺序来给查询规划器/优化器尽可能多的灵活性。

这意味我们无法确切知道会在哪些值上调用 test，但可以给出一个上下界。程序终止也从是/否问题变成了是/否/可能。例如，对于 R(x) and test(x) and S(x)，任何查询执行最多调用 R 或 S 中的值，最少调用两者交集的值。如果 test(x) 对所有 x ∈ R ∪ S 终止，则查询终止；若对某个 x ∈ R ∩ S 发散，则查询发散；否则结果不确定。但所有终止的执行应该给出相同结果。

然而，作者不知道如何以组合式的方式指定这种不确定性。两种典型语义（操作语义和指称语义）都有困难。

3. 混合求值：在局部约束下优化

如果不想完全放弃声明式优化，可以设计一种类型系统，标记哪些函数是“健康的”（保证终止）或“干净的”（没有副作用），从而允许查询规划器在安全时优化。这种方法类似于 SQL 中的确定性函数（DETERMINISTIC）声明。但这种方法要么过于保守（限制表达力），要么需要复杂的分析。

作者指出，当合取项中存在黑盒函数时，关系数据库通常采用“安全计划”策略：先执行所有基于索引的、确定性的部分，再对剩余较少的元组调用黑盒函数。这实际上相当于一种后处理过滤。

关键要点

• 有限函数式编程（λFS）：将关系视为有限布尔函数，支持集用哈希表或平衡树表示，可推广到其他默认值域，并自然支持张量代数。
• 核心矛盾：递归引入非终止性，而非终止性又与求值顺序交织。数据库追求优化自由度，编程语言追求组合式可推理性，两者在用户定义函数存在时产生冲突。
• 求值顺序影响终止性：简单的例子（R∩S过滤黑盒谓词）表明，不同的求值顺序可能导致谓词在不同参数上被调用，进而影响查询是否终止。
• 三个方向：
  1. 固定从左到右