William Byrd on "The Most Beautiful Program Ever Written" [PWL NYC]

William Byrd 先从 Scheme 中列表、符号、Lambda、环境和闭包逐步构造一个精简 Lisp 解释器，指出少数规则已能表达词法作用域、高阶函数和递归。随后他把解释语义写成 miniKanren 关系，反向执行同一关系来寻找满足输入输出约束的表达式与程序。程序合成因此成为对解释器语义的搜索和约束求解；其效率与可表达约束仍有限。

自动字幕 · 引文按字幕原文展示，可点时间戳回看片段。

视频章节 6

1. ▶ 0:00
   五行程序与解释器之美
2. ▶ 12:44
   Scheme 的列表和表达式
3. ▶ 30:52
   构造 Lisp 解释器
4. ▶ 48:50
   环境、闭包与递归
5. ▶ 63:12
   关系解释器和反向求解
6. ▶ 77:25
   约束驱动的程序合成

具体观点与证据 4

仅靠变量查找、函数构造与应用就能表达通用计算，数字与条件可另行编码。

讲者明确承认额外语法对效率和表达力仍有价值。

you only need these three lines that's turn complete actually

▶ 44:35–44:43 探索此观点 →

解释器的环境记录变量绑定，扩展环境使闭包保留词法作用域。

演示以高阶函数表示环境，也可换成数据结构表示。

the environment is going to contain somehow associations between variables and values

▶ 44:12–44:24 探索此观点 →

将解释器写成关系后，既可求输出，也可反求输入或补全缺失代码。

程序合成仍受搜索复杂度与给定约束质量影响。

even code or some mixture thereof we can put variables anywhere we want

▶ 75:01–75:12 探索此观点 →

局部程序与测试不相容可被证明，即使搜索尚不能合成完整程序。

不相容不说明一定是代码错，也可能测试或底层解释语义错。

the partially specified code you've written is actually incompatible with one of your tests

▶ 83:51–83:59 探索此观点 →

补充字幕原文 2

将关系解释器用于程序合成，可以从约束中推断缺失部分。

program synthesis so we have the ability

▶ 74:31–74:39

关系语义把等式看作双向约束，而非只有由表达式到结果的单向计算。

there's no direction to that equal sign

▶ 73:28–73:34

解读边界

演讲展示的是研究原型与示例，程序合成可能返回许多满足约束但不符合意图的程序；字幕说明运行时间约束当时尚不能直接表达，性能改进仍在进行。