逻辑程序的抽象机

# 逻辑程序的抽象机 来源：https://chisistyping.bearblog.dev/abstract-machines-for-logic-programs/ *2026年4月6日* \基于与 [Rob Simmons](https://typesafety.net/rob/about/) 的交谈。读者先决条件：熟悉推理规则、皮亚诺表示法（Peano notation）和状态机。\] 可以说，以下推理规则定义了加法：只要 `plus N M P` 成立，数字 `N` 和 `M` 之和即为 `P`。 `` ----------------- pz plus 0 N N plus N M P -------------------- ps plus (s N) M (s P) `` 利用这些规则，下面是一个推导 2 + 2 = 4 的过程： `` ----------------- pz plus 0 2 2 --------------- ps plus 1 2 3 --------------- ps plus 2 2 4 `` 推理规则集本身并非程序，它们只是关系的定义。若要利用我们的加法定义进行计算，我们必须将正在做的事情视为*搜索*一个数字 `X`，使得给定输入 `N` 和 `M` 时，`plus N M X` 成立。**逻辑编程**的目的是让我们能够将一组推理规则（或许连同查询一起）作为程序来“运行”。我们可以使用什么心智模型来逐步思考逻辑程序是如何运行的？ #### 栈机 下面是一个指定为状态机的程序，它评估形式为 `plus N M _` 的查询，其中 `N` 和 `M` 是已知的（在逻辑编程术语中，它们是*地基的/ground*，这意味着它们不包含需要求解的逻辑变量）： `` k >> plus 0 N _ |----> k << N k >> plus (s N) M _ |----> k; s _ >> plus N M _ k; s _ << N |----> k << s N `` 符号说明： - 机器的状态为： - `k >> q`（在栈 `k` 上评估查询 `q`），或 - `k << a`（向栈 `k` 返回答案 `a`）。 - 栈 `k` 是代表“计算下一步”的帧列表。对于此机器，我们唯一需要的帧是 `s _`，它指示我们加一。 - 要启动机器，配置状态 `[] >> plus N M`（其中 `[]` 是空栈），等待其进入配置 `[] << P`，并读取 `P` 作为结果。 我使用的语法旨在暗示推理规则中使用的关系表示法，并暗示逻辑编程语言可能使用这种类型的机器作为内部表示，推理规则可以被编译成这种表示。 在 `plus 1 2 _` 上的示例运行： `` . >> plus 1 2 _ |----> .; s _ >> plus 0 2 _ . ; s _ >> plus 0 2 _ |----> .; s _ << 2 . ; s _ << 2 |----> . << 3 `` #### 模式（Modes） 为了生成此机器，我们必须做出一个关键选择：**关系中的哪些位置是输入，哪些是输出？**这称为关系的**模式分配**。在上面的示例中，我们选择前两个位置作为输入，最后一个位置作为输出（分配模式 `i/i/o`）。然而，我们可以为 `plus` 关系选择其他模式，它们对应于不同的抽象机。 下面是一个栈机，它基于模式分配 `i/o/i` 实现减法。（你可能听说过人们声称逻辑程序可以“反向运行”；这就是其中一种含义。） `` k >> plus 0 _ P |----> k << P k >> plus (s N) _ (s P) |----> k; _ >> plus N _ P k; _ << P |----> k << P `` （这里我们实际上根本不需要栈，但为了统一性我们包含了它。） 步骤链示例： `` . >> plus 3 _ 4 |----> .; _ >> plus 2 _ 3 . ; _ >> plus 2 _ 3 |----> .; _ ; _ >> plus 1 _ 2 . ; _ ; _ >> plus 1 _ 2 |----> .; _ ; _ ; _ >> plus 0 _ 1 . ; _ ; _ ; _ >> plus 0 _ 1 |----> .; _ ; _ ; _ << 1 . ; _ ; _ ; _ << 1 |----> 4 . << 1 `` 注意，*此*抽象机可能会卡住： `` . >> plus 3 _ 2 |----> .; _ >> plus 2 _ 1 . ; _ >> plus 2 _ 1 |----> .; _ ; _ >> plus 1 _ 0 . ; _ ; _ >> plus 1 _ 0 |--/-> `` 这对应于自然数减法是一个偏函数（partial function）的事实。当我们以关系的形式编写事物时，其中之一就是我们不必担心部分性和非确定性。但一旦我们对将关系作为程序运行感兴趣，这些担忧就会出现。 但是，到目前为止，我们只是将*带模式的*关系转换为抽象机的状态转换，这或许稍微更“操作化”了一些，但它仍然是一个关系，只是状态和状态后继者之间的关系（在模式 i/o 下）。最终，我们希望将这个状态机视为全语言中的*函数*，这意味着要思考类型，但让我们再稍作等待。 我们还可以想象以另一种模式运行 `plus`：o/o/i。换句话说，给我所有和为 `P` 的数字对 `N,M`。以下是栈机。 `` k >> plus _ _ N |----> k << 0,N k >> plus _ _ (s P) |----> k; s _, _ >> plus _ _ P k; s _, _ << N , M |----> k << s N , M `` 此机器是非确定性的。以下是输入 `. >> plus _ _ 3` 的一次运行： `` . >> plus _ _ 3 . << 0 , 3 `` 另一次运行： `` . >> plus _ _ 3 . ; s _ , _ >> plus _ _ 2 . ; s _ , _ ; s _ , _ >> plus _ _ 1 . ; s _ , _ ; s _ , _ << 0 , 1 . ; s _ , _ << 1 , 1 . << 2 , 1 `` #### 读者和/或我在后续帖子中的练习：添加具有多个前提的规则示例。 #### 我们在做什么？ 如果你从事编程语言规范和实现的业务，这种转换是一件相当标准的事情：我们取各种被称为**大步骤（big-step）**或**自然（natural）**语义的东西，并将其转换为**抽象机**，类似于 Landin 的 SECD（https://doi.org/10.1093%2Fcomjnl%2F6.4.308）（尽管我们这里不关心 -ECD 部分；我直接从 Harper（https://www.cs.cmu.edu/~rwh/pfpl.html）那里继承了仅栈的表示法）。栈也可以被视为*延续（continuations）*的一阶表示，Reynolds 在最初的**定义性解释器（definitional interpreters）**论文中描述了这种联系（https://homepages.inf.ed.ac.uk/wadler/papers/papers-we-love/reynolds-definitional-interpreters-1998.pdf）。定义性解释器可以被视为我们最初给出的推理规则的最直接递归解释，但它们没有给我们表达关系完全通用性的能力，包括部分性和非确定性，顺便说一句，这些也是人们可能希望为编程语言实现的东西—— alongside 异常、效果处理器（effect handlers）、并发和其他有用的编程惯用语。抽象机是实现此目的的一种工具。 Reynold's 对表示为递归函数的定义性解释器执行这些转换的过程称为*功能对应（functional correspondence）*。 1992年，Hannan 和 Miller 描述了如何通过手工在任意逻辑程序上执行这些转换，以便可以正式验证其正确性：From operational semantics to abstract machines（https://www.lix.polytechnique.fr/~dale/papers/mscs92.pdf）。 2004年，Mads Sid Ager 确定了可以自动化此过程的逻辑程序片段：From natural semantics to abstract machines（https://scispace.com/pdf/from-natural-semantics-to-abstract-machines-4kgcst64qr.pdf）。 我通过 Simmons 和 Zerny（2013）（https://dl.acm.org/doi/10.1145/2505879.2505899）了解了这项工作，他们通过与 Reynolds 的*功能*对应进行类比，创造了*逻辑*对应（logical correspondence）一词，并将先前的结果扩展到**子结构操作语义（substructural operational semantics）**（https://www.cs.cmu.edu/~fp/papers/lics09.pdf）。 从我目前对文献的理解来看，这种可能性（以及在适当限定条件下自动化）的观察大多被框定为*编程语言的操作语义*作为主要应用。但是，“定义为推理规则集合的关系”的范围要大得多，特别是当你考虑到依赖类型语言的先进采用时，这些定义采取索引归纳定义（indexed inductive definitions）的形式。最近，我对该过程为其他类型程序所隐含的抽象机感到好奇。