查询语言中的求值顺序与非终止性

# 查询语言中的求值顺序与非终止性 来源：https://www.rntz.net/post/2026-06-11-datalog-nontermination.html 2026年6月 上个月我在FLOPS（https://functional-logic.org/events/flops/2026/）上做了一个关于**有限函数式编程**（https://arxiv.org/abs/2604.26161）（简称“λFS”）的演讲，这是我最新的一次尝试（此前有Datafun（https://www.rntz.net/datafun)），旨在将函数式编程与类似Datalog或SQL的关系式编程结合起来——还包括张量代数，何乐而不为呢？ 在λFS中，关系R被视为一个函数：定义R\(*x*\) = true 当且仅当*x*属于R，否则为false。这个函数是**有限**的，因为R\(*x*\) = true 只对有限多个输入*x*成立：这些输入构成了它的**支撑集**。该论文（https://arxiv.org/abs/2604.26161）给出了一种类型系统来确保函数具有有限支撑集。在运行时，我们通过将支撑集存储在哈希表或平衡树（类似数据库中的表）中来表示有限布尔函数。 这种方法可以推广到任何带有“默认”值的余域。函数的支撑集是那些输出非默认值的输入；例如，以false为默认值的布尔值，或以0为默认值的整数。有限函数可以表示为一个键值表，其中的键是函数的支撑集；任何其他键隐式映射到默认值。非布尔有限映射自然产生于聚合操作，而张量代数本质上是非布尔（通常是实值）有限映射的关系代数。 ## 非终止性与求值顺序 在演讲中，我提到递归是λFS的未来工作。自然，有人——我认为是五十嵐淳（Atsushi Igarashi）——问到了难点所在。主要难点在于递归可能导致非终止性。非终止性的语义通常使用域理论，而域理论在近几十年已不再流行，因此我从未深入学习过，觉得它有点令人生畏¹（https://www.rntz.net/post/2026-06-11-datalog-nontermination.html#fn-1）。 此外，一旦涉及非终止性或任何效应，就存在求值顺序的问题。即使在具有合流性的无类型λ演算中，按名调用和按值调用也会在不同程序上终止。更糟糕的是，在关系式语言中，“求值顺序”的含义比函数式语言更为宽泛。考虑这个例子： 给定`R,S : nat => bool`输入表 和 `test : nat -> bool` 黑盒谓词，令 `Q(x) := R(x) and test(x) and S(x)` 查询。这里，`=>` 表示一个有限函数，以表的形式表示；而 `->` 表示任意函数，以过程或闭包的形式表示。从关系式角度思考，我们的查询 `Q` 是表 `R` 和 `S` 的交集，并由黑盒谓词 `test` 过滤。 核心问题是：**我们以何种顺序求值这个查询？**我们可以从左到右：对于 `R` 中的每个 `x`，如果 `test(x)` 通过，则检查 `x` 是否在 `S` 中。用Python表示： ```python [x for x in R if test(x) if x in S] ``` 或者，注意到 `test` 可能很昂贵，但查表很便宜，我们可以在调用 `test` 之前先检查 `x` 是否在 `S` 中： ```python [x for x in R if x in S if test(x)] ``` 如果我们碰巧知道 `S` 比 `R` 小得多，我们可以通过遍历 `S` 而非 `R` 来节省大量时间： ```python [x for x in S if x in R if test(x)] ``` 标准的关系式哲学将求值顺序视为实现细节，由查询优化器决定。然而，这种顺序可能会影响 `Q` 是否终止，因为不同的顺序会在不同的参数上调用 `test`。一个刻意构造的例子： ```python 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")`，它会永远循环。但如果我们**在调用 `test` 之前**先求 `R` 和 `S` 的交集，那么只会测试 `"hello"`，从而终止。 我在λFS中表述了这个问题，但它也会出现在任何支持用户自定义函数的SQL或Datalog引擎中，并暴露了典型的数据库和编程语言假设之间的张力： **数据库**：查询引擎可以选择执行策略以优化性能。 **编程语言**：我们可以组合性地推理程序行为——特别是关于终止性或执行时间。 λFS试图弥合数据库与编程语言，结果卡在了尴尬的中间地带：我必须要么偏向某一视角，要么找到一种折中之道。目前我尚未找到最佳方法。因此，这里提出三个前进方向——三个可能的λFS（或带非终止函数的Datalog）语义草图。 ## 1. 从左到右求值具有简单的代价模型 最简单的实现策略也具有最直接的语义：从左到右求值。这是最典型的编程语言方法：它避免了查询规划，将责任完全交给程序员。正如我的朋友Rob Simmons（https://typesafety.net/rob/about/）在开发**有限选择逻辑编程**（https://dl.acm.org/doi/10.1145/3704849）时向我指出的那样，这使得查询的执行时间易于预测和推理；这大致就是FCLP实现Dusa（https://dusa.rocks/docs）的代价模型。 在这种方法中，由 *n* 项组成的合取变成至多 *n* 层嵌套循环。例如，`R(x) and S(y)` 变成2层循环： ```python for x in R: for y in S: yield (x,y) ``` 在像 `R(x) and S(x)` 这样的查询中，`S(x)` 的变量已经完全被实例化，于是我们生成一个测试而不是循环： ```python for x in R: if x not in S: continue yield x ``` 如果某个合取项的部分变量已被实例化，我们需要一个索引；例如，执行 `R(x,y) and S(y,z)`，我们希望按 `y` 对 `S` 进行索引： ```python for x,y in R: for z in S_index[y]: -- 假设有合适的 S_index yield (x,y,z) ``` 如果我们有这些索引，并且所有合取项都是有限映射的应用，那么代价模型很简单：计算前缀触发次数。也就是说，对于合取的每个前缀，**统计满足它的自由变量赋值数量**。因此对于 `R(x,y) and S(y,z)`，我们相加： 1. 满足 `R(x,y)` 的 `x,y` 元组数量。 2. 满足 `R(x,y) and S(y,z)` 的 `x,y,z` 元组数量。 对于像 `test(x)` 这样的黑盒谓词呢？对于这样的合取项： 1. 它的所有参数必须由前面的合取项实例化，这样当我们到达它时，我们拥有具体的值。 2. 我们对前面合取项的每次触发，都加上调用 `test(x)` 的代价。这可能超过总的 `x` 值的数量；例如，`R(x) and S(y) and test(x)` 会对每个 `x,y` 对调用一次 `test(x)`。 这直接回答了关于终止性的原始问题：我们只对满足前面合取项的那些值运行谓词。完全巧合的是，从左到右的实例化要求恰好与有限函数式编程论文（https://arxiv.org/abs/2604.26161）中的类型系统匹配；我最初认为这是类型系统的一个弱点，但采用从左到右的执行策略后，它变得完全合理。 我喜欢这种方法的简单性和可预测性，并欣赏它“直面问题”，让程序员负责性能（尽管这显然也是一个缺点）。不幸的是，对于某些查询（**循环查询**），这种方法无法获得可接受的性能——例如，三角形查询 `edge(x,y) and edge(y,z) and edge(x,z)`²（https://www.rntz.net/post/2026-06-11-datalog-nontermination.html#fn-2）。 ## 2. 非确定性求值顺序允许声明式优化 我们已经看到了 `R(x) and test(x) and S(x)` 的三种可能的求值顺序。为什么非要毫无必要地承诺一种顺序呢？典型的数据库方法是通过不指定求值顺序来给查询规划器/优化器尽可能多的自由度。这意味着我们无法准确说出将在哪些值上调用 `test`，但我们可以**上下界**这个集合。类似地，程序终止从“是/否”问题变成“是/否/可能”。 回到我们的运行示例 `R(x) and test(x) and S(x)`，我们不能在没有某个 `x` 值的情况下调用 `test`。我们唯一的来源是 `R` 和 `S`；因此任何查询执行都会**最多**在 `R` 或 `S` 中的值上调用 `test`，并且**至少**在两者都包含的值上调用 `test`。如果 `test(x)` 对所有 `x ∈ R ∪ S` 都终止，那么我们的查询终止；如果它对某些 `x ∈ R ∩ S` 发散，那么查询发散；否则，它可能两种情况都出现。但所有终止的执行应该给出相同的结果。 不幸的是，我不知道如何以一种组合性的方式指定这种非确定性。有两种典型的语义方法：操作语义和指称语义。 操作语义方面，我不确定如何给出对应自底向上逻辑编程的语义，更不用说捕捉求值顺序变化了。特别地，在λFS中，有限λ如何求值？正常的程序式λ在应用于参数之前不会归约，但有限函数的全部意义就在于它们不会那样做；它们像数据库查询一样急切地被制成表。但如何在小步操作语义中捕捉这种行为并不明显。（Datafun确实有操作语义，但那只是因为使用了单子推导，这承诺了从左到右求值——正是我想要摆脱的！） 指称语义方面，自然的进展方式是在**有限函数式编程论文**（https://arxiv.org/abs/2604.26161）中概述的指称语义基础上，增加域理论和某种形式的非确定性。不幸的是，我对非确定性的域理论（幂域）还不够熟悉，不知道如何使其工作。 如果你认为你知道合适的方法，或者想一起研究这个问题，请给我发邮件（*[email protected]*，rot13（http://www.rot13.com/)）。 ## 3. “并行与”具有最声明式的行为 如果我们能鱼与熊掌兼得呢？到目前为止，我假设如果执行 `test(x)` 且它发散，那么我们的查询发散。这就是求值顺序重要的原因：它影响我们在哪个 `x` 上调用 `test`。如果我们允许自己思考得**不那么顺序化**，就可以放弃这个假设。 令 ⊥ 表示发散。典型的 `and` 实现是顺序的，首先检查左参数，如果结果为 `false` 则短路： ```python false and x = false -- 短路；不计算 x true and x = x ⊥ and x = ⊥ -- 我们从未有机会计算 x。 ``` 这很丑陋：逻辑合取是对称的，但这个 `and` 是左偏的。让我们在保持连续性的同时恢复对称性： ```python false and x = false -- 无需进一步计算 x true and x = x x and false = false -- 无需进一步计算 x x and true = x ``` 我称之为“并行与”，类似于Plotkin的“并行或”³（https://www.rntz.net/post/2026-06-11-datalog-nontermination.html#fn-3）。顺序“与”总是完全计算其左参数，但并行“与”同时计算两个参数，当任一参数为 `false` 或两者都为 `true` 时终止。这奇迹般地恢复了λFS的确定性。考虑我们之前的例子： ```python R := {"hello", "world"} S := {"hello", "alice"} test x := (x == "hello") or loop-forever() Q(x) := R(x) and test(x) and S(x) ``` 从左到右执行计算 `test("world") and S("world") = ⊥ and false`。对于顺序“与”，这会发散，但对于并行“与”，它简单地为 `false`。无论我们先遍历 `R`、先遍历 `S` 还是它们交集，我们都得到相同的直观正确结果：`Q = {"hello"}`。 不幸的是，如何高效实现并行 `and` 并不明确。然而，这并非完全不可能：例如，miniKanren（https://minikanren.org/）的搜索策略类似于并行或的实现，我听说Will Byrd（http://webyrd.net/）提到Andorra Prolog支持一种类似于并行与的合取形式。我自己在miniKanren 2025上发表了一篇论文（https://arxiv.org/abs/2510.26016），关于使用迭代器接口实现最坏情况最优连接的公平合取。所以我认为这个问题是可解的。但这值得吗？⁴（https://www.rntz.net/post/2026-06-11-datalog-nontermination.html#fn-4） ## 脚注 1. 更复杂的是，有两种不同类型的递归：(a) **递归函数**，它是惰性计算的——函数体只有在函数应用需要时才被计算；以及(b) **递归关系**（在λFS中，有限函数），在自底向上的关系式编程中，通过迭代到不动点急切地计算（我们从空关系开始，反复应用定义直到稳定）。但第二种可能可以用第一种来定义：递归足以定义迭代。↩（https://www.rntz.net/post/2026-06-11-datalog-nontermination.html#fnref-1） 2. 具体地，令 *edge* = {(1, *x*) : *x* ∈ [1..*n*]} ∪ {(*x*, 1) : *x* ∈ [1..*n*]}，其中 *n* 很大。那么三角形（查询的结果）是那些至少有两个变量（*x*,*y*,*z*）为1而另一个为[1..*n*]中任意值的三元组；因此共有 3*n*−2 个，即 Θ(*n*)。但是满足前缀 `edge(x,y) and edge(y,z)` 的三元组有 Θ(*n*²) 个。因此从左到右求值做了二次工作来找出线性结果。更一般地，从左到右求值对应于左深二叉连接计划，对于循环查询，已知二叉连接计划可能渐近低效：循环查询需要**最坏情况最优连接**（https://dl.acm.org/doi/10.1145/3180143）。↩（https://www.rntz.net/post/2026-06-11-datalog-nontermination.html#fnref-2） 3. 我认为“并行或”起源于Gordon Plotkin的《LCF Considered as a Programming Language》（https://homepages.inf.ed.ac.uk/gdp/publications/LCF.pdf）（1977），但我发现这些讲义（https://www.cl.cam.ac.uk/teaching/2526/DenotSem/DenSem-Notes.pdf）更易入门；参见第64页，§8.1，“完全抽象性的失败”。↩（https://www.rntz.net/post/2026-06-11-datalog-nontermination.html#fnref-3） 4. 另见与Meven Lennon-Bertrand的mastodon讨论（https://lipn.info/@mevenlennonbertrand/116658145724067149），他相当合理地质疑了我将布尔值上的并行或/与与公平逻辑编程析取/合取进行类比的正确性。↩（https://www.rntz.net/post/2026-06-11-datalog-nontermination.html#fnref-4）