💻 computer science

The Functional Machine Calculus III: Control

本文将功能机器演算从顺序计算扩展至分支与循环控制流，通过引入多操作数栈和延续栈的简单操作语义，实现了对包含条件、异常处理和迭代等特性的最小完备命令式语言的忠实嵌入，并保持了类型化终止性和合流归约等关键性质。

原作者： Willem Heijltjes

发布于 2026-03-03

📖 1 分钟阅读☕ 轻松阅读

原作者： Willem Heijltjes

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

这篇论文介绍了一个名为**“功能机器演算”（Functional Machine Calculus, FMC）的新理论，特别是它的第三部分：“控制”（Control）**。

为了让你轻松理解，我们可以把计算机程序想象成**“在厨房里做菜”，而这篇论文就是给这个厨房设计的一套全新的、超级灵活的烹饪规则**。

1. 背景：两个世界的冲突

在编程世界里，一直有两个“派系”在打架：

函数派（Functional）：像做数学题，讲究逻辑严密、结果可预测，但处理“副作用”（比如存数据、报错、随机数）很别扭。
命令派（Imperative）：像做菜，讲究步骤、顺序，可以随意修改食材（变量），但逻辑容易乱，很难证明程序一定是对的。

以前的理论（比如“单子 Monad"）试图把这两个派系强行融合，但往往像把油和水倒进一个杯子里，需要复杂的搅拌器（转换层），而且很难同时处理多种效果。

2. 核心创意：把程序看作“流水线上的传送带”

作者 Willem Heijltjes 提出了一个非常直观的想法：别把程序看作抽象的数学公式，把它看作一台机器在操作“传送带”（栈）。

以前的机器（Krivine 机器）：只有一条传送带。
- 推（Push）：把食材放上去。
- 拉（Pop）：从上面拿一个食材。
- 执行：把拿到的食材交给厨师处理。
这篇论文的升级：
1. 多条传送带（Locations）：以前只有一条带子，现在可以有很多条带子，分别叫“存储带”、“输入带”、“输出带”。你想存数据？去“存储带”拿。想打印？去“输出带”放。这就像厨房里有多个操作台，互不干扰。
2. 分支与循环（Control）：这是本文的重点。以前的传送带只能直直地走。现在，传送带上可以安装**“分岔路口”和“循环轨道”**。

3. 三大魔法：分支、异常与循环

这篇论文最厉害的地方，是用一种极其简单的方式统一了三种复杂的控制流：

A. 分支（Conditionals / If-Else）

想象你在传送带上放了一个**“路标”**。

如果路标显示“是（True）”，传送带就通向“做汤”的厨房。
如果路标显示“否（False）”，传送带就通向“做沙拉”的厨房。
创新点：在旧理论里，这很复杂。在这里，这只是一个简单的“选择标签”。程序走到这里，看一眼标签，自动滑向对应的分支。

B. 异常处理（Exceptions / Try-Catch）

想象传送带上的**“紧急出口”**。

如果在做菜时（程序运行中）发现食材坏了（出错），厨师可以扔出一个**“红色标签”**（异常）。
传送带会立刻停止当前的流程，顺着“红色标签”的指示，滑向“急救室”（Catch 块）。
创新点：作者把“异常”和“分支”看作同一种东西。异常就是一个特殊的“路标”，告诉程序：“别走这条路了，去那边！”

C. 循环（Loops）

想象传送带上的**“回旋轨道”**。

程序走到一个路口，如果标签是“继续（Loop）”，它就绕一圈回到起点，重新做一遍。
如果标签是“停止（Break/Return）”，它就冲出轨道，结束循环。
创新点：循环不再是复杂的递归定义，而是简单的“如果标签是 X，就绕圈；否则，就退出”。

4. 为什么这很牛？（简单总结）

极简主义：作者只用了几种最基础的指令（推、拉、选择、循环），就构建出了包含“存储、报错、随机数、循环、条件判断”的完整编程语言。就像只用“积木”和“胶水”就搭出了摩天大楼。
统一性：以前处理“报错”和“循环”需要完全不同的理论工具。现在，它们都是传送带上的“标签”和“轨道”。这让理论变得非常干净、统一。
安全性：这套系统自带“安全检查员”（类型系统）。
- 如果你试图在一个没有“出口”的循环里死循环，或者试图在一个没有“急救室”的地方扔“异常”，安全检查员会立刻发现并阻止你。
- 这保证了程序要么成功运行完，要么在出错前被安全拦截，绝不会“死机”或产生不可预知的后果（在特定条件下）。

5. 一个生动的比喻：乐高积木

想象以前的编程理论是**“乐高积木”**，但每种功能（存数据、报错、循环）都需要不同形状的积木，而且要把它们拼在一起非常困难，容易散架。

这篇论文提出的 FMC，就像是发明了一种**“万能连接件”**。

你想存数据？用连接件插到“存储口”。
你想报错？用连接件插到“出口”。
你想循环？把连接件弯成一个圈。
最重要的是：无论你怎么拼，只要符合连接规则（类型系统），整个结构就是稳固的、不会散架的，而且你可以清楚地看到每一步是怎么走的。

总结

这篇论文并没有发明什么复杂的“新魔法”，而是换了一个更聪明的视角：把复杂的程序控制流，还原成了最原始的**“传送带上的选择与循环”**。

它告诉我们，函数式编程（逻辑）和命令式编程（步骤）其实是一回事，只要我们把它们放在一个正确的“机器模型”里，它们就能完美融合，既灵活又安全。这对于未来设计更可靠、更智能的编程语言有着巨大的启发意义。

这篇论文《The Functional Machine Calculus III: Control》（功能机器演算 III：控制）由 Willem Heijltjes 撰写，发表于 MFPS 2025。它是功能机器演算（Functional Machine Calculus, FMC）系列的第三部分，旨在通过扩展之前的模型，将控制流（Control Flow）操作（如分支、循环、异常处理）无缝整合到统一的功能 - 命令式计算模型中。

以下是对该论文的详细技术总结：

1. 研究问题 (Problem)

在编程语言理论中，一个核心挑战是如何统一函数式编程（基于 $\lambda$ -演算，具有组合性、引用透明性和类型安全）与命令式编程（具有副作用、明确的执行顺序和控制流）。

现有的方法（如 Moggi 的 Monad、Levy 的 CBPV、Plotkin 和 Pretnar 的 Effect Handlers）虽然有效，但在组合多个效应（effects）时往往面临复杂性（如 Monad 的组合问题、Handler 的双层结构复杂性）。
之前的 FMC 工作（Heijltjes 2022）已经成功统一了顺序计算（Sequencing）和位置（Locations，用于建模存储、I/O 等），但尚未涵盖分支（Branching）和循环（Looping）控制流。
本文旨在解决如何在一个最小化、类型化且保持合流归约（Confluent Reduction）性质的演算中，自然地嵌入条件语句、异常处理和迭代循环。

2. 方法论 (Methodology)

作者采用操作语义（Operational Semantics）的方法，将 $\lambda$ -演算视为一种基于栈的抽象机器（Krivine Machine）的指令集，并对其进行扩展。

核心思想：将 Krivine 机器扩展为具有多个操作数栈（Operand Stacks）和一个续体栈（Continuation Stack）的机器。
- 操作数栈：用于建模副作用（如存储、I/O、概率），通过“位置”（Locations）区分。
- 续体栈：用于建模控制流（顺序、分支、循环）。
控制流扩展：
- 引入选择标签（Choice Labels, $i, j, k...$ ）：替代传统的 skip，代表计算的不同分支（如异常、退出码、数据构造器）。
- 条件组合（Case）： $M ; i \to N$ 。先执行 $M$ ，如果 $M$ 以选择 $i$ 结束，则继续执行 $N$ ；否则丢弃 $N$ 。
- 循环（Loop）： $M i$ 。只要 $M$ 以选择 $i$ 结束，就重复执行 $M$ ；否则终止。
语义模型：
- 小步操作语义：基于抽象机器的状态转换。
- 大步操作语义：描述完整的计算过程。
- 归约语义：定义了合流的归约关系（Reduction Relation）。
类型系统：引入基于和类型（Sum Types / Coproducts）的简单类型系统。类型被定义为内存类型向量之间的蕴含，输出类型被扩展为选择标签索引的和类型（ $\tau_I$ ）。

3. 关键贡献 (Key Contributions)

A. 语法与机器扩展

FMC 被扩展为包含以下六个核心构造：

变量 ( $x$ )
应用/压栈 ( $[N]_a. M$ )
抽象/弹栈 ( $a\langle x \rangle. M$ )
选择/标签 ( $i$ )
分支/Case ( $N ; i \to M$ )
循环 ( $M i$ )

B. 控制流的统一建模

论文展示了如何通过上述构造统一建模多种控制流机制：

异常处理：throw e 映射为选择 $e$ ；try M catch e N 映射为 $M ; e \to N$ 。
条件语句：布尔值被编码为选择标签（ $\top, \bot$ ），if B then M else N 通过 $B$ 的结果选择分支。
循环与跳出：while 和 do-while 循环通过循环构造 $M i$ 实现，break 和 return 通过不同的选择标签跳出循环。
代数数据类型：非归纳的数据类型（如常量、构造器）被建模为选择标签的和类型。

C. 类型系统与性质

简单类型系统：扩展了之前的类型系统，输出类型变为和类型 $\tau_I$ 。
类型保证：
- 进展性（Progress）：类型化的程序要么终止，要么可以执行一步。
- 终止性（Termination）：在没有循环构造（$Mi$）的情况下，类型保证机器终止。
- 强规范化（Strong Normalization）：在无循环且类型化的情况下，归约过程是强规范化的。

D. 理论证明

合流性（Confluence）：通过平行归约（Parallel Reduction）技术证明归约关系是合流的。
机器终止与强规范化：
- 使用可归约性（Reducibility）方法证明机器终止。
- 通过定义度量评估（Measured Evaluation），计算机器运行中的弹栈（pop）步骤数量，证明 $\beta$ -归约严格减少该度量，从而证明强规范化。

4. 主要结果 (Results)

最小且完整的命令式语言嵌入：FMC 成功嵌入了一种包含全局存储、异常处理、循环、条件语句和代数数据类型的完整命令式语言。
统一的语义：该模型同时支持：
- 直接的、直观的操作语义（基于机器）。
- 合流的归约语义（基于 $\lambda$ -演算风格）。
- 简单类型系统。
效应组合的简化：与 Monad 或 Effect Handlers 不同，FMC 通过栈操作和选择标签自然地组合了多种效应（存储、I/O、控制流），避免了 Monad 的组合难题和 Handler 的双层结构复杂性。
类型推断与安全性：类型系统能够捕捉异常处理、循环退出和分支逻辑，确保程序在类型检查后不会发生未捕获的异常或死循环（在无循环构造时）。

5. 意义与影响 (Significance)

理论统一：该工作为“函数式”与“命令式”范式提供了一个深刻的统一模型。它表明，控制流（分支、循环）和副作用（存储、I/O）可以被视为同一底层机器（多栈机器）上的自然指令，而非通过复杂的语义转换（如 Monad 变换）添加的额外层。
语义清晰性：通过“选择即值”（Exceptions-as-values）和“控制流即和类型”的视角，简化了异常处理和分支逻辑的语义理解。
形式化验证基础：由于保留了合流归约和强规范化性质，FMC 为验证包含复杂控制流和副作用的程序提供了坚实的理论基础。
未来方向：
- 论文提到正在研究将效应处理（Effect Handlers）引入 FMC，以支持更通用的代数效应。
- 探讨 FMC 中的“代数分支”与当前“控制扩展”之间的关系。
- 扩展支持归纳数据类型、递归和局部存储。

总结：
这篇论文通过引入基于选择标签的分支和循环机制，将功能机器演算（FMC）从顺序计算扩展到了完整的控制流计算。它不仅成功嵌入了一种完整的命令式语言，还保持了 $\lambda$ -演算的核心优良性质（合流性、类型安全、强规范化），为统一函数式与命令式编程范式提供了一个简洁、强大且形式化严谨的新框架。