Byrd Inverts Three-Line Lisp Core to Automate Code Synthesis

Byrd逆转三行Lisp核心实现代码自动合成 将极简的三行Lisp解释器转换为双向关系，使逻辑引擎能够反向执行，从而将标准求值转变为自动化程序合成。 Byrd深入剖析了Lisp解释器的基础三行核心——变量查找、lambda抽象和过程应用，认为这一极简结构才是真正的“软件领域的麦克斯韦方程组”。他梳理了该解释器从简单计算器演化为研究环境作用域与递归等编程语言语义的强大实验平台的过程。演讲的高潮在于展示了如何使用miniKanren将该元循环求值器编码为关系程序，从而实现自动化程序合成和quine（自产生程序）生成。 William Byrd展示了一个完备的、图灵完备的Lisp解释器可以精简为三个核心构件：变量查找、lambda抽象和函数应用。 (45:18) Alan Kay曾著名地将LISP 1.5手册第13页上的Lisp解释器誉为“软件领域的麦克斯韦方程组”，作为研究语言语义的可扩展实验室。 (5:27) 在miniKanren中将元循环求值器实现为关系型解释器，可将求值过程转变为双向约束问题，从而实现自动化程序合成和quine生成。 (61:02) 原型合成器Barliman借助优化后的miniKanren引擎，运行速度比朴素实现快约1000万倍，能够从零合成诸如append等完整的递归函数。 (75:08)

Computer scientist William Byrd argues that a minimal, metacircular Lisp interpreter encapsulates the foundational essence of computation. By interpreting the mathematical equality in its operational semantics bidirectionally, developers can transform basic evaluation into automated program synthesis and interactive verification. The Three-Line Foundation of Universal Computation (39:16) Drawing on Dan Friedman's index-card philosophy, Byrd demonstrates that a complete, Turing-complete call-by-value lambda calculus interpreter requires only three fundamental mechanisms: variable lookup, lambda abstraction, and procedure application. Auxiliary features like arithmetic, booleans, recursion primitives, and data structures are non-essential syntactic conveniences; arithmetic and conditionals can be Church-encoded, while recursive behavior can be derived via fixed-point combinators such as the "Poor Man's Y combinator." In Byrd's presentation, this core is realized through a higher-order design where both environments and closures are represented directly as host Scheme procedures. Bidirectional Semantics via Relational Interpreters (61:02) Traditional compilers and interpreters treat the equal sign as a unidirectional evaluation arrow, executing source expressions left-to-right to produce terminal values. In contrast, Byrd, Friedman, and collaborators developed miniKanren to implement the operational semantics of Lisp as an executable, bidirectional mathematical relation. In approximately 43 lines of code, this relational evaluator (eval-expo) allows any parameter—whether the input expression, the environment, or the output value—to be replaced by an unknown logic variable. Program Synthesis and Quine Generation (69:02) Running the relational interpreter backward turns program execution into automated program synthesis. When constrained to match a specific output, the engine synthesizes expressions that evaluate to that result, generating solutions ranging from simple quoted data to thunks and structural extractions. When tasked with John McCarthy's classic challenge of finding an expression whose value equals itself—a quine—the query (eval-o e e) immediately generates trivial self-evaluating constants as well as complex, higher-order quines featuring quotes and closures without manual hints or Gödel-numbering schemes. Test-Driven Synthesis in Barliman (75:08) To handle larger search spaces, Byrd and his collaborators developed Barliman, a specialized tool pairing an optimized relational engine—running roughly 10 million times faster than naive miniKanren—with a graphical interface. To prevent the search engine from "cheating" by hardcoding constant responses, developers supply multiple input-output examples and utilize generated symbols (gensyms) that cannot appear literally in the synthesized code. Beyond full synthesis, Barliman functions as a continuous proof engine during test-driven development: as a developer types partial code with unfilled holes, the underlying relational engine checks consistency against test cases in real time, immediately flagging when a partial implementation is provably incompatible with the specifications. While relational interpreters turn programming into a flexible constraint-solving system, Byrd notes significant technical frontiers remain. Current implementations can infer program structures and leverage syntactic priors to prune search spaces, but they cannot yet synthesize code under meta-constraints such as asymptotic time complexity or strict memory bounds.

William Byrd 在演讲中指出，仅需变量查找、lambda 抽象与过程调用这三行核心规则的 Lisp 元循环解释器，便构成了图灵完备的计算基石；若将其中的等号视为无方向的数学双向关系，解释器即可转化为能够逆向推导代码、生成 Quine 与辅助证明的程序合成引擎。 极简核心与三行图灵完备解释器 (55:08) Byrd 继承了 Dan Friedman 将深刻计算思想压缩在 3x5 或 4x6 英寸卡片上的哲学，探讨了仅用 Lisp 编写 Lisp 的元循环解释器。尽管大多数程序员习惯为语言填充算术运算、条件分支和丰富数据类型，但 Byrd 证明这些非核心结构都可以被剥离或通过丘奇编码（Church encoding）替代。语言的真正骨架仅包含三行核心规则：变量查找、lambda 抽象以及过程调用。结合高阶环境（Higher-Order Environment）的设计，环境自身便是一个接受变量名并返回绑定的过程，未绑定的标识符则触发错误。通过 Dan Friedman 的“穷人 Y 组合子”（Poor Man's Y combinator），该极简内核无需内置 define 或 letrec，即可通过自应用实现阶乘等递归计算，其图灵完备机制甚至先于图灵机概念的确立。 破除等号单向性：从求值到关系式推导 (61:02) 常规编译器与解释器普遍将等号视为单向评估箭头，即左侧表达式求值化简为右侧数值。Byrd 强调数学上的等号完全具备双向对称性。借鉴 John McCarthy 在 1960 年代对 Lisp 求值规则的规范，Byrd 与合作者历时十余年，在嵌入式逻辑编程语言 miniKanren 中将操作语义直接翻译为一个仅约 43 行 Scheme 代码的关系解释器 eval-expr-o。在该模型下，程序执行转变为解代数方程：系统既能正向计算表达式的值，也能固定输出反解输入，或在程序各处引入逻辑未知数进行双向联合求解。 逆向程序合成与消除字面量漏洞 (75:08) 将求值器运行在逆向模式下即可实现自动程序合成。例如固定输出为 '(I want milkshake)，解释器会自动生成引用列表、零参 thunk 调用或 car 解构等多种合法表达式；输入 McCarthy 提出的自求值难题 (eval-o e e)，引擎除列举数字与布尔值等自求值原子外，能无先验提示地合成非平凡的 Quine。然而逻辑求解器类似“许愿神仙”，倾向于寻找最省力的漏洞——当试图逆向推导列表连接函数 append 时，若测试用例不充分，求解器会直接合成忽略参数并硬编码返回结果的常数函数。为迫使其生成包含 null?、car、cdr 和 cons 的通用递归逻辑，必须提供多组约束，并采用运行时互不冲突的生成符号（gensym）杜绝字面量作弊。 连续证明引擎与交互式测试驱动开发 (81:12) 为克服原生 miniKanren 解释器搜索过慢的瓶颈，Byrd 与团队构建了后端性能提升约一千万倍的交互工具 Barliman。在集成开发环境中，开发者可以编写带有未知“空洞”的部分代码并补充输入输出测试用例。后台引擎持续消耗处理器核心充当定理证明器：一旦用户填入错误的变量或设计了冲突的分支结构，系统能实时判定当前不完整代码与测试集在逻辑上不相容并即时报错。该范式将测试驱动开发演进为连续的形式化证明过程，辅以简单的语法结构先验概率（例如 define 通常包裹 lambda，lambda 内部常接条件语句），从而大幅剪枝搜索空间。 该研究证明了操作语义与关系编程深度结合的潜力，但 Byrd 坦承目前的程序合成系统主要依托输入输出示例与词法作用域约束，尚无法指定时间复杂度（如 O(1)）或空间界限（如 O(N)）等元级计算成本约束，这仍是程序合成领域有待攻克的关键方向。

## Background 本视频由 YouTube 频道 PapersWeLove 于 2017 年 5 月 24 日发布，记录了在纽约举办的技术分享活动。页面简介指出，犹他大学的研究副教授 William E. Byrd 在演讲中深入探讨了他心目中“有史以来最美丽的程序”——用 Lisp 编写的 Lisp 元循环解释器，并解析了围绕该解释器展开的诸多惊人思想与前沿延伸。 ## TL;DR William Byrd 从师从 Daniel Friedman 的经历切入，现场演示了如何在 Scheme 中逐步构建出一个基于高阶表示的微型 Lisp 解释器，并展示其如何被浓缩为仅有三行核心规则（变量查找、Lambda 抽象与函数调用）的图灵完备程序。随后，Byrd 将视角从传统的单向求值推向数学与逻辑上的双向对称关系，揭示了“认真对待等号”的深层含义。通过基于 miniKanren 的关系式解释器及其衍生工具 Barliman，演讲生动展示了代码逆向推导、自产生程序（Quine）的自动生成、完形填空式的程序合成，以及后台实时定理证明等突破性应用。 ## Atmosphere & style 整场演讲洋溢着纯粹的极客热忱与学术幽默，Byrd 举重若轻地在白板式现场编码与深刻的数理哲学反思之间自如切换。他频频用“奶昔”、“极客战栗（nerd chills）”以及调侃 Haskell 程序员的俏皮话打破高深理论的距离感，让现场充满阵阵会心的笑声。随着代码从几行极简规则一路演化到惊人的程序自动合成，观众在轻松欢快的氛围中体会到计算本质的震撼之美。 ## Bulletin - [05:27](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=327s) William Byrd 探讨了被称为“软件领域麦克斯韦方程组”的 Lisp 元循环解释器，指出只需保留变量查找、Lambda 抽象与过程调用三行核心规则，即可构成图灵完备的微型求值器。 - [01:01:02](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=3662s) 通过在逻辑编程语言 miniKanren 中将求值器重新实现为双向关系，传统的单向代码执行被转化为代数约束求解，使得系统能够逆向求解输入、枚举 Quine 乃至自动合成程序。 - [01:17:21](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=4641s) 基于该理论开发的程序合成工具 Barliman 结合了剪枝优化与 Gensym 机制，搜索速度相比原生版本提升约 1000 万倍，可在交互式测试驱动开发中实时证明不完全代码与测试用例之间的逻辑不兼容。 - [01:27:36](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=5256s) 研究团队最新的初步实验表明，通过在关系式解释器中融入人类常见的 AST 父节点惯用模式（如 lambda 内部倾向于嵌套 if/cond），能将程序合成效率提升数个数量级。 ## Key takeaways - [02:33](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=153s) 自认为完全掌握某项经典概念是程序员最危险的思维定势，正如仅有几行规则的考拉兹猜想（3n+1）至今仍难倒顶尖数学家一样，极简代码同样蕴含极深的理论复杂度。 - [05:27](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=327s) Alan Kay 将写在《LISP 1.5 Programmer's Manual》第 13 页的 Lisp 元循环解释器誉为“软件领域的麦克斯韦方程组”，其微小的体积承载了 CPS 变换、定界续体以及可变状态等海量语言特性的衍生可能。 - [08:30](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=510s) 反思解释塔（Reflective Towers of Interpreters）构建了多层相互解释的架构，下层解释器可向上访问并修改上层机制以在运行时改写自身语义，展现了元循环解释器极致的理论演化方向。 - [12:40](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=760s) 嵌套列表本质上就是树形结构，而递归是处理树最自然的手段；Lisp 的同音异义性与 S-表达式让程序能够以最纯粹的形式自如修改与操作自身。 - [34:02](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=2042s) 测试解释器时必须严格为输入代码包裹 quote（引用），避免测试表达式在外层宿主 Scheme 环境中被提前求值，从而产生解释器已实现特定特性的假象。 - [39:16](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=2356s) 算术操作和条件分支在理论上都是可以剔除的语法糖，图灵完备解释器的最核心精髓仅由三行构成：变量查找、Lambda 抽象生成闭包以及过程调用。 - [49:10](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=2950s) 在高阶表示的解释器中，环境与过程闭包本身均被表示为 Scheme 的高阶函数，变量寻值被精简为调用环境函数 (env var)，未命中则向父闭包递归转发。 - [59:38](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=3578s) 约翰·麦卡锡在论文中写下的 value(e, r) = v 中的等号往往被传统编译器视为从左到右的单向流动，但严肃对待等号的数学双向对称性是打破传统计算范式的关键。 - [01:01:02](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=3662s) 在 miniKanren 中实现的 43 行关系型解释器 eval-expo 消除了输入与输出的界限，支持通过指定结果来逆向推导代码或输入参数，例如秒解 Quine 与列表拆分组合。 - [01:13:56](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=4436s) 将关系型解释器中任意代码位置替换为未知逻辑变量，系统便跨入程序合成领域；面对逻辑系统如“狡黠精灵”般钻空子硬编码常量的行为，需通过扩充测试集与 Gensym 施加结构性约束。 - [01:21:55](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=4915s) Barliman 界面不仅能基于输入输出示例自动合成递归算法，其后台运行的 miniKanren 还能作为定理证明器，在用户敲入冲突代码的瞬间在数学层面上证明不一致性并实时拦截。 - [01:29:52](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=5392s) 关系式程序合成在搜索未知变量时并非盲目枚举，而是由解释器内置的环境作用域（如 letrec 绑定）动态约束其候选空间，使递归调用自然纳入候选分支。 ## Detailed walkthrough ### [00:00](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=0s) 从中学生涯到印第安纳大学：五行改变人生的代码 演讲者 William E. Byrd（昵称 Will）回顾了自己的经历：他曾做过初中老师、开办过夏令营，后来拿到计算机科学学位并成为一名 Java 工程师。由于厌倦了 Java 和 JavaScript 琐碎的开发日常，他决定前往印第安纳大学（Indiana University）攻读研究生，跟随 Daniel P. Friedman 教授学习。Dan Friedman 撰写了著名的经典教材《The Little LISPer》（以及修订版《The Little Schemer》、《The Seasoned Schemer》），后来两人还共同合著了《The Reasoned Schemer》。在 Will 入学第一学期的前几周，Dan 向他展示了一段彻底改变他一生的极简代码。 Will 直言，过去十二三年来他一直在试图真正参透这“短短五行代码”，甚至做好了将余生全部投入去理解其深远影响的准备。与那些热衷于编写包含十万行代码的编译器或两百万行操作系统内核的工程师不同，Will 坦言自己更偏爱极其精炼、高度抽象的极简设计。 - **卡片哲学**：Dan Friedman 推崇一种“3x5 英寸卡片”（或 4x6 英寸卡片，折算大约相当于 A4 纸的一小角）的思考法则——如果无法把一个核心思想浓缩在一张 4x6 的卡片上，说明你想得还不够透彻，必须“think harder”；一旦成功提炼到 3x5 卡片上，就可以基于它写出一本小册子。 - **震撼体验**：这段核心程序每每被 Will 回想起来，依然会让他激动得浑身泛起“nerd chills（极客战栗）”。 --- ### [02:33](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=153s) 所谓“理解”的危险陷阱与考拉兹猜想（Collatz Conjecture） 面对现场众多熟知 Lisp、刷过 SICP（《计算机程序的构造和解释》）、写过很多解释器并对 Lambda 演算有所了解的资深开发者，Will 坦言自己作这场报告十分忐忑。他指出，随着编程年限增长，程序员最容易陷入一种致命的心态，即自认为已经彻底弄懂了某个经典结构，觉得它再也变不出什么新花样： > “And that's the most dangerous way of thinking is to think you understand something right and that there are no kind of new tricks in this.” —— William E. Byrd 他习惯每隔两三年便回过头去重新审视那些很早以前就学过且以为掌握了的旧概念，却几乎总能从中发现全新的观察视角。在计算机科学及任何深奥的学科中，真正伟大的思想都具备多面性。 为了证明极其简短的程序同样能蕴含无穷无尽的深奥复杂度，Will 举了著名的“考拉兹猜想”（Collatz Conjecture，即 $3n+1$ 问题）作为类比：一个只有两三行乘除与加法的简单函数，数十年来全世界顶尖的数学家竭尽全力都无法证明它对于任意正整数输入是否一定停机。传奇数学家保罗·埃尔德什（Paul Erdős）曾对此感慨道：“数学还没有准备好应对考拉兹问题。”连三行算术代码都能难倒历史上最伟大的数学大脑，这也警戒着人们必须对“写在 3x5 卡片上的极简程序”抱有足够的敬畏之心。 ```mermaid flowchart TD accTitle: Collatz Function Complexity accDescr: 一个简单的 3n+1 规则展示了极简代码可能具备的惊人数学深度与停机复杂性。 Start["正整数输入 n"] --> Check{"n 是否为 1？"} Check -->|"是"| Stop["停机终止"] Check -->|"否 (偶数)"| Div["n / 2"] Check -->|"否 (奇数)"| Mul["3n + 1"] Div --> Check Mul --> Check ``` --- ### [05:27](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=327s) Lisp 元循环解释器：软件领域的麦克斯韦方程组 Will 随后引出了本次分享的核心主角：用 Lisp 本身编写的 Lisp 解释器（即“元循环解释器”）。初涉 Lisp 的人往往会被满眼的括号所困扰，继而纠结于 `lambda` 究竟是什么、嵌套两层 `lambda` 又是何用意；但在一步步手动跟踪执行追踪、弄清求值语义后，人们就会开始对解释器进行改写与把玩。这个解释器最美妙的地方在于，它是进行编程语言实验的完美实验台，具备近乎无限的可扩展性与衍生性： - **程序变换的“诱导剂”**：Will 把续体传递风格（Continuation-Passing Style, CPS）形容为程序变换界的“入门毒品（gateway drug）”。只要把解释器转化为 CPS 风格，就能大展身手；如果做“二次 CPS 变换（CPS it twice）”，便能自然导出定界续体（Delimited Continuations）。 - **语言特性的极简扩展**：在解释器参数中增加一个 `store`，就能轻易引入 `box`，实现可变状态（mutation）和副作用；还能极其轻松地自由切换传值调用（Call by Value）、按需调用（Call by Need）与传名调用（Call by Name）。 Will 指出，整个计算机科学界没有任何其他构件能像这套解释器一样，以如此微小的体积承载如此繁多的思想。面向对象编程先驱艾伦·凯（Alan Kay）在早年翻到《LISP 1.5 Programmer's Manual》第 13 页底部时，被那段用 Lisp 写出的 Lisp 解释器深深震撼，甚至改变了自己的一生，并感叹它就是“软件领域的麦克斯韦方程组（Maxwell's equations of software）”： > “These are Maxwell's equations of software.” —— Alan Kay 就像经典物理中把前人总结的四道优美电磁方程写在一张卡片上、花上一生去体会其衍生含义一样，Lisp 解释器在计算领域同样扮演着这一角色。 --- ### [08:30](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=510s) 反思塔、类型推断与“来自上帝之书的代码” 为了展现该程序令人惊叹的发展方向，Will 提到了更为深奥的奇特结构——反思解释塔（Reflective Towers of Interpreters）：底层解释器被上一层解释器解释，上一层又被再上一层解释，构成多层乃至无穷高度的解释塔。其极其迷人却又烧脑的机制在于：被解释的下层解释器能够反向“向上触及”正在解释它自身的上层解释器，并通过修改上层解释器的执行机制，在运行时动态改写自己本身的语义。Dan Friedman 甚至公开表示自己拒绝再碰反思塔，因为那“太烧脑了（melted his brain too much）”，是他明确立誓不再触碰的领域。对此有兴趣的读者可以参考浅井健一（Kenichi Asai）的研究，以及 Nada Amin 在 Strange Loop 上题为《Programming Should Eat Itself》的主题演讲。 ```mermaid flowchart TD accTitle: Reflective Tower of Interpreters accDescr: 无穷反思塔中底层解释器向上访问并改变自身语义的执行关系。 subgraph ReflectiveTower["反思解释塔 (Reflective Tower)"] L3["更高层解释器 (Level N)"] L2["上层解释器 (Level 2)"] L1["底层解释器 (Level 1)"] L3 -->|"逐层解释运行"| L2 L2 -->|"解释并驱动执行"| L1 L1 -.->|"反射修改 (改变自身语义)"| L2 end ``` 这种前沿探索即便让 Lambda 演算的资深专家思考其推论时，脸上都会泛起恐惧的神色。除了反思塔，元循环解释器还可以向类型推断系统延伸：使解释器与类型推断器共享同一个核心 AST 结构并产生紧密交互。正如 CPS 是代码变换的 gateway drug 一样，“Lisp in Lisp”正是领略整个程序设计语言宏伟世界的 gateway drug。 Will 表示，在接下来的时间里，他将现场带领大家以 Dan Friedman 的方式重新编写这个 Lisp 解释器。这里他引用了数学家保罗·埃尔德什的浪漫传说：上帝有一本珍藏了宇宙间所有最完美证明的“天书（The Book）”；而在软件世界里，这几行 Lisp 元循环解释器，正是那段理应收录于天书之上的极致神作。 ### [11:15](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=675s) “书中的程序”与 S-表达式入门 William Byrd 引用了数学家保罗·埃尔德什（Paul Erdős）关于“上帝之书”的典故：每当数学家发现一个极其优雅美丽的证明，就会感叹这是收录在“天书”（the Book）中的证明。Byrd 指出，他当晚要展示的正是这样一段“天书中的程序”。Byrd 直言：“I've written hundreds of interpreters and I've read lots of books on interpreters, but this to me is the one in the book. Everything else is a pale imitation.”（我写过成百上千个解释器，也读过无数关于解释器的书籍，但在我看来，唯独这个是收录在天书里的程序，其他一切不过是拙劣的仿作）。 为了让全场跟上节奏，Byrd 询问台下有多少人熟悉 S-表达式（symbolic expressions）或能够看懂括号，结果举手的大约只有一半。Byrd 安慰大家不用担心，他会亲自演示教学。他提醒听众，这篇论文蕴含着极其深邃的思想，今晚即便只是浮光掠影地扫视，也可能会让人感到“眩晕”；若真的觉得头晕，不妨“闭上双眼、身体前倾，房间就会停止旋转”。他保证，一旦大家对这个概念有了感知，就会被一种狂热的激情所点燃，想要把其余的所有细节全部搞懂，甚至可以在演讲后一起喝着奶昔深入讨论。 - 核心演讲主题：“天书中的程序”——用 Lisp 编写的 Lisp 元循环解释器（metacircular interpreter）。 - 现场受众基础：现场大约只有 50% 的听众熟悉 S-表达式和 Lisp 语法。 --- ### [12:40](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=760s) Chez Scheme 的交互体验与树状数据结构 Byrd 解释道，Scheme 是 Lisp 的一种方言，而 Lisp 的名字正是源自“表处理”（List Processing）。他打开了信赖已久的 Chez Scheme（现已遵循开源许可证）。他特别强调了 Chez Scheme 的交互式顶层环境叫做 REPL，并幽默地纠正其发音是“reppel”而不是“reple”。Chez Scheme 的卓越之处在于，即使用户只是在终端里交互式输入表达式，系统也会在后台即时将其直接编译为机器码；Chez Scheme 会预先进行分析，判断是直接求值更快，还是先编译再求值更快。 ```mermaid flowchart TD accTitle: REPL Evaluation Flow accDescr: Flowchart illustrating how Chez Scheme processes input expressions either by direct evaluation or by compiling on the fly to machine code. subgraph REPL ["Scheme REPL (Read-Eval-Print Loop)"] Input["输入 S-表达式 (例如 5, (+ 2 3))"] --> Analysis{"速度判定分析"} Analysis -->|"直接求值更快"| Eval["直接求值 (Evaluate)"] Analysis -->|"编译后执行更快"| Compile["即时编译至机器码 (On-the-fly Compile)"] Eval --> Output["输出结果"] Compile --> Output end ``` 随后 Byrd 带领观众认识最基本的数据构成：纯数字 `5` 求值得到 `5`；包含数字的列表 `(5)` 则由优美的圆括号包裹；包含两个元素的列表 `(5 6)` 绝不会被“逗号等杂物玷污”。列表内部还可以嵌套列表形成 `((5))` 乃至更深层次的结构。Byrd 指出，“嵌套列表”在计算机科学里的另一个名字就是“树”（tree）。他顺带调侃了技术发展史：现在的 XML 以及更早的 SGML，其用于树结构样式转换的语言除了 XSLT 之外，SGML 时代还有一个名为 DSSSL（Document Style Semantics and Specification Language）的语言，而 DSSSL 本质上就是 R4RS Scheme。树是一种归纳定义的数据类型，处理树的最自然方式就是递归（recursion）。大多数程序天然就是树形结构，如果想要一种能够自如修改和操作程序的编程语言，基于树与递归的 Lisp 是无可比拟的。 - 推荐学习资源：Andrew Plotkin（网名 zarf）编写的互动小说游戏《Lists and Lists》，玩家在游戏中由一位神灯精灵指导学习 Scheme 编程，甚至能在其中实现逻辑编程系统（受限于 Z-machine 的内存上限）。 - 语法纯粹性：列表元素以空格分隔，完全省略了主流语言中的逗号分隔符。 --- ### [17:03](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=1023s) 逻辑值、引用（Quote）与符号（Symbol） 在 Scheme 的类型系统中，布尔值真表示为 `#t`，假表示为 `#f`。Byrd 调侃道：“#t is a representation of truth; there is no representation of beauty, but we have #f which is a representation of false.”（`#t` 代表真理；虽然没有代表美丽的符号，但我们有代表虚假的 `#f`）。Scheme 规定，除了 `#f` 之外，系统内的所有值在条件上下文中都会被视为真（例如数字 `5` 也是真）。 随后 Byrd 引入了一个极其深邃且引发诸多理论争议的运算符——`quote`（引用）。`quote` 的作用是原样返回其包裹的内容，阻止求值。由于数字 `5` 是自求值字面量（self-evaluating literal），`quote 5` 依然是 `5`；但对于列表 `(5 6)` 或空列表 `()`，使用 `quote` 可以直接获得其字面数据。为了避免繁琐的输入，Scheme 引入了单引号语法糖，即 `'(5 6)`。 除了数值、布尔值和列表，Lisp 还有一个至关重要的一等公民类型——“符号”（Symbol）。Byrd 针对面向对象语言打趣道：“If you program in Java, I'm sorry, you don't get symbols.” 符号（如 `'milkshake`）既不是变量名，也不是字符串，而是一个表示概念的不可分割的原子值（atomic value）。在 Scheme 底层，符号之间的比较在指针级别极快，因此非常适合用于表示具有特定语义的数据实体，而无需像 C 语言那样用冷冰冰的数字常量来充当枚举。 --- ### [19:48](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=1188s) 谓词、Cons 构造器与分支条件（if / cond） 在操作列表与数据时，Byrd 介绍了基础谓词（predicate）。Scheme 的函数调用均采用前缀表达式，例如 `(null? '())`。以问号结尾是 Scheme 命名谓词的约定，此表达式判断传入参数是否为空列表并返回 `#t`，而 `(null? 5)` 则返回 `#f`。 接着，Byrd 讲解了如何构造列表结构。除了直接引用字面量或调用 `(list 3 4 5)` 外，最核心的底层运算符是 `cons`（意为 Construction）。Byrd 回忆道，他的博士导师 Dan Friedman 曾与 David Wise 在 1976 年合作发表了具有里程碑意义的论文《CONS Should Not Evaluate Its Arguments》，奠定了类似 Haskell 中的惰性求值思想；随后 Henry Baker 还撰写了一篇标题极具双关戏谑风格的论文《CONS Should Not CONS Its Arguments》。基础的 `cons` 接受两个参数，把一个新元素链接到现有列表的头部，例如 `(cons 5 '())` 产生 `(5)`，而嵌套的 `(cons 6 (cons 5 '()))` 则构筑起链表结构。 ```mermaid flowchart LR accTitle: Cons Memory Structure accDescr: Diagram illustrating how cons pairs construct a linked list of two elements: six and five. subgraph ConsCells ["内存中的 Cons 对 (Pair) 结构"] C1["cons cell 1"] C2["cons cell 2"] N["'() (空列表)"] C1 -->|"car (数据)"| D1["6"] C1 -->|"cdr (后续)"| C2 C2 -->|"car (数据)"| D2["5"] C2 -->|"cdr (后续)"| N end ``` 在程序控制流方面，Byrd 演示了条件分支的基本形态： 1. `if` 表达式：由测试表达式、后继表达式（consequent）与替代表达式（alternative）三部分构成。例如 `(if (null? 5) 6 7)` 的求值结果为 `7`。 2. `cond` 表达式：用于消除深层嵌套 `if` 所带来的混乱。每个分支由条件与结果配对组成，系统会按顺序检索首个满足条件的分支。 此外，Byrd 还展示了 Scheme 的基本算术函数（如 `+` 和 `*`），它们本身是绑定到具体计算过程的普通函数对象，并原生支持大整数（bignums）的任意精度计算。最后，他引出了定义变量和函数的 `define` 操作符。 ### [23:37](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=1417s) 变量绑定、环境与 Lambda 表达式 William Byrd 继续讲解 Scheme 的基本概念，首先通过 `define` 为值赋予名称。为了举个生活化的例子，他提到自己刚刚喝了一杯香芋奶茶，于是写下 `(define taro 'good)`，将符号 `'good` 绑定到名称 `taro` 上。随后他在 REPL 中输入 `taro`，系统便会在“环境”（environment）中查找该变量，并返回其值 `'good`。通过这一操作，Byrd 说明了 `define` 的本质：为一个值赋予名称，无论这个值是符号还是其他类型。 ```mermaid flowchart LR accTitle: 变量求值流程 accDescr: 展示在 REPL 中输入变量名后通过环境查找其值的基本求值流程 subgraph EvalProcess["求值流程"] Input["输入: taro"] Env["环境 (Environment)<br/>taro ↦ 'good"] Output["返回值: 'good"] Input -->|"查找变量"| Env Env -->|"取得绑定值"| Output end ``` 接着，Byrd 引入了“函数”（或者严格来说叫“过程”，procedure）的概念，在 Scheme 中使用核心表达式 `lambda` 来创建。在终端里，他的编辑器自带排版替换功能，将输入的 `lambda` 自动显示为数学符号 $\lambda$。Byrd 解释道，一个 `lambda` 表达式包含形参列表（formal parameters）和函数体（body）。例如，恒等函数写作 `(lambda (x) x)`，Byrd 念作 “Lambda x x”，它的功能仅仅是返回传入参数的值。 在 Scheme 中，外层圆括号通常表示过程调用（procedure call），除非首位置出现诸如 `quote` 或 `define` 这样的“特殊形式”（special form）。Byrd 展示了将恒等函数应用于参数 `5` 的全过程： - 运算符表达式（operator，常称作 “rator”）求值为一个接受单参数的过程； - 操作数表达式（operand，常称作 “rand”）求值自身（即数值 `5`）； - 运行时执行过程应用（procedure application），将求得的过程应用到求得的实参上，最终返回结果 `5`。 Byrd 强调了“表达式”（expression）与“值”（value）之间的关键区别，并指明这套操作数与运算符求值并应用的机制，正是他们接下来要亲手实现的解释器核心。 随后，Byrd 定义了一个名为 `double` 的过程。在演示时，他打趣说：“I can double my fun”，结果引发了错误，他笑着调侃 Haskell 程序员肯定会因此找他麻烦（“The Haskellers are going to give me grief”）。接着他测试了对 `5` 进行双倍运算。Byrd 还进一步展示了 Scheme 的灵活性甚至危险性：他执行了 `(define define 5)`，将关键字 `define` 自身重定义成了整数 `5`。面对观众的反应，Byrd 解释说：“I can do a lot more than that. I can change what Lambda means and things like that; that's where the real fun begins.” 不过他打住话题，重启了 Scheme 交互环境，并开玩笑对台下说大家还没准备好见识那样的魔法：“You're not ready yet.” --- ### [27:11](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=1631s) 宏系统与 Pmatch 模式匹配 Byrd 对听众说，大家现在已经掌握了 Scheme 的基本要素；虽然听上去像句玩笑，但写解释器真正需要的基础知识就只有这么多。在正式动手之前，他还想引入一个虽然不属于标准 Scheme、但极易通过宏（macro）扩展出来的工具——模式匹配宏 `pmatch`。Scheme 拥有极为强大的宏系统，允许开发者自由扩展语言语法。 Byrd 加载了 `pmatch` 宏，并解释它的设计精神与条件分支 `cond` 类似，但它不是判断布尔条件，而是针对表达式的结构进行匹配。他现场演示了一个例子：对表达式 `(list 3 4)` 进行模式匹配，匹配的模式形式为 `(,x,y)`。Byrd 说明，虽然无需深究逗号在语法层面的全部细节，但可以直观理解为这个双元素模式与传入的列表相匹配，从而使变量 `x` 绑定到 `3`，`y` 绑定到 `4`。匹配成功后，右侧的表达式 `(+ x y)` 便可使用这些绑定变量，顺利计算出结果 `7`。 Byrd 指出，模式匹配非常强大，尤其在与 Scheme 的“准引用”（quasiquotation，即反引号 `` ` ``）和“去引用”（unquote，即逗号 `,`）结合使用时。在 `pmatch` 内部，实际上隐式包含了这种准引用的反解机制。 --- ### [29:10](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=1750s) 构建解释器骨架：从命名到 Eval-expr 具备了所有预备知识后，Byrd 切换回代码文件开始编写解释器。在着手写逻辑前，面临的第一个难题是起名字：“One thing that we need to do is, you know, decide on the name for our interpreter. That's the hard part, right? So names are hard.” 台下一位观众提议命名为 `Fitzroy`。Byrd 跟着打趣并记下：“Define Fitzroy... All right, so we have a name. This is our life now, and thank you, derailed us all.” 玩笑过后，Byrd 询问大家下一步该写什么。有人回答 `pmatch`，Byrd 指出还差一步：必须先定义接收参数的过程，而“当心存疑虑时，答案永远是 Lambda”（“When in doubt, the answer is Lambda, right?”）。由于调用求值器时传入的是一个待求值的表达式并期望返回其值，Byrd 决定将这个函数命名为 `eval-expr`（尽管他觉得叫 `Fitzroy` 也不错）。Byrd 特别给出了一条安全提示：绝不能把形式参数命名为 `exp`，因为 Scheme 自带求以 $e$ 为底的指数函数 `exp`，一旦参数名与内置函数冲突，在后续编写中很容易引发极其古怪的错误（“If you call your function eval, hilarity may ensue”）。 定义好过程签名后，主体部分正是针对形参 `expr` 展开的 `pmatch` 匹配。整个求值架构由此确立： ```mermaid flowchart TD accTitle: eval-expr 调度流程 accDescr: 展示 eval-expr 接收表达式并通过 pmatch 派发到对应子句的流程 ExprIn["输入表达式 expr"] --> PMatch{"pmatch expr"} PMatch -->|"数值卫句 (,n (? number?))"| RetN["返回自身: n"] PMatch -->|"(add1,e)"| Recur["递归求值: (add1 (eval-expr e))"] PMatch -->|"更多特殊形式 / 应用"| FutureForms["后续扩展 (Lambda, 变量等)"] ``` --- ### [32:02](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=1922s) 支持自求值数值与引用的重要性 确立了解释器骨架后，Byrd 开始填充能够处理的具体表达式类型。首先是基础数值（例如最开始测试过的数字 `5`）。在 `pmatch` 中，如果仅写匹配模式 `,n`，它会无差别地匹配任何传入的表达式。因此必须引入“守卫”（guard）或谓词（predicate），形如： ```scheme (,n (guard (number? n))) ``` 只有当模式结构匹配且守卫函数（此处为 `number?`）返回真值（即任何非 `#f` 的值）时，该匹配分支才会执行。 现场有观众提问：为什么不直接使用 `cond` 搭配 `(number? expr)` 呢？Byrd 回答：完全可以使用 `cond`，目前的简单场景下 `pmatch` 确实显得大材小用；甚至整套解释器根本不需要宏，仅靠 `car` 和 `cdr` 等列表基本操作就能写出来。然而，等到后续引入带有更复杂结构的 `lambda` 表达式时，`pmatch` 的解构优势就会体现得淋漓尽致。 对于数值的求值结果，Byrd 提问数值应该求值成什么，台下回应：“自身”。于是右侧求值体直接返回 `n`。至此，一个最简的解释器诞生了。Byrd 将代码保存到文件 `interp.scm` 并在 REPL 中加载测试。他邀请观众给出一个测试表达式，有人喊出 `5`。Byrd 幽默地回应：“You will go far, but that's the wrong answer.”（你会大有前途的，但这个回答是错的）。 Byrd 澄清，正确的测试调用必须是 `(eval-expr '5)`，给参数加上引用号。因为如果不加引用，测试表达式在传入 `eval-expr` 之前就会先被宿主 Scheme 环境求值。例如若执行 `(eval-expr (+ 2 3))`，外层 Scheme 会先将其计算为 `5` 再传给解释器，从而给人一种“我们的解释器竟然已经支持加法运算了”的假象： > “Our interpreter works so well that we already can handle addition! Wow, that's really impressive. And if you've written enough interpreters, you've run into this problem before. It's like, whoa, I guess I can turn in my homework early.” Byrd 指出，这是初写解释器时非常经典的错误，因此向解释器喂入代码时必须严谨地加上 `quote`。 --- ### [35:06](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=2106s) 扩展原始操作：递归求值 Add1 确立了数值自求值的逻辑后，Byrd 决定为这门解释语言添加更多能力，首选便是 Scheme 内置的自增操作符 `add1`。 在解释器中，他们新增了一个匹配子句来处理列表结构： ```scheme (`(add1,e) (add1 (eval-expr e))) ``` Byrd 借此展示了使用 `pmatch` 的直观性：模式清楚地要求外层是一个 `add1` 列表，里面包含一个子表达式 `e`。这个子表达式 `e` 可以是任意复杂的结构，不仅可以是一个数字，还可以是另一个会产生数值的子表达式（例如嵌套调用 `(add1 (add1 5))`）。 在右侧的求值实现中，解释器递归调用 `(eval-expr e)` 来解析内部子表达式的值，然后借助宿主 Scheme 提供的底层 `add1` 函数对求出的结果加一并返回。Byrd 总结道，通过借用 Scheme 自身的 `add1` 来实现目标语言中的 `add1`，元循环求值的初步机制已经显现，接下来便是在交互环境中载入并验证其正确性。 ### [36:33](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=2193s) 完善算术操作与条件分支语句 William Byrd 继续在解释器中扩充基础特性。处理一元操作符时，他在模式匹配中加入对 `add1` 和 `sub1` 的支持，并强调测试时必须严格对子表达式进行递归求值，否则很容易出现漏求值的情况。Byrd 调侃道，自己刚才本该使用高大上的“复制粘贴抽象”（copy and paste abstraction），惹得台下一阵笑声。 紧接着是乘法 `*` 的实现。乘法与先前的一元操作不同，它接受两个子表达式 `E1` 和 `E2`。Byrd 提问这里需要进行几次递归调用，观众异口同声回答“两次”。处理方法非常直观：分别递归调用 `eval-expr` 计算出 `E1` 和 `E2` 的值，再用宿主环境的乘法函数将它们相乘。 接下来是条件分支表达式 `if`，其结构包含测试条件（test）、结论分支（consequent）和可选分支（alternative）。对于 `if` 的求值，Byrd 再次幽默地套用“复制粘贴抽象”，并打趣说“Haskell 里大概有个复制粘贴单子（copy and paste Monad）之类的东西吧”。观众询问 `if` 是否具有短路特性，Byrd 澄清：像 `and` 和 `or` 确实会做短路求值，而对于 `if`，必须先求值测试条件；如果测试为真，则只求值第一个子表达式，否则只求值第二个分支，两者绝不会被同时执行。 - `add1` 与 `sub1`：匹配单参数形式，递归求值其子表达式后再进行加减一运算。 - 乘法 `(* E1 E2)`：需要发起两次递归调用分别求值 `E1` 和 `E2`。 - 条件分支 `(if test consequent alternative)`：通过宿主 Scheme 的 `if` 结构调度，仅对匹配条件的那一条分支求值。 --- ### [39:16](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=2356s) 图灵完备的核心：三大核心规则与过程调用 Byrd 话锋一转，指出当前写出的解释器其实“非常无聊”，因为它本质上只是个计算器，尚未触及整个解释器最美丽的核心。他断言，解释器最精华的部分仅由“三行代码”构成。面对他的提问，台下观众猜了 `lambda`、`apply`、`eval`、`define` 和 `quote` 等各种关键字。Byrd 揭晓，这三行正是：`lambda`、过程调用（application）以及变量查找。除此以外的算术和结构都是次要的，仅凭这三者就足以达成图灵完备。他感慨丘奇（Alonzo Church）的 Lambda 演算早在图灵机之前就已经诞生，甚至哥德尔最初都不相信它是图灵完备的。 Byrd 首先实现过程调用。在 Scheme 极简的语法中，函数调用被表示为包含运算符表达式（rator）与运算对象表达式（rand）的列表。在模式匹配库 `pmatch` 中，这行通配模式必须放在最后，以免覆盖其他具体特性的匹配模式。求值过程遵循常规思路：分别对 `rator` 和 `rand` 递归求值。 求得两个值之后，`rator` 的值代表过程，而 `rand` 的值代表实参。应用过程的方法极其直接——直接使用括号将其包裹起来执行调用。Byrd 强调，这行代码极其精炼，“要是眨一下眼，你就会错过它”；有些人患有所谓的“括号盲症”（parentheses blindness），看不出加了括号有何玄机，但这种行为上的本质差异是毋庸置疑的。 > “The beautiful part of the interpreter has to do with three lines and only three lines.” —— William Byrd ```mermaid flowchart TD accTitle: 三大核心规则求值流 accDescr: 展示表达式如何通过三大核心规则进行求值、环境查找与过程调用。 subgraph EvalRouter["eval-expr 表达式分发"] E["输入表达式"] --> CaseVar{"是否为符号（变量）?"} CaseVar --"是"--> VarLookup["【规则一】变量查找：(env x)"] CaseVar --"否"--> CaseLambda{"是否为 Lambda?"} CaseLambda --"是"--> LamCreate["【规则二】Lambda：构造闭包过程并等待调用"] CaseLambda --"否"--> AppCall["【规则三】过程调用：((eval-expr rator) (eval-expr rand))"] end ``` --- ### [42:00](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=2520s) 引入环境传递：变量表示与符号查找 在分析 `lambda` 表达式时，形参 `x` 以标识符形式出现。如果 `x` 随后出现在函数体或引用的表达式中，它就成了一个变量引用。变量 `x` 当前的值是多少？Byrd 直言：“现在还不知道，只有在运行时真正发生过程调用时才会揭晓。”如果传入实参 5，那么在函数体内 `x` 的值就是 5。 为了能够在函数体执行时查找与变量绑定的具体值，解释器必须引入一个查找机制，即经典的“环境”（environment）。Byrd 宣布他们将编写一个“环境传递解释器”（environment-passing interpreter）。一旦在参数列表中加入 `env`，整个解释器的架构就发生了质的飞跃，前面提到的三行核心代码全部都与环境紧密纠缠在一起。 第三条核心规则正是变量查找（variable lookup）。在 Scheme 中，变量可以直接用符号（symbol）来表示。为了匹配独立的变量，Byrd 在模式匹配中增加了一个 `symbol?` 的保护谓词（guard）。至于环境的具体内部实现，Byrd 采取了一种极致精简且斯巴达式的设计：将环境直接表示为一个接受单一变量作为参数的过程。既然环境本身就是一个过程，那么查找变量 `x` 的方式就变成了直接调用该环境过程 `(env x)`。 - 过程调用的形式：`(rator rand)` 分别对两者递归求值，然后执行 `((eval-expr rator env) (eval-expr rand env))`。 - 变量的本质：编译/解析期只是标识符，其实际值被延迟绑定到运行时的调用时刻。 - 环境机制：在参数中传递 `env`，用高阶过程表示环境映射，通过直接执行 `(env var)` 完成寻值。 --- ### [46:25](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=2785s) 闭包的本质：Lambda 与环境扩展 最后是 `lambda` 规则的处理。在 Scheme 中，`lambda` 表达式求值后会生成一个过程（procedure）。Byrd 将过程解释为一种“延迟计算”（delayed computation）：在定义函数的当下，由于尚未获取到实参，解释器缺乏足够的信息来执行函数体；唯有等到该过程被真正调用、实参绑定到形参之上、并形成具备正确作用域的环境后，才能求值函数体。 如何表示这样一个过程？台下观众打趣喊道“Lambda”，Byrd 笑着引用电影台词回应：“没错，这招‘60% 的时候，每一次都管用’（60% of the time, it works every time）。”解释器生成的正是一个 Scheme 的底层 `lambda` 过程：`(lambda (arg)...)`。 Byrd 郑重提醒大家厘清概念：这里的 `arg` 并不对应形参名 `x`，而是对应运算对象 `rand` 求值后得到的具体数值。过程调用行与 `lambda` 行在逻辑上紧密相扣——调用时传入实参值，形参 `arg` 便绑定该值。最后，过程被调用时，需要在一个“扩展了的环境”（extended environment）中递归求值函数体 `body`。Byrd 随即着手对之前写好的各行代码进行“重构”（retro-fit），将环境参数 `env` 贯穿传递下去，并引出了下一个关键动作：如何用最简洁的 `lambda` 来构造扩展环境。 > “Lambda expression evaluates to what in Scheme? A procedure... which you can think of as a delayed computation where we don't have enough information to do the computation in the body yet, but we're going to wait until the procedure gets called.” —— William Byrd ### [49:10](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=2950s) 用 Lambda 构建高阶环境与闭包 William Byrd 带领现场观众完成了求值器（`eval-expr`）中最核心、最具魔力的闭包与环境扩展部分。当面对“如何扩展环境”这一问题时，观众席给出了“用 `lambda`”的答案，Byrd 笑着称赞道：“没错，确实是用 `lambda`。虽然它是个‘只会一招的小矮马’（one trick pony），但这招实在太厉害了。”他随即写下 `(lambda (y)...)`，并兴奋地表示：“这就是‘极客战栗’（nerd chills）开始的时刻。” ```mermaid flowchart TD accTitle: 高阶环境查找逻辑 accDescr: 展示传入变量 y 后与绑定变量 x 进行比较并决定返回 arg 还是向父环境递归查找的流程 subgraph Lookup["环境闭包 (lambda (y)...)"] Check{"y 等于 x 吗？<br/>(eq? y x)"} Hit["返回当前参数值<br/>arg"] Miss["在父环境中递归查找<br/>(env y)"] end Check -->|"是 (命中)"| Hit Check -->|"否 (未命中)"| Miss ``` 这个所谓扩展后的“环境”，本质上就是一个接受单一参数 `y` 的 Scheme 过程。在它的内部，求值逻辑通过条件判断完成： - 调用 `(eq? y x)` 比较查找的变量 `y` 与刚刚绑定的形参 `x`。 - 如果二者相等，则直接返回实参求值后的值 `arg`。 - 如果二者不相等，则执行 `(env y)`，把查找任务委托给上一层旧环境。 Byrd 强调，这个最内层的 `lambda` 构成了扩展环境，而外层的 `lambda` 则构成了所定义的程序函数（Procedure）。这种在解释器内部同时将环境与过程均表示为函数的设计，被称为环境与过程的高阶表示（Higher-order representation）。在这种表示下，函数应用分支（Application）无需显式操作数据结构；但 Byrd 指出，如果未来改用列表（List）等纯数据结构来表示环境和过程，原本写在 `lambda` 分支里的闭包构建工作，就会挪到应用分支（Application）中去完成。 --- ### [51:36](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=3096s) 修复初始环境与阶乘测试成功 在写完核心逻辑后，Byrd 准备测试这个解释器。当尝试调用 `(eval-expr '(+ 1 6))` 时，系统立刻报错，观众席敏锐地提醒他忘记传入初始环境。Byrd 称赞道：“非常聪明，你说得对！”那么最底层的空环境（Empty Environment）长什么样？答案依然是 `lambda`： ```scheme (lambda (y) (error 'lookup "unbound")) ``` 只要试图在空环境中查找任何未绑定的变量 `y`，系统就会抛出 `unbound` 错误。修复之后，基础算术运算返回了正确的 `7`，查找未绑定变量 `x` 成功报错，恒等函数 `((lambda (x) x) 5)` 也正确求得 `5`。为了进行终极测试，Byrd 又补上了一个 `zero?` 条件分支。 接下来是检验解释器完整性的终极考验：使用 Dan Friedman 所谓的“穷人版 Y 组合子”（Poor Man's Y Combinator）来运行递归阶乘（Factorial）。Byrd 解释说，当前的微型语言里既没有 `define`，也没有用于相互递归的 `letrec`，但因为有强大的 `lambda`，便能通过纯粹的函数构造达到不动点（Fixed point）并实现递归。当他在黑板上的解释器中把这串复杂的阶乘表达式送入求值并成功打印出计算结果时，全场响起掌声与欢呼，Byrd 赞叹道：“Awesome, well done!” --- ### [55:08](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=3308s) 剔除“废码”：写在 4×6 索引卡片上的宇宙钥匙 验证成功后，Byrd 笔锋一转，开始对刚刚写出的几十行代码进行大刀阔斧的“净化”。他半开玩笑地宣称：“除了最后三行，前面加的所有分支全都是‘毒瘤’（abomination）！”他一口气把数字常量、`zero?`、加减法、`if` 表达式全部删掉，只保留了最纯粹的三个分支：变量查找（Variable lookup）、抽象（Lambda abstraction）和应用（Application）。 ```mermaid flowchart LR accTitle: 极简求值器的三大核心支柱 accDescr: 展示仅剩的三行核心解释器架构：变量引用、函数构造与函数调用 subgraph CoreInterpreter["3×5 索引卡片求值器"] Var["1. 变量查找<br/>(lookup x in env)"] Abs["2. Lambda 抽象<br/>(构造高阶过程闭包)"] App["3. 函数应用<br/>(求值算子与操作数并调用)"] end Var ~~~ Abs ~~~ App ``` Byrd 指出，这仅有三行核心逻辑的代码就是著名的“写在 3×5（或 4×6）索引卡片上的解释器”。他赞叹道： > “That is the magic. Okay, this is the key to the universe. You have everything here.”（这就是魔法所在。这就是解开宇宙的钥匙，你所需要的一切都在这里了。） - **极简主义与图灵完备**：无需内置数字，数字可以通过丘奇编码（Church encoding）实现；无需内置 `if`，条件分支同样可以用函数编码。所有这些为了实用性与效率添加的语法糖都可以剔除，仅凭这三行代码就达到了完整的图灵完备性（Turing-complete），甚至其背后的 Lambda 演算模型在历史上比图灵机出现得更早。 - **环境传递求值器**：该程序本质是一个按值调用（Call-by-value）、基于环境传递的 Lambda 演算解释器。 - **可扩展性演进路径**： - **状态与可变性（Mutation）**：在此解释器中引入 Store（存储），即可支持类似 Scheme 中 `set!` 的赋值操作。 - **延续与控制流（Continuations）**：对该解释器实施 CPS 变换（Continuation-Passing Style），把程序未来的计算表示为一个延续过程；若进行双重 CPS 变换（CPS twice），就能得到限定延续（Delimited continuations），进而模拟任何现代控制流结构。 - **作用域规则转变**：只需修改变量在环境中的查找方式，便能轻松在词法作用域（Lexical scope）与动态作用域（Dynamic scope）之间切换。 Byrd 动情地回顾了导师 Dan Friedman 对所有学生的教诲：拿一叠 4×6 的空白索引卡片，花上 45 分钟一遍又一遍地手写这几行解释器代码，“直到你的眼睛开始流血，将它深深烙印在你的大脑和心灵之中，你就永远不会忘记它”。只要彻底参透并亲手推动它运转，就能领略计算理论中所有可计算函数的终极奥秘。 --- ### [59:38](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=3578s) 重读麦卡锡：等号的双向性与关系式视角的开启 在演示完高阶解释器后，Byrd 将话题转向这套思想在全新语境下的深刻演化。他展示了约翰·麦卡锡（John McCarthy）的经典论文《A Micro-Manual for LISP - Not the Whole Truth》（LISP 微型手册——并非全貌）。在该论文中，麦卡锡以极其简练的数学规则定义了 `cons` 以及名为 `value` 的 Lisp 求值器。 Byrd 引导观众敏锐地观察麦卡锡论文中的公式表达：麦卡锡写下了 `value(e, r) = v`，即表达式 `e` 在环境 `r` 下“等于”值 `v`。关于这个不起眼的等号，Byrd 发出了深刻的反思： > “The notion of equality is actually one of the most subtle notions in all of mathematics and logic and computer science. Anyone who thinks they understand equality as just kind of some throwaway idea hasn’t thought about it hard enough.”（等同性的概念实际上是整个数学、逻辑学和计算机科学中最微妙的概念之一。任何认为自己理解了等同性、并把它当作随手可抛的简单概念的人，都还没有对其进行足够深入的思考。） Byrd 指出，传统编程语言、解释器和编译器的思维定势，总是把那个等号视为“从左到右”单向流动的单行道：给定一段表达式，写一个求值函数或编译器把它单向运行出最终的值。然而，从数学和逻辑关系的角度来看，等号两边本应具备对等的对称性。如果打破从左向右的单向求值枷锁，把求值器视作一个真正的多向关系（Relation），计算将展现出完全不同的广阔天地。 ### [01:01:02](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=3662s) 把等号当真：关系型编程与 miniKanren 解释器 William Byrd 将视线从常规的求值函数拉回到一个根本性的数学问题：在普通代数中，等号是双向的约束，而在传统编程中，求值往往只是一个单向箭头。高中代数教大家解方程时，核心是通过 $x$、$y$、$z$ 等未知变量推导让等式两边成立的数值。Byrd 提出了一个大胆的前提：“如果我们认真对待等号会怎样？如果我们认真地说，好吧，这就像代数，对吧？”（“what if we seriously said all right well this is like an algebra right”）。为此，他和 Daniel P. Friedman、犹他大学的 Michael Ballantyne 以及 Greg Rosenblatt 等学者耗费了整整 12 年时间，在逻辑/关系型编程语言 miniKanren 中构建了一门解释器。 ```mermaid flowchart LR accTitle: 传统解释器与关系型解释器的对比 accDescr: 对比传统求值单向流动与关系型求值双向约束的运行机制 subgraph Traditional["传统解释器（单向计算）"] E1["表达式 Expr"] -->|"求值 eval"| V1["值 Val"] end subgraph Relational["关系型解释器 miniKanren（双向约束）"] E2["表达式 Expr 或未知量?"] <-->|"eval-expo 逻辑关系"| V2["值 Val 或未知量?"] end ``` Byrd 指出，这个在 miniKanren 中用 `eval-expo` 实现的解释器虽然不能像极简 Lisp 一样缩印在 3×5 英寸的卡片上，但也只有 43 行代码左右，且结构与数理逻辑中的操作语义（Operational Semantics）完全平行。在现场加载代码并启动 miniKanren 查询系统时，Byrd 调侃道：“在必须加载文件之前，一切都很好，对吧？这种破事可没有数学支撑，大概得用 Monad 之类的垃圾玩意儿来解决。”（“it's all fine and good until you have to do things like load a file right there's no math for that probably a monad or something junk for that”）。进入系统后，解释器隐去了初始空环境，表达式和计算结果作为关系的两个端口并列存在。在最基础的正向查询中，向表达式端口传入数字 `5`，系统便如实推导未知量 $X$ 为 `5`；传入恒等函数 `((lambda (x) x) 5)`，系统同样正确解出其闭包求值结果为 `5`。 - 该关系型解释器基于逻辑编程语言 miniKanren 编写，核心关系命名为 `eval-expo`。 - 解释器的形式化逻辑与教科书式的操作语义规则几乎逐行对应，总长度仅约 43 行。 - 在 miniKanren 查询中，传统函数的“输入参数”与“返回值”被降维为平等的逻辑项，均可放入逻辑未知量。 --- ### [01:06:26](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=3986s) 逆向程序生成：“我想要奶昔”与 99 种说“我爱你”的方式 一旦求值过程变成了代数方程，系统就具备了逆向求解程序代码的能力。Byrd 演示了这一机制：固定输出端口的值为列表 `(I want milkshake)`（我想要奶昔），而将代码表达式端口设为未知变量进行求解。系统首先给出的解是直接引用字面量 `'(I want milkshake)`；随后要求给出更多解时，系统推导出了一个由无参匿名函数包裹并立即调用的复杂程序 `((lambda () '(I want milkshake)))`；紧接着，系统生成了通过 `car` 获取嵌套列表头元素的程序 `(car '((I want milkshake)))`。 Byrd 结合犹他大学同事 Matt Might 的博客故事作了生动的引申：Matt Might 曾在情人节写过一篇题为《在 Racket 中说“我爱你”的 99 种方法》（*99 ways to say I love you in Racket*）的博文。Byrd 现场使用 `run 99` 指令，让解释器当场自动合成了 99 个求值结果均为 `(I love you)` 的 Scheme 表达式。这些自动生成的代码包含各种嵌套调用、高阶函数和列表操作构造，每一段程序都能在标准 Scheme 环境中合法且准确地跑出这句表白。 --- ### [01:09:02](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=4142s) 解出 Quine 与逆向列表追加（Append） 在成功生成常规程序的基础上，Byrd 将问题引向了计算机科学领域的经典难题——Quine（自产生程序，即输出结果与自身代码完全一致的程序）。他提到 John McCarthy 在 1960 年的奠基论文中曾留下一道难题：“一个高难度的数学练习：寻找一个列表（即程序表达式）e，使得 e 的值等于 e”（“a difficult mathematical type exercise find a list e that means a program expression e such that the value of e is equal to e what is that called a quine”）。在 miniKanren 中，解决这个问题仅仅需要书写一行代数等式：要求求值关系的表达式与目标结果绑定到同一个逻辑变量 `e` 上。系统率先给出了数值自求值（`5` 求值为 `5`）和布尔自求值（`#t`、`#f`），随后经过简短推导，自动搜寻出一段符合严格 Quine 定义的高阶闭包构造代码。 ```mermaid flowchart TD accTitle: 利用关系型解释器逆向推导代码与输入 accDescr: 展示关系型解释器在 Quine 生成和 append 逆向参数推导中的应用场景 subgraph QuineGen["Quine 生成"] Q["求解: eval(e) = e"] --> S1["简单平凡解: 5, #t, #f"] Q --> S2["高阶非平凡解: 自产生闭包表达式"] end subgraph RelAppend["列表追加 append 逆向求解"] Def["解释执行递归 append 定义"] --> InputSolve["设定结果: '(a b c d e)"] InputSolve -->|"已知右侧参数 '(d e)"| SingleVar["解出未知参数 X = '(a b c)"] InputSolve -->|"双未知数求解"| MultiVar["解出 X 与 Y 的所有拆分可能"] end ``` 随后，Byrd 展示了 Michael Ballantyne 提出的方向：在解释器内部运行更复杂的实用程序。Byrd 用 `letrec` 编写了一个标准的递归列表拼接函数 `append`，其逻辑是检查列表 `L` 是否为空，空则返回 `S`，否则递归取头并 `cons` 到剩余部分的拼接结果上。当正向运行拼接 `'(a b c)` 与 `'(d e)` 得到 `'(a b c d e)` 验证无误后，Byrd 颠倒了计算的方向：将结果固定为 `'(a b c d e)`，并将第一个输入参数替换为未知变量，询问“什么列表和 `'(d e)` 拼接能得到 `'(a b c d e)`？”系统立即秒推解出 `'(a b c)`。这种双向推演不仅限于单参数，即使将输入参数同时设为两个未知数 $X$ 和 $Y$，关系系统也能自动枚举出将结果拆解为两个子列表的所有有效组合方案。 ### [01:12:47](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=4367s) 关系式解释器的双向性与等号的真义 William Byrd 现场展示了关系式解释器强大的双向求解能力。他提出一个查询：寻找哪两个列表拼接起来能够得到 `(A B C D E)`。解释器给出的第一个解是空列表 `()` 与 `(A B C D E)`；随后他将查询方式换成 `run*`，解释器一口气找出了所有可能的分割配对组合。Byrd 指出，熟悉 Prolog 或 miniKanren 等逻辑编程语言的人对这种查询并不陌生，但这里的关键在于：“请注意，我们并没有去写一个专门的逻辑程序，我们只是把一个普通的 Scheme 程序放进了我们的解释器里。” ```mermaid flowchart LR accTitle: Bidirectional Execution of Append accDescr: Diagram showing how a relational interpreter solves for append inputs and outputs symmetrically. subgraph Inputs["自由逻辑变量"] L1["变量?x"] L2["变量?y"] end subgraph Engine["关系式解释器 (miniKanren)"] App["(append?x?y) = '(A B C D E)"] end subgraph Results["反向求解全解集"] R1["'() 与 '(A B C D E)"] R2["'(A) 与 '(B C D E)"] R3["... 其余所有分割组合"] end Inputs --> Engine Engine --> Results ``` 通过这一操作，计算范式发生了本质转变。Byrd 强调：“我们正在严肃地对待等号——我们主张‘相等’真的就意味着‘相等’，而且等号本身并不具备方向性，我们理应能够求解任意一侧的未知项。”不仅可以反向推算输入，如果向系统提供完整的输入与输出（比如输入 `(A B C)` 与 `(D E)`，声明输出为 `(A B C D E)`），miniKanren 会返回一串代表一致性满足的逻辑变量符号，证明命题成立。 - 传统的函数调用具有严格的输入到输出的单向性，而关系式解释器消除了这一限制。 - `run*` 能够穷尽搜索空间，返回匹配该等式的所有解组合。 - 逻辑编程的核心优势在于不需要编写专用解算器，而是借助语义约束自动双向推演。 --- ### [01:13:56](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=4436s) 迈入程序合成：从推导变量到“狡黠的精灵” 既然逻辑变量可以放置在输入和输出位置，Byrd 顺势向听众发问：代码里还有哪些地方可以塞入逻辑变量？答案是：任何地方。Byrd 现场做了一个实验，把代码中原本写着符号 `s` 的位置替换为一个代表未知表达式的逻辑变量，随后调用 `run 1`。解释器准确无误地把被抹掉的 `s` 推断了出来。这一刻标志着演示正式跨入“程序合成”（Program Synthesis）的领域。开发者只需指定预期的输入与对应的输出，利用关系式解释器的语义作为逻辑规则，系统便会通过搜索和约束求解，自动推断出缺失的代码碎片。 然而，当 Byrd 尝试把原本的函数名 `append` 挖空替换为逻辑变量时，意想不到且引人发笑的事情发生了。解释器给出的第一个解并不是大家预期的 `append`，而是一个直接忽略入参、永远硬编码返回 `(A B C D E)` 的匿名过程。面对台下的哄堂大笑，Byrd 调侃道：“miniKanren 就好像在说：‘有种你证明我是错的啊！’”为了制服这个像“阿拉丁神灯里的狡黠精灵”一样钻空子的解释器，Byrd 增加了测试样例——不仅要求它处理 `(A B C)` 和 `(D E)`，还要求处理两个空列表并返回空列表。有了多组样例的约束，解释器被迫收敛，终于正确合成了 `append`。当进一步要求生成第二个解时，系统立刻又给出了一个零参数的可变参数函数包装调用，再次展现了逻辑系统寻找捷径的滑稽“智慧”。 “我们有能力以‘期望的输入及其对应的期望输出’这种形式来指定信息，并借助我们编写为关系及逻辑编程系统的解释器语义来进行推断——本质上就是进行搜索和约束求解，从而推断出缺失的值。”——William Byrd --- ### [01:17:21](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=4641s) Barliman 工具与基于示例的交互式合成 原生 miniKanren 在无优化状态下进行程序合成极其缓慢，因为随着代码变大，搜索空间呈指数级膨胀。为此，Byrd 介绍了由他与 Greg Rosenblatt、Michael Ballantyne 等人联合开发的工具——Barliman。Barliman 的底层包含大量剪枝优化，运行速度比朴素版本快了约 1000 万倍；前端则是 Byrd 自学 Swift 编写的极简图形界面。在该界面左上方，函数的结构被大量挖空（例如定义为 `define` 一个未知函数名 `,A`，接受未知参数列表 `,B`，函数体也是未知的逻辑变量 `,C`）。 ```mermaid flowchart TD accTitle: Barliman Synthesis Workflow accDescr: Flowchart illustrating how Barliman synthesizes programs from incremental test examples. subgraph UI["Barliman 界面"] Code["挖空模板: (define,A (lambda,B,C))"] Tests["测试示例集合 (I/O Examples)"] end subgraph Solver["优化搜索核心 (1000 万倍加速)"] Search["剪枝约束求解器"] Gensym["Gensym 机制 (杜绝字面常量作弊)"] end subgraph Output["合成演进"] Draft1["阶段1: 常量硬编码返回"] Draft2["阶段2: 条件分支与单层解构"] Final["阶段3: 递归调用生成完整 append"] end Code & Tests --> Search Search --> Gensym Gensym --> Draft1 --> Draft2 --> Final ``` 在演示中，Byrd 逐步向 Barliman 提供示例： 1. **第一个测试**：输入两个空列表 `()` 与 `()`，期望得到 `()`。Barliman 几毫秒内给出的解是：一个返回 `()` 的全通函数。 2. **第二个测试**：追加 `'(a)` 和 `'(b)` 输出 `'(a b)`。Barliman 迅速生成一个 `if` 判断：如果第二个参数为空则返回空，否则返回字面常量 `'(a b)`。 3. **引入 Gensym**：为了杜绝这种硬编码字面常量的“作弊行为”，Byrd 引入了生成符号（gensym）。系统必须保证测试中的特定符号绝对不会出现在生成的源码中，从而迫使合成器必须通过结构性操作来转移数据。 4. **第三个测试**：增加一个长度为 2 的列表样例。Barliman 停顿思考了片刻，屏幕上终于跳出了递归调用，完整合成了标准的 `append` 算法核心逻辑。 现场 Byrd 还打趣地跟听众互动，当自己不小心敲错测试输入时，台下观众立即指出错误，Byrd 笑着回应：“有没有人想来 Barliman 团队当 QA 测试员？” --- ### [01:21:55](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=4915s) 极限测试驱动开发与后台自动定理证明 Byrd 进一步展示了 Barliman 超越普通代码合成器的潜能：将其作为一种极致的“测试驱动开发”（TDD）实时辅助编辑器。假设面临一个合成器由于搜索空间过大而无法一步到位的复杂任务，开发者可以先写测试，然后由人类亲自编写代码骨架，并留下若干挖空的占位符表达式。在输入过程中，Barliman 的后台线程会持续运转，不断验证用户当前键入的代码与既有测试样例之间是否存在逻辑矛盾。 为了验证这一点，Byrd 在编写 `append` 的条件分支时，故意在判断列表为空后尝试返回错误的变量 `l`。Barliman 瞬间将该测试标红并报错拒绝——“电脑说不行”（Computer says no）。Byrd 解释说，这是因为后台的 miniKanren 本质上是一个定理证明器（Theorem Prover），它能够严格在数学层面证明：用户当前写下的不完全代码片段，与某个给定的测试用例在逻辑语义上是绝对不相容的。 “你可以只把它当成一个编辑器来用，它会在后台持续耗尽你的所有 CPU 核心、温暖你的公寓，并不顾一切地试图证明——请注意这真的是一种‘证明’，因为 miniKanren 本身就是一个定理证明器——你所编写的部分指定的代码，实际上与你的某一个测试是不相容的。”——William Byrd - 实时不一致性检测能精确定位冲突，但不代表一定是代码写错了，也可能是测试本身有 Bug，甚至是底层解释器的语义定义存在漏洞。 - 无论出错的原因属于哪一种，系统都可以百分之百断定代码与规范之间存在无法调和的矛盾。 - 这种融合了定理证明与不完全程序规约的技术，已经开始走向实际应用，并在更广阔的程序合成前沿领域展现出巨大价值。 ### [01:24:20](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=5060s) 关系语义、程序合成与最美程序的秘密 William Byrd 谈到程序合成（Program Synthesis）领域目前正在经历一场复兴，但他认为他们团队的独特之处在于实现合成的方法：回归讲座一开始展示的那段优美的解释器代码，重新审视其最初的数学描述，并“把等号真正当回事”。这种做法将传统用于形式化规范的关系语义（Relational Semantics）直接转变为可执行代码。团队设计了 miniKanren 语言来优雅地编码这些关系，并辅以大量的搜索优化。一旦将解释器写成关系，就能玩起强大的“填空游戏”（完形填空式程序合成）。 ```mermaid flowchart TD accTitle: 基于 miniKanren 的关系式解释器架构 accDescr: 展示了如何将数学定义的关系语义编码为 miniKanren 解释器，进而通过约束求解实现双向执行、程序填空合成以及定理证明。 subgraph RelationalCore["理论与实现"] A["数学形式规范<br/>(关系语义中的等号)"] --> B["miniKanren 关系编码<br/>(消除输入输出方向)"] B --> C["高度优化的<br/>关系式解释器"] end subgraph Capabilities["衍生能力与应用"] C --> D["正向求值 / 逆向生成<br/>(如生成 Quine)"] C --> E["填空式程序合成<br/>(根据测试样例补全代码)"] C --> F["验证器逆转<br/>(Proof Checker 变为 Theorem Prover)"] end ``` Byrd 指出，这种关系化思路具有极高的通用性，例如将一个证明检查器（Proof Checker）写成关系，就能直接把它变成自动定理证明器（Theorem Prover）。他推荐感兴趣的观众观看他和 Greg Rosenblatt 在上一届 Clojure/conj 上所作的演讲，其中展示了更多范例。随后他向社区发出邀请，推荐访问 minikanren.org，并欢迎大家参加他在周末举办的线上 Hangouts（分为入门与进阶系列），甚至表示如果有人想参与研究、改进工具的 UI 或者单纯聊聊，“给我发封邮件，打个招呼，我们一起去喝杯奶昔”。 在总结演讲主题时，Byrd 再次赞叹用 Lisp 编写的高阶解释器是何等精妙：它不仅极其紧凑，融合了计算机科学的核心思想，而且无论从无限解释器之塔、元循环、程序变换还是关系语义的角度去审视它，每一次换个视角，它都能揭示出全新的奥秘。William Byrd 总结道：“从某种意义上说，我们对解释器了如指掌，但在另一种切实的意义上，我绝不会猜到只要把那个程序用逻辑编程语言编码，你就能做到这种事情，但事实证明你确实能做到。”他呼吁大家花时间深入研读并理解这一经典作品，寻找属于自己的观察视角。 - 推荐参考资料：William Byrd 与 Greg Rosenblatt 在 Clojure/conj 上的演讲，深入展示了关系编程与合成的应用。 - 社区入口：访问 minikanren.org 获取研究资料；Byrd 在周六和周日定期主持入门与高阶 Google Hangouts。 - 核心哲学：同一个微小（few-line）的核心程序，换用关系逻辑来执行，就能从普通的“解释器”蜕变为“程序合成器”。 --- ### [01:27:36](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=5256s) 问答环节：高阶元约束与启发式加速 在全场掌声之后，进入了简短的现场提问环节。第一位观众提问：既然测试用例被当作程序的约束条件来猜测未知代码，那么能否施加“元约束”（Meta-constraints）？例如规定“必须是常数时间算法”或“内存占用为 $O(1)$”？ Byrd 回答称这是一个极好的问题。在程序合成中，核心难点在于如何明确形式化你对程序行为的预期。目前他们除了使用输入输出测试，还可以使用类型推导（以相同风格编写关系式类型推断器）或逻辑中的高层性质来约束搜索。关于运行时间或内存复杂度的元约束，Byrd 坦言：“我们目前还没达到可以讨论预期运行时间那种程度，尽管那确实是我非常希望能做到的事情。”不过，程序合成学界已有其他研究团队在专注解决带有预期渐进复杂度的合成问题。 紧接着，Byrd 分享了他们刚刚开展的一项突破性实验： - 就在演讲前一天，Byrd 编写了一个新版本的技术，让系统学习 Scheme 代码中的常见惯用模式（Idiomatic patterns）。 - 这种学习非常简单，仅通过分析表达式的父节点模式，例如：在 `define` 内部通常会出现 `lambda`；在 `lambda` 内部通常会出现 `if` 或 `cond`。 - 将人类的编程风格先验知识融入关系式解释器中进行特化，而不仅仅依赖纯语义规则。 - 初步实验显示，仅仅引入这种极简的代码结构模式先验，“看起来就将合成速度提升了许多个数量级”（speeds up synthesis many orders of magnitude）。团队目前正在探索如何将该技术与现有的各项搜索优化相结合。 --- ### [01:29:52](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=5392s) 问答环节：环境作用域与搜索空间的确定 第二位观众针对之前的代码补全演示提出了疑问：“在给出 `append` 答案的例子中，系统是如何看待搜索空间的？它怎么知道要找到 `append`，`append` 是如何进入搜索空间的？”观众注意到系统并非凭空猜出递归，最开始甚至猜过直接返回参数列表的简单函数。 William Byrd 解释了其中的机制： - 搜索并非漫无目的地在所有可能的符号中乱撞，而是完全由解释器内置的环境（Environment）与作用域机制决定的。 - 在关系式解释器内部，团队完整实现了变量查找机制（Variable Lookup）以及 `letrec` 的绑定语义。 - 在对 `append` 进行合成时，未知的空缺代码处于 `letrec` 定义的作用域内部。根据 `letrec` 的语义，被定义的函数名 `append` 在其函数体执行时已经绑定在当前环境中。 - 当解释器在填空过程中尝试为未知表达式寻找合理的变量时，它的规则之一就是：“解释器会去查找当前环境中已绑定的所有变量，逐一尝试，看看是否有助于导出符合测试的解。”因此递归调用天然地包含在候选分支中。 简短的答疑结束后，现场再次致谢并结束了本场分享。 ## Notable quotes > [59:38](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=3578s) The notion of equality is actually one of the most subtle notions in all of mathematics and logic and computer science. Anyone who thinks they understand equality as just kind of some throwaway idea hasn’t thought about it hard enough. — William Byrd > [02:33](https://www.youtube.com/watch?v=OyfBQmvr2Hc&t=153s) And that's the most dangerous way of thinking is to think you understand something right and that there are no kind of new tricks in this. — William E. Byrd ## Mentioned William E. Byrd, Daniel P. Friedman, John McCarthy, Alan Kay, Alonzo Church, Paul Erdős, Ken Shirriff, Michael Nielsen, Kenichi Asai, Nada Amin, David Wise, Henry Baker, Andrew Plotkin, Matt Might, Michael Ballantyne, Greg Rosenblatt, Chez Scheme, Scheme, Lisp, Java, JavaScript, Haskell, Prolog, Racket, Swift, miniKanren, Barliman, The Little LISPer, The Little Schemer, The Seasoned Schemer, The Reasoned Schemer, Essentials of Programming Languages, LISP 1.5 Programmer's Manual, A Micro-Manual for LISP - Not the Whole Truth, Two Sigma, Chartbeat, University of Utah, Indiana University ## Video description Meetup: http://bit.ly/2okyAH3 Audio: http://bit.ly/2qkAczZ Sponsored and hosted by Two Sigma (@twosigma) and Chartbeat (@Chartbeat) Description ------------------ William E. Byrd "explores what he considers to be the most beautiful program ever written---a Lisp interpreter written in Lisp---and a few of the many amazing ideas related to this metacircular interpreter." References - The Little Schemer by Daniel P. Friedman and Matthias Felleisen - Essentials of Programming Languages by Daniel P. Friedman and Mitchell Wand - John McCarthy's Recursive functions of symbolic expressions and their computation by machine, Part I - LISP 1.5 Programmer's Manual by John McCarthy, Paul W. Abrahams, Daniel J. Edwards, Timothy P. Hart and Michael I. Levin (see especially page 13!) - John McCarthy's A micro-manual for LISP - not the whole truth - "Maxwell's equations of software" examined by Ken Shirriff - Lisp as the Maxwell’s equations of software by Michael Nielsen - miniKanren, live and untagged: quine generation via relational interpreters (programming pearl) by William E. Byrd, Eric Holk, and Daniel P. Friedman - The Reflective Language Black by Asai, Kenichi - Programming Should Eat Itself by Nada Amin, Strange Loop, 2014 Bio ----- William E. Byrd (@webyrd) is a Research Assistant Professor in the School of Computing at the University of Utah. He is co-author of 'The Reasoned Schemer', and is co-designer of the miniKanren relational programming language. He loves StarCraft (BW & SC2). Ask him about the scanning tunneling microscope (STM) he is building. [Source](https://www.youtube.com/watch?v=OyfBQmvr2Hc)

[59:38] William Byrd: The notion of equality is actually one of the most subtle notions in all of mathematics and logic and computer science. Anyone who thinks they understand equality as just kind of some throwaway idea hasn’t thought about it hard enough. [2:33] William E. Byrd: And that's the most dangerous way of thinking is to think you understand something right and that there are no kind of new tricks in this.

[8:30] William Byrd: Just like CPS is the gateway drug of program transformations lisp in lisp is the gateway drug of the whole world of programming languages I think. [59:38] William Byrd: anyone who thinks they understand equality as just kind of some throwaway idea hasn't thought about it hard enough

[0:00] [Music] [0:17] so I'm will and you know I was a a [0:21] middle school teacher and I ran a summer [0:24] camp and I did all these things and then [0:26] at some point I got a degree in computer [0:29] science and I worked was a Java [0:30] developer and all this stuff right and [0:32] then I got fed up with the JavaScript [0:35] and the Java and all that and I went to [0:37] graduate school at Indiana University to [0:39] work with Dan fredman uh who you may [0:42] have heard of he's someone who you wrote [0:44] a book called The Little lisper and a [0:48] revised version called the little [0:49] schemer and the season schemer I wrote a [0:52] book with him called the reason [0:54] schemer [0:55] and um I took Dan's class the first you [1:01] know semester I was there and and uh you [1:04] know a couple weeks in to the class Dan [1:07] showed me a program that changed my life [1:10] you know and basically I've spent the [1:12] last 12 13 years trying to understand [1:16] like these five lines of code right and [1:20] I will spend the rest of my life trying [1:22] to understand the implications of these [1:25] five lines of code and this is what I [1:28] like okay so some people like writing a [1:30] 100,000 line compiler or an operating [1:33] system kernel with two million lines of [1:34] code or whatever and and that's great [1:37] what I like is sort of going the [1:40] opposite way I like the 3x5 card or the [1:43] 4x6 card and if you're not an American I [1:46] don't know what that is uh it's A4 or [1:49] something I don't know uh so it's like a [1:52] you know 3x5 card maybe a 4x6 card if [1:56] you can't fit down the idea on a 4x6 [2:00] card then think harder that's sort of [2:03] Dan's philosophy right and ideally you [2:06] get it down to the 3x5 card and then you [2:08] write a little book on it and so that's [2:11] that's kind of his his way of thinking [2:13] uh and I I share a lot of that [2:16] sensibility so what I would like to talk [2:19] a little bit about today is this program [2:21] that I saw and it just it just floored [2:24] me and to this day I get nerd chills [2:27] every time I think about it right [2:29] they're really get nerd chills and um I [2:33] think you know I was nervous about I am [2:36] nervous about giving giving this talk [2:38] because one of the dangers I think is [2:40] that when you've been programming for a [2:43] while and I know a lot of people in this [2:44] audience like no list or they've worked [2:46] through sicp or they've written lots of [2:49] interpreters and all these sorts of [2:50] things they know something about Lambda [2:52] calculus after a while you can feel like [2:55] you understand something and that's the [2:58] most dangerous [3:00] way of thinking is to think you [3:02] understand something right and that [3:03] there are no you know kind of kind of [3:05] new tricks in this and um basically [3:09] every time I learn something new about [3:12] computer science or you know every [3:14] couple years or something like that I [3:15] like to go back and try to think about [3:18] those things which I learned a long time [3:20] ago and I'd stop thinking about you know [3:23] because I thought at least you know I've [3:25] got some grasp of this and almost always [3:27] I'll I'll have a new angle right right [3:30] and for the really truly deep ideas [3:32] computer science or anywhere any other [3:35] field you know uh there there are many [3:38] ways of looking at these deep ideas and [3:42] I'm going to show you you know a couple [3:44] ways of looking at this this program um [3:47] but I'm not kiding what I can say say [3:50] that I'm going to spend the rest of my [3:51] life trying to understand it and there [3:53] are many other people who've tried to [3:55] spend you know their careers basically [3:58] understanding aspects of this feline [4:00] program and you know to give you sort of [4:03] a reminder of you know a feline program [4:07] the amount of complexity you can fit in [4:08] there does anyone know about the [4:09] collapse [4:11] function what's the collapse [4:18] function yeah it's this little a little [4:21] function you like three and plus one and [4:25] you know you have like a division by two [4:27] or something like that and you know [4:30] basically you're trying to figure out if [4:31] you give an integer a positive integer [4:34] as an input will this operation [4:37] terminates just got some multiplications [4:39] additions and divisions right and it's [4:40] like a tiny little program and you know [4:42] it's like a three line or two line [4:44] program and uh the best mathematicians [4:47] in the world have been trying to prove [4:49] for many decades utterly without success [4:52] that this program always terminates if [4:54] you give a positive integer and Paul [4:56] arish one of the great mathematicians at [4:58] all time at one point said mathematics [5:00] is not ready for the the collapse [5:04] problem right so um so that's a [5:07] three-line program who stumped some of [5:10] the greatest Minds in history so I'm [5:12] talking about like a feline program okay [5:15] so that should give you [5:17] pause that should give you pause and we [5:20] all have to have a healthy amount of [5:22] respect for the the 3x5 card program um [5:27] so anyway uh the program I'm going to [5:30] talk about is an interpreter for lisp [5:33] written in lisp and um it's one of these [5:39] things where if you don't know lisp and [5:41] you first see it you're like well what [5:43] are these parentheses and then after a [5:44] while you kind of start figing what this [5:46] Lambda thing that's that's uh something [5:49] to wrap your head around and why are [5:50] there two lambdas like nested what does [5:52] that mean and you kind of go over over [5:55] these different ideas of time and [5:57] eventually you kind of get some sense [5:58] you trace through bunch of programs and [6:00] like all right kind of get some sense of [6:02] what's going on and then you start [6:03] modifying The Interpreter and one of the [6:05] great things about this program is that [6:09] there's so many ways to change it and [6:11] explore it and play with it you can add [6:14] arguments to The Interpreter you can [6:16] rewrite The Interpreter in a variety of [6:19] correctness preserving transformation [6:21] Styles one uh program transformation you [6:25] can apply a sign called continuation [6:26] passing style which I consider the weed [6:30] drug of program Transformations you know [6:32] normally you CPS that sucker and then [6:34] from then on you know it's Off to the [6:37] Races so you know you CPS an interpreter [6:40] you CPS it [6:42] twice that gives you delimited [6:46] continuations and now you're cooking [6:47] with gas you can add a store argument to [6:52] The Interpreter right you can add boxes [6:56] and you could start doing you know [6:58] mutation and side effects in different [7:01] ways you can do call by value versus [7:03] call by need versus call by name [7:06] trivially right um You can do all sorts [7:09] of things that are really deep and give [7:11] you deep insights into concepts of [7:13] programming languages that you'll use [7:15] you know the rest of your career or the [7:17] rest of your hobby uh years or whatever [7:21] and so uh I don't know of any other [7:23] artifact in all of computer science that [7:25] packs so many ideas and the potential [7:28] extensions to explore so many different [7:30] areas uh as this interpreter and in fact [7:34] um you know Alan K uh said that when he [7:39] first saw the lisp interpreter written [7:41] in lisp at the bottom of page 13 of the [7:44] lisp 1.5 manual right it changed his [7:48] life and he realized these are Maxwell's [7:51] equations of software right it's very [7:53] much the same write down four little [7:55] equations it helps if you like take them [7:57] from the other mathematicians and [7:59] physics and call them Ma anyway but you [8:02] take you know you write down the four [8:03] equations and you put that on the 3x5 [8:06] card right and then you spend the rest [8:07] of your life trying to understand what [8:09] those four equations are uh what the [8:11] implications are so that's very much [8:13] what this interpreter is and I'm I you [8:16] know I can't I can't do justice to it I [8:19] can only show you a couple of the many [8:21] aspects of this multi- aspected you know [8:24] beautiful system and many of which you [8:27] know I I feel like I'm a complete Noob [8:28] to [8:30] um but I can tell you that there are [8:32] very interesting things out there so for [8:33] example there's this idea of reflective [8:37] towers of interpreters we have an [8:39] interpreter interpreting an interpreter [8:41] interpreting an interpreter that part's [8:43] already interesting but when you have [8:45] infinitely deep tower or infinitely tall [8:48] tower that's when it starts getting fun [8:50] and in particular it becomes especially [8:52] fun when The Interpreter being [8:55] interpreted by another interpreter can [8:57] reach back up into The Interpreter [8:59] interpreted it and change the [9:01] semantics of itself by changing how The [9:05] Interpreter interpreting it works and [9:08] this is one of the things that Dan [9:10] fredman says he refuses to work on [9:12] because it melted his brain too much [9:15] it's like basically the one thing that [9:17] he's like who won't he won't touch [9:18] anymore so uh that's the sort of fun you [9:21] can have you know it's bad enough having [9:24] a five or six line program but when you [9:26] have infinitely many of them interacting [9:28] in these ways then you can do very [9:30] interesting things and if you're [9:31] interested in that sort of thing I would [9:33] point you to the work of kichi asai and [9:36] also uh my friend Nat Min gave a keynote [9:39] at uh strange Loop a few years ago and [9:41] she talked about this I think she called [9:43] The Talk programming should eat itself [9:46] and she talked about this reflective [9:48] Tower idea okay so that's that's just [9:50] one aspect you can go [9:52] deep you can go deep that direction if [9:55] you want I haven't touched that yet uh I [9:58] want to connect that [9:59] with the thing I'm going to show you and [10:02] even the people who do uh this type of [10:05] very bizarre programming they kind of [10:06] get scared look on their face when they [10:09] start thinking about the implication so [10:11] that's that's a good that's a good [10:13] feeling when you know you're scaring the [10:15] veterans of the Lambda [10:17] calculus um so that's you so so that's [10:21] something I want to [10:22] accomplish and there are many many other [10:25] directions you can go program [10:26] transformation directions different [10:28] evalu valuation orders all sorts of [10:31] things and then you can layer a type [10:32] system on it that kind of thing now you [10:34] have The Interpreter and the type [10:36] influencer and they share structure and [10:38] you can have them interact in [10:39] interesting ways and all these sorts of [10:41] things so um just like CPS is the [10:44] gateway drug of program Transformations [10:46] lisp and lisp is the gateway drug of the [10:50] whole world of programming languages I [10:53] think so uh what we're going to do is [10:57] write an interpreter we're going to [10:59] write the lisp in lisp in the way that [11:02] Dan wrote it and Paul Irish the great [11:05] mathematician had this idea that there [11:07] was a book that God kept that had every [11:10] beautiful proof in it only the beautiful [11:12] ones and every once in a while he or [11:15] someone else would come across a [11:16] particularly elegant and beautiful proof [11:19] oh that's a proof in the book and so [11:21] we're going to see a program in the book [11:23] this is the program of the book I've [11:25] written hundreds of interpreters and [11:27] I've read lots of books on interpreters [11:29] but this to me is the one in the book [11:32] everything else is a pale [11:35] imitation all right so who here uh is [11:40] familiar with s Expressions symbolic [11:42] expressions or some flavor of list they [11:44] can read parentheses all right maybe [11:47] half and a half okay well I'll teach you [11:50] how to do it I'll teach you how to do it [11:53] and some of the things I'm going to show [11:54] you you know like I said this is [11:56] jam-packed full of deep ideas and I can [11:58] only scratch the surface but even [12:00] scratching the surface may leave you [12:03] dizzy if that's the case close your eyes [12:07] lean forward and the room will stop [12:10] spinning and then as we go on you'll be [12:13] able to hopefully pick up on some of the [12:16] concepts and ideas and I'll show you [12:17] some stuff at the end that maybe uh will [12:19] be surprising to you even if you don't [12:21] understand all the details and the great [12:24] thing is that once you have some sense [12:26] of what this is about you will be filled [12:29] with a fiery passion to learn all the [12:31] rest and I can point you to some some [12:34] references for that or we can talk about [12:36] it over a [12:37] milkshake so the first thing I'm going [12:40] to do is talk about lists let's talk [12:44] about lists so scheme is a lisp and lisp [12:49] comes from list processing that's what [12:52] lisp stands for list processing so we're [12:54] going to talk about lists and symbols [12:57] that's the first thing we're going to [12:58] talk about so let me go ahead and start [13:00] up trusty sha [13:02] scheme which is now covered under an [13:05] open source license [13:08] woohoo all right so sha scheme has this [13:11] thing called the repple and it's [13:13] pronounced reppel not [13:15] reple and this you probably familiar [13:18] with if you've used other languages that [13:21] have interactivity one of the cool [13:23] things about a good scheme [13:25] implementation is that even though I'm [13:26] typing Expressions interactively those [13:29] those get compiled on the fly directly [13:31] to machine code actually at least some [13:33] versions of say shay does an analysis [13:36] first to determine whether or not it's [13:38] faster to evaluate it or faster to [13:40] compile and evaluate it um so um this is [13:44] faster in general than in a lot of [13:46] systems okay let's write a simple scheme [13:50] program like five five evaluates to five [13:55] all [13:55] right uh we don't have to make it [13:58] evaluate to five but let's pretend that [14:00] we will [14:02] now what else can we have we can have a [14:05] list containing five and you could see [14:09] the list is represented by these [14:12] beautiful [14:14] parentheses we can have a list [14:17] containing five and [14:19] six notice that I did [14:23] not defile my program with commas or any [14:29] else like [14:36] that we can have a list that contains a [14:43] list what do you think's going to [14:46] happen more parenthesis look at [14:50] that we can go [14:53] deeper we can go as deep as we [14:56] want so we have lists we can have lists [14:58] of lists what is another name for a list [15:00] of [15:01] lists a [15:04] tree oh have you ever heard of [15:06] trees right have you heard of this thing [15:09] called XML this new fangle [15:12] thing do you know what language came [15:14] before [15:16] XML what [15:18] language sgml yes right you have you [15:21] heard of something a beautiful thing [15:23] called [15:25] xslt brings joy into your heart do you [15:27] know what the sgml equivalent of xslt [15:31] was see see who knows the Obscure [15:34] stuff disle has anyone heard of dle [15:38] dsssl what is that Dynamic style and [15:42] semantics language or whatever something [15:44] like that you know what dle was it was [15:47] lisp it was R4 RS scheme because if [15:52] you're going to work on tree structured [15:55] data what's the right way to work on it [15:58] a tree is an inductively defined data [16:00] type how do you deal with that recursion [16:03] that's how you deal with trees so lisp [16:07] is all about recursion and dealing with [16:10] trees programs most programs represented [16:13] as trees if you're going to have a [16:15] programming language that can modify [16:19] programs what better way to do it well [16:22] they'll be people the has scers will say [16:24] they're better wayson but anyway don't [16:26] don't listen to them [16:30] okay so we have lists and things like [16:33] that by the way if you want to learn [16:35] scheme there's an awesome interactive [16:37] fiction game by Andrew Plotkin AKA zarf [16:39] called lists and lists where a genie [16:43] teaches you to program and scheme and [16:45] you can actually Implement logic [16:47] programming inside of that scheme [16:49] although eventually you'll run out of [16:51] memory because the Z machine doesn't [16:52] have that much space but anyway it's a [16:54] good exercise so we have lists we have [16:57] list contained lists which are trees we [16:59] have numbers which evaluate to [17:00] themselves there are other values like [17:03] hasht is a representation of Truth there [17:07] is no representation of beauty but we [17:11] have hash F which is a representation of [17:13] false an interesting fact about scheme [17:16] is that every value in scheme is [17:18] considered true except for hash F so [17:20] five is considered true well that that's [17:23] beautiful is open to [17:26] debate um so we have also this amazing [17:30] and very deep operator called quotation [17:33] quote quote and that is the topic of a [17:38] lot of stuff I won't get into but you [17:40] know quote itself this is a very [17:42] controversial operator how it should [17:44] behave you know people have created [17:46] entire versions of lisp just based on [17:49] different Notions of quotation but in [17:52] scheme the way quote works is quote of [17:54] anything gives you back that thing okay [17:57] so we quoted five we get back five we [17:59] actually don't need to quote five quotes [18:01] five is something called a self quoting [18:03] or self-evaluating literal but we can do [18:05] things like quote a list we can quote a [18:08] list of 56 and we back the list 56 we [18:11] can quote the empty [18:13] list which has nothing in it because we [18:17] use quote so much we don't necessarily [18:19] want to write quote this way we're going [18:21] to have a Shand scheme doesn't have a [18:22] lot of short hand but this is one of [18:24] them so we're going to [18:26] write this quote some of like that 56 [18:31] okay this I will allow uh I don't like [18:35] too much you know messing with my [18:38] symbolic Expressions but this will be [18:39] okay and then in addition to having [18:42] things like numbers and lists and list [18:44] containing lists in true and false [18:46] values or booleans we have an amazing [18:49] thing called the [18:50] symbol and if you program in Java I'm [18:54] sorry you don't get symbols if you [18:56] program in many languages you don't get [18:57] symbols but you do have symbols in in a [19:01] scheme in most lisps so we can say [19:06] milkshake with a quote around it and [19:08] that gives us back milkshake milkshake [19:11] is a symbol it's a symbol it's not a [19:13] string strings are different symbols are [19:16] things that represent metaphorically [19:18] objects that we might care about okay [19:20] this is an atomic value we can't tear it [19:22] apart we can't do anything like that [19:24] it's just it's a unique thing and it [19:26] turns out internally it's fast to [19:28] compare symbols so we can use symbols to [19:30] represent interesting data we don't have [19:32] to say we're in C and so a milkshake is [19:36] five or whatever it is right so we can [19:38] do we can do things like this which are [19:40] classier okay so we have symbols lists [19:43] we can have symbols inside of our lists [19:45] and things like that we can also make [19:48] decisions we can um do things like ask [19:52] if a list is empty so I can say is the [19:56] empty list null so if I have a [20:00] list which PRS the thing that comes [20:03] inside the PRS first that is basically a [20:07] function call unless is something like [20:09] quote there are something called special [20:11] forms that have special evaluation rules [20:13] but in this case we're just calling a [20:15] function and the function you can tell [20:17] is a predicate has a question mark [20:19] that's going to return true or false [20:21] okay so we are asking if the input [20:24] expression evaluates to the empty list [20:28] and it does [20:29] we can ask if five is [20:31] null five is not null okay so we can [20:35] make a function call we have Notions of [20:37] predicates we can [20:39] also um build up lists in other ways [20:42] that I haven't shown you yet so I shown [20:44] you two ways of list I can just quote a [20:46] literal list or I can call a function [20:48] called list 34 five I can also [20:54] um build up list likee structures using [20:57] an operator called cons cons for [21:00] construction in fact Dan Freedman who [21:02] was my adviser uh wrote a very famous [21:05] paper with David Wise 1976 called KH [21:07] should not evaluate arguments which was [21:09] one of the first papers on laziness like [21:11] you have in Haso and there was another [21:13] paper by Henry Baker called KH should [21:15] not cons this arguments and that's like [21:17] must have stayed up all night coming up [21:19] with that [21:21] one so the typical way to use cons is to [21:25] con some object onto an existing list so [21:28] we can cons five onto the empty list now [21:30] we get a list containing five you know [21:32] and and I can build up chains of things [21:34] using cons so I can cons six onto the [21:37] list I get back from the cons 5 cons [21:39] takes two arguments and I can build [21:41] these lists up okay all right so that's [21:46] cons and we've seen like the null test [21:50] let me show you how to make a a choice [21:53] so I can use something like [21:55] if if five is null [21:59] then return six otherwise return seven [22:02] so if has three sub Expressions we have [22:05] a test expression What's called the [22:07] consequent expression and then the [22:10] alternative expression so what would be [22:12] the value of this [22:14] expression seven okay all right so [22:17] that's one way to make a choice and [22:21] there there are other ways another way [22:23] to make a choice is something called [22:26] cond and the reason I'll use this [22:28] notation um the reason that we have this [22:32] cond operator cond is conditional [22:34] operator is that it may be that we want [22:37] to make lots of [22:38] choices so instead of having nested ifs [22:42] which gets annoying at some point we can [22:44] do something like [22:51] this okay what do you think this [22:53] expression will evaluate [22:55] to eight all right great [23:00] awesome I'll show you a couple other [23:02] things uh one is you know we can do [23:05] things like addition or multiplication [23:09] okay so addition is like [23:11] plus it's actually a function bound to a [23:14] procedure that knows how to do addition [23:16] we also have multiplication so I [23:20] can right and so I can deal with big [23:24] nums arbitrarily large Precision integer [23:26] so that's multiplication [23:28] and um I can also do things like [23:32] Define I can Define functions I can [23:35] Define all sorts of things I can give a [23:37] name to something I'll call this I don't [23:40] know I just had a Tarot milkshake so to [23:43] find tarot to be quote good there's a [23:48] symbol and if I type tarot then the [23:50] variable gets looked up and something [23:52] called an environment and I get back the [23:55] value of that variable which is a symbol [23:57] good so Define just gives a name to some [24:01] value I can give other sorts of values [24:03] if I want doesn't matter um and another [24:07] concept is that of a function and the [24:10] reason or procedure technically and the [24:13] way I create a procedure is with this [24:15] expression called Lambda you type it l m [24:17] BDA but I've got this fancy thing that [24:19] turns it into a symbol and what you do [24:22] with Lambda [24:24] is you have a list of arguments these [24:28] are noral parameters to your procedure [24:30] and then you have a body so this is [24:32] Lambda XX is the way i' pronounce it and [24:35] this is just going to return its [24:36] argument the value of this argument so [24:38] this is the identity function the value [24:40] is the identity function and we've [24:42] already seen that you can write [24:44] parentheses and Par parentheses normally [24:48] mean a procedure call we're not [24:50] specifically calling it but that's [24:52] that's the case unless we have what's [24:54] called a special form in the first [24:56] position like quote or def [24:59] something like that so I am going to [25:01] apply to [25:02] apply that the value of that uh Lambda [25:06] expression which will evaluate to a [25:08] procedure to the expression five five is [25:11] an expression that evaluates to the [25:13] value five so we are starting to have [25:15] the notion of expression versus value [25:18] and I get back five through a mechanism [25:21] that involves a number of steps we [25:23] evaluate the argument Expressions [25:27] there's something called the operator [25:29] expression the rater and the Rand the [25:32] operand we evaluate the operator that [25:35] evaluates to procedure of one argument [25:38] we we evaluate the Rand expression that [25:42] evaluates to itself in this case and [25:44] then we perform a procedure [25:46] application and we apply that procedure [25:49] to the value of the argument and we get [25:51] back five in this case Okay so that's [25:53] the mechanism that we're going to [25:56] implement and I can of course [25:59] give a [26:01] name to a function I can let me call it [26:09] double okay so now I have a body that's [26:11] a little more interesting and I [26:14] can double my [26:16] fun that doesn't work the hasc is are [26:20] going to give me grief but I could [26:22] double five and get two in binary so you [26:27] can double anything you want and I can [26:30] Define all sorts of things so I can uh [26:33] do things like Define define to be [26:37] five [26:38] right why is that a oh that's a great [26:40] thing so um I can do a lot more than [26:45] that I can change what Lambda means and [26:47] things like that that's where the real [26:49] fund begins I'm not going to talk about [26:50] that that's uh for the next talk but I'm [26:54] going to restart my [26:56] scheme just say [26:59] saying just saying I could I could fly [27:02] solo with that one but I know how to do [27:04] it but I'm not GNA do you're not ready [27:07] yet you're not ready [27:11] yet okay so so now you know scheme okay [27:17] now well you're joking or you think [27:19] you're you think I'm joking but that's [27:21] basically all you need okay there's one [27:23] other thing I'm going to talk about or [27:25] show you very quickly that's not [27:26] technically uh into scheme but it's easy [27:30] to add because scheme has this very [27:32] powerful macro system that allows you to [27:34] extend the language in different ways [27:37] and so what I'm going to do is I'm going [27:38] to load a macro for pattern matching [27:41] something called [27:43] pmch and this is just one of many [27:46] systems that allow you to do pattern [27:48] matching and so basically pmch is [27:51] similar in spirit to our cond except now [27:54] we are going to match against an [27:55] expression so I can say we're going to [27:58] match against list 34 and now we can [28:01] have just like with a cond different [28:03] pattern or different expression or [28:04] different Clauses but now we're going to [28:06] match against a pattern so I could [28:11] say I have a pattern that matches [28:14] against list of two [28:16] arguments and these commas I'm not going [28:19] to really get into the details of what [28:21] the commas mean syntactically but [28:23] basically you can think that this list [28:25] of two elements is getting pattern [28:28] matched against the list we get back the [28:29] list 34 so the X will be associated with [28:33] or bound to three the Y will be bound to [28:36] four and then on the right hand side we [28:40] can use the those x's and y's and sure [28:45] enough we get back seven okay so that's [28:48] what P match does if you haven't seen [28:50] pattern matching before it's very [28:51] powerful especially in conjunction with [28:54] a form of quotation and scheme called [28:56] quasi quotation or back quote that's [28:58] really what's going on if you know [28:59] scheme there's an implicit back quote [29:02] here okay and those commas are called [29:06] unquote all right so now we know [29:10] basically everything we need um to write [29:12] an interpreter so let's do [29:15] that all right so let me go back to my [29:19] file here so I'll load my [29:21] pmch and I can put this code up online [29:24] if people want to see [29:25] it all right [29:29] okay so one thing that we need to um do [29:34] is you know decide on the name for our [29:38] interpreter that's the hard part right [29:40] so names are hard what would be a good [29:43] name for an [29:44] interpreter [29:49] Fitzroy Define Fitzroy how do you spell [29:54] that all right so we have a name this is [29:58] our life now and thank you derailed us [30:03] all so um well what do you think I [30:07] should type [30:13] next p match almost we're not quite [30:16] ready the arguments so we need to define [30:18] a function procedure that's going to do [30:20] something so I have to type [30:22] Lambda that's a good thing when in doubt [30:25] the answer is Lambda right [30:28] so we have a Lambda expression it's [30:31] going to take some arguments okay so if [30:33] we looked at our interpreter here when [30:35] we writing stuff like Plus three4 or our [30:38] our reppel or this is basically an [30:41] evaluator interpreter whatever you want [30:43] to call it technically it's not an [30:45] interpreter that's a form of of [30:47] evaluation but it's an evaluator um so [30:51] if you look over there we have an [30:52] expression coming in and we evaluate the [30:55] expression to get a value back so [30:58] we can have an expression that's a good [31:00] name and I'm going to call this eval [31:04] expression okay Fitzroy would have been [31:07] fine but this is a vow [31:10] expert it's important as a safety tip to [31:13] not call that argument exp now why would [31:17] that [31:18] be yeah because scheme has an [31:21] exponential function built in called X [31:23] and if you [31:26] type you get very errors if you do it [31:29] wrong so I call it exper all [31:35] right uh yeah if you call your function [31:37] AOW hilarity May [31:39] ensue can always [31:42] restart [31:45] now now it's time for p match and what [31:48] are we going to P match against well [31:51] guess what we don't have a lot of choice [31:54] how about [31:55] exper all right so we're going to PE [31:57] match against it like writes [31:59] itself okay so what sort of Expressions [32:02] do we want to have in our language how [32:05] about numbers numbers a good thing to be [32:08] able to evaluate we had five right that [32:09] was our first scheme program so we're [32:11] going to have program we're going to [32:12] evaluate five so the way that uh you [32:17] write that pattern is that comma in will [32:19] match against anything and I mean [32:22] anything so that's no good we have to [32:26] add something called a guard where we [32:28] can add a [32:29] predicate and so the [32:31] predicate is basically part of this [32:34] matching process so if the pattern [32:37] matches against exper then Additionally [32:40] the guard has to return a true value [32:42] that is any other value value any [32:45] anything other than hasf in order for [32:47] the entire pattern to be considered [32:49] matching and in which case we try the [32:51] right hand side yes [33:00] we could we could totally use a a cond [33:01] here and uh in that case we could just [33:05] have you know the number question mark [33:07] of in right uh so right now it's not [33:09] really paying for itself it's a lot a [33:11] lot more mechanism than we need but when [33:13] we start getting the things like Lambda [33:15] that have more structure we could do [33:17] that's a very good question we don't [33:19] need pmatch okay this should be very [33:21] clear we could do everything with car oh [33:23] sorry did I talk about car car we'll [33:25] talk about car in a minute maybe maybe [33:27] maybe we can avoid talking about car [33:29] we'll see there's like a historical [33:31] accident that involves some of the names [33:34] and scheme that have not yet been [33:36] corrected intentionally uh but we don't [33:39] talk about that so uh anyway so we we're [33:43] we're going to use P match for reasons [33:44] we'll see in a minute we don't have to [33:46] so what do you think a number should [33:48] evaluate [33:50] to itself okay sounds good so we'll just [33:53] write down n so now we have an [33:56] interpreter so let's try it [34:00] well you know I don't have that much [34:03] time okay so we're going to load this [34:07] thing uh interp that [34:11] SC okay and now we can test it eval [34:16] exper and all right someone give me a [34:19] nice expression to [34:21] evaluate five you're you will go far but [34:26] that's the wrong answer the right answer [34:28] is quote of five because we want to make [34:32] sure that whatever expression we pass in [34:35] is not evaluated by scheme a classic [34:38] error let me show [34:41] you well our interpreter works so [34:44] well that we already can handle [34:48] addition wow that's really [34:51] impressive and if you've written enough [34:53] interpreters you've run into this [34:54] problem before it's like whoa that's I [34:57] guess I can in my homework [34:59] early okay so that's why we put a quote [35:02] in front of whatever we're passing in so [35:04] really quota five all right well maybe [35:06] we want to have more things than just [35:09] numbers how about we [35:12] add add [35:13] one add one is a function and scheme [35:17] that adds one to his numeric argument so [35:21] let's Implement add [35:23] one so [35:26] um let me add another Clause here and in [35:29] this case we're actually going to match [35:31] against a [35:32] list okay so we see list structure and [35:36] now you start seeing why we're using [35:37] pmatch so the expression we expect is an [35:40] add one expression which has a [35:43] subexpression inside of it this could be [35:45] arbitrarily complicated this doesn't [35:47] just have to be a number this could be [35:48] something that evaluates to to another [35:50] such as another called add one okay all [35:53] right so what do we do now in this case [36:00] oh yeah add one well where did we get [36:02] add one [36:05] from scheme we hope it's built in we'll [36:08] see all right so I'm going to call Val [36:13] expert inside of e all right so I'm [36:18] going to use schemes add one to [36:21] implement add one in my language okay o [36:24] that's cool so let's try it [36:33] okay so now let [36:35] me quote add [36:39] one okay and then I can always do the [36:43] test like this because otherwise you [36:46] might accidentally not evaluate the sub [36:49] expression okay all right so now we can [36:52] do add one that's [36:55] great all right and uh I have one called [36:59] sub [37:00] one all right same thing right all right [37:05] I should have used copy and paste [37:06] abstraction well I kind of did but okay [37:10] so you see how this [37:12] goes that's fine we could add a few [37:15] other things so we could add something [37:19] like [37:22] multiplication now multiplication is [37:24] interesting because our version [37:26] multiplication is going to take two [37:28] sub Expressions o E1 and E2 so now how [37:31] do we write this [37:35] thing how many recursive calls do we [37:37] have to make two two right wow this is [37:41] like falling off a log whoops all [37:44] right okay so we're going to [37:47] multiply what we get back when you [37:50] evaluate [37:51] E1 and E2 and multiply that okay all [37:55] right uh let's do another one how about [38:01] if so we I already told you there's a [38:03] test and a consequent and an alternative [38:08] so how do we evaluate [38:10] if any ideas this is tricky if using if [38:15] you're catching [38:17] on all [38:18] right how about [38:21] if eval [38:23] expert of T copy and paste [38:31] substraction yeah all right there's [38:35] probably like a copy and paste Monet and [38:37] has or something [38:39] right so copy and paste substraction now [38:42] we have if [38:50] great uh can we short circuit well for [38:53] for things like and and or we might want [38:56] to do short circuit of valuation for if [38:58] we're going to have to evaluate the test [39:00] but if semantics are that if the test is [39:03] true we will only evaluate the first sub [39:06] expression otherwise we'll only evaluate [39:07] this sub expression so they they won't [39:09] both be evaluated [39:12] okay okay [39:16] now basically this interpreter is pretty [39:19] boring all right it's pretty boring and [39:22] the reason is we have not gotten to the [39:24] beautiful part of The Interpreter the [39:26] beautiful part The Interpreter has to do [39:28] with three lines and only three lines [39:31] what are those three [39:33] lines [39:36] Lambda that's the I told you it's always [39:38] the answer [39:39] right told you what's the second one [39:43] it's not Lambda what was that apply [39:46] application and the third [39:49] one not a [39:51] vow not [39:53] procedure was [39:55] that not Define [39:59] not quote Oh wow all right I stumped [40:01] y'all ha all right we'll figure it out [40:04] in a minute okay so let's uh try you [40:10] know what uh let's try [40:12] doing let's try doing a vow Okay so [40:16] we've already seen the syntax and scheme [40:18] it's minimalist I'd say not Roco and [40:23] basically we have a Raider expression an [40:26] operator expression and an upper Rand [40:28] expression if you read a book and you [40:30] see Raider and Rand that's what they [40:31] mean you want to put this line last in [40:34] your pmch so it doesn't overlap this [40:36] pattern does not overlap with the others [40:38] this becomes fun when you start doing [40:40] logic programming where the ordering [40:42] isn't supposed to matter but in this [40:43] case P match evaluates in the top down [40:45] and so we're going to put our our [40:47] application case last all right okay [40:50] what do we do we know the drill we are [40:53] going to evaluate via copy and paste [40:56] substraction the Raider and the Rand [40:59] perfect evaluate the [41:02] Raider and evaluate the [41:07] Rand all right now what do we do with [41:11] those two aru two values the raer is [41:14] supposed to evaluate to a procedure some [41:16] representation of procedure and this is [41:18] going to evaluate to some argument that [41:20] we're going to call the procedure on so [41:22] what do we do now apply it how do we [41:25] apply it [41:27] no Lambda doesn't apply but you're right [41:30] that I got caught up we're going to use [41:32] apply which is through [41:35] parentheses right that's it if you blink [41:38] you'll miss it some people have what [41:41] might call parentheses blindness and [41:43] they like just can't see that that is [41:45] different than without those parentheses [41:47] but they are different there you know [41:49] there's no mistaking the difference in [41:52] Behavior okay so that is our [41:55] application uh very nice so that's one [41:57] one of our three magic operators we also [42:00] have this thing called Lambda so I can [42:02] match against the Lambda expression this [42:04] is where the pattern matching comes in [42:05] nicely and I can give a name to the [42:08] variable and I can have a body [42:10] expression okay H so something's got to [42:15] have to happen with the [42:17] Lambda do you see that x what is [42:22] X well there's a list containing X but [42:25] the X itself not part of the list what [42:27] is is that mean what is that [42:30] thing it's an [42:32] identifier and if the X were to appear [42:34] inside of Rand what would that [42:38] be it's a variable reference okay so [42:41] this is how we have a variable reference [42:43] and what's the value of the variable X [42:46] tell [42:47] me don't know yet when will you [42:53] know no at runtime when we've actually [42:55] done the procedure application that's [42:56] right we won't know until then so if I [43:00] call the resulting procedure with five [43:03] as the argument what would be the value [43:04] of [43:05] x five so we have this idea that if a [43:09] variable appears in the body at some [43:12] point we may have to look up the value [43:14] associated with that variable or bound [43:15] to the variable and in order to do that [43:17] we need some mechanism for variable [43:19] lookup and the traditional way of doing [43:22] that in this sort of interpreter is [43:23] called an environment so we are going to [43:26] write an environment passing interpreter [43:30] okay anytime you hear passing that means [43:33] that there's going to be an argument [43:35] coming in to our function for The [43:37] Interpreter so you see right now we [43:40] basically have a calculator we have an [43:42] expression but there's no context of the [43:45] expression there's no notion of variable [43:47] Bindings that may be you know in play at [43:50] this point so we're going to have to add [43:52] something else to this expression or [43:54] sorry in addition to the expression as [43:56] an argument [43:57] so I'm going to add an environment and [44:00] this changes [44:01] everything all those three magic lines [44:04] are going to in some way be involved [44:07] with the [44:09] environment okay so now we have an [44:12] environment and the environment is going [44:15] to contain somehow associations between [44:18] variables and values now what do you [44:21] think the third magic line of code is [44:24] based on what you've seen [44:28] parenthesis this is the parenthesis line [44:31] the [44:31] application cons nope cons is useful but [44:35] you actually don't need it you only need [44:37] these three lines that's turn complete [44:39] actually it's amazing we can delete all [44:40] the other junk the other stuff's junk [44:43] you don't need [44:44] it you don't need it you only need the [44:47] three lines and I'm serious about that [44:49] you only need the three lines you know [44:51] you heard of this thing called a turning [44:52] machine this came first Lambda calculus [44:55] came first [44:57] girdle didn't believe church that it was [45:01] turn complete even though turn [45:02] completeness hadn't been the term [45:04] yet okay we need one more thing no we [45:08] don't need to find [45:10] either was it variable lookup that's it [45:13] that's the last piece of magic we got to [45:15] have a way to look up those variables [45:18] all right [45:20] so I need a guard because I have my [45:23] match anything pattern and I am going to [45:26] repres represent variables as [45:29] symbols okay because we have symbols and [45:31] scheme so if we have a pattern which is [45:35] just a symbol by itself right we're [45:37] going to say that's a variable and we're [45:38] going to look it up how do we look up a [45:42] variable in the environment okay now I [45:45] have to tell you a piece of information [45:47] you don't know I am going to represent [45:49] my environment as a procedure of one [45:51] argument that takes a variable so how do [45:54] I actually look up X in the environment [45:59] uh I'm not going to evaluate it actually [46:01] look up X in the [46:02] environment like [46:04] that procedure call okay this is where [46:08] it gets kind of weird it's like kind of [46:09] Spartan right I mean I'm just like got a [46:11] procedure there's only thing one one [46:13] useful thing a procedure can do call it [46:16] takes one argument give it one argument [46:18] call it a that's that's it all right so [46:21] that's what we're doing okay great now [46:25] Lambda what are what is Lambda going to [46:33] do ah yes extend the environment it's [46:36] the magic words the environment [46:39] extension is the key thing here so [46:41] Lambda expression evaluates to what in [46:44] scheme a procedure okay so we have to [46:47] have a representation of a procedure [46:49] which you can think of as a delayed [46:50] computation where we don't have enough [46:52] information to do the computation in the [46:54] body yet but we're going to wait until [46:56] the procedure gets called and then some [46:59] value will be bound to that variable and [47:00] then we'll be able to evaluate the body [47:01] at that point because we'll have the [47:02] correct context we'll know the variable [47:04] bindings of scope so we have to somehow [47:08] represent a procedure huh how can we [47:12] represent a procedure do you think [47:15] Lambda there you [47:17] go 60% of the time it works every [47:24] time all right [47:27] Lambda ARG that's right we're gonna have [47:31] an argument coming in what is that ARG [47:33] thing do you think what does that [47:35] correspond to in the three magic lines [47:37] of [47:39] code not it doesn't correspond to X and [47:42] this is something we have to be very [47:43] careful [47:45] with it corresponds to the value of the [47:49] Rand remember the procedure application [47:52] line and the Lambda line are intimately [47:54] connected because we're going to end up [47:56] doing a procedure call on this Lambda [47:59] expression on the value of that Lambda [48:01] expression that's is going to evaluate [48:02] to a scheme procedure and we're going to [48:04] call the scheme procedure and pass in [48:06] the value of the operand therefore ARG [48:08] will be bound to the value of operand if [48:10] we're calling the identity function on [48:13] five Rand will be evaluate to five ARG [48:16] will be bound to five okay keep that in [48:19] mind okay so now what I heard was we [48:22] have to evaluate the body in the [48:25] extended environment so let's do that [48:28] how do we [48:29] evaluate the [48:33] body eval expert right if only we had a [48:36] procedure that knew how to evaluate the [48:38] body well that's what we're writing [48:40] magic of recursion evaluate the body now [48:43] we have to feed in an Express an [48:45] environment and we have to go back and [48:48] rcon these lines because they don't have [48:50] environments yet okay so we have to have [48:53] an environment so for these lines down [48:54] here it's kind of boring it's just good [48:57] old environment [48:58] okay but up here we need an extended [49:01] environment what is the extension how [49:04] are we extending the [49:07] environment Lambda that's right you [49:10] laugh it is correct you extend it using [49:12] a [49:15] Lambda yeah it's a one trick pony but [49:18] it's got a good [49:19] trick [49:21] lamba [49:23] why all right this is when the nerd [49:25] chills start [49:29] okay that is an environment remember we [49:33] wanted to look something up we called X [49:36] on the environment well that's the sort [49:38] of creature we're talking about a [49:40] procedure of one argument we're creating [49:41] a procedure of one argument that's our [49:43] environment it's our extended [49:44] environment so what are we going to do [49:45] with that environment what's going to [49:46] happen [49:48] inside if oh wow yeah that's right we [49:52] have to make a choice if of what oh I [49:55] didn't tell you this part yet [49:58] if equals well there's this thing called [50:01] EQ huh okay if what is equal what two [50:06] things do we want to [50:07] compare Y and X okay if they are equal [50:12] then what do we [50:14] return not X [50:17] AR this is the critical piece and here's [50:20] the other critical piece what do we do [50:23] if they don't if they aren't equal [50:27] in we're going to look up an in what do [50:29] we look [50:30] up y not X Y because Y is what's coming [50:34] in that Lambda the innermost Lambda that [50:36] innermost Lambda is an environment [50:38] extended environment that Lambda right [50:40] there is a procedure so we have what's [50:43] called a higher order representation of [50:45] environments and procedures in our [50:48] interpreter okay so let me go and fix up [50:52] my vow experts to give them environments [50:55] see these lines are boring because we're [50:56] not messing with the environment at all [50:59] that's not interesting at all and you [51:01] could say the application line isn't [51:03] messing with the environment and that's [51:05] true with this [51:07] representation of procedures and [51:09] environments but if we change our [51:10] representation of procedures and [51:11] environments it actually does matter [51:13] you'll see that if we were to use data [51:16] structures such as lists to represent [51:19] our environment and procedures then the [51:23] this application line would have a [51:24] different looking structure BAS [51:26] basically the work that we're doing up [51:28] here in the Lambda line we get put into [51:30] the application line all right so in [51:34] theory this should work [51:36] now we'll see if you all were paying [51:39] attention Okay eval expert let's try it [51:43] out okay so add one hopefully still [51:47] works [51:49] oh all [51:52] right we didn't pass it in oh I need oh [51:56] the call was wrong o very CL very clever [51:59] okay so you're right we need to [52:01] call a v exper Now with an environment [52:04] what does an environment look [52:06] like [52:07] Lambda yeah again see all you need is [52:13] Lambda [52:15] y okay and what is this environment [52:17] going to [52:19] do what happens if we look up a variable [52:23] like X in this environment what should [52:25] happen error means it's not bound okay [52:29] this environment starts out with nothing [52:31] bound unless we want to put it in there [52:33] so we can do a call to schemes error we [52:36] call it look up something like that you [52:39] know [52:40] Unbound all right perfect okay we get [52:44] back to seven I can now look up a [52:46] variable in the empty environment like X [52:49] and I got my error okay I [52:52] can um go ahead and do something like [52:55] create a Lambda expression let me try do [52:57] Lambda [52:58] XX okay it gives me a procedure a scheme [53:01] procedure representing my procedure in [53:03] my language I can do a procedure [53:05] application let's see if this works I [53:07] apply it to [53:09] five and I get back five proof it works [53:13] I can do something a little more [53:15] interesting Lambda applied to Lambda so [53:18] I should get back to identity function [53:20] and I can apply the result of that to [53:24] five okay and then [53:27] uh there's one ultimate [53:31] test I think we've implemented [53:33] everything uh oh there's one more thing [53:36] we need to add let me just add one more [53:39] clause which is zero huh okay so we're [53:43] going to add one CLA more Clause to see [53:44] if something's equal to zero and we just [53:47] follow our [53:48] usual our usual thing all right and I [53:51] think that may be enough now to to do [53:55] what I was going to show [53:57] so there's one standard test case um [54:01] which tests [54:03] everything and it's [54:06] factorial and it is [54:08] factorial [54:11] using something called what Dan Freeman [54:14] calls the poor man's y combinator uh [54:17] you'll notice we don't have Define in [54:19] our language for in our interpreter [54:21] there's something called letre to Define [54:22] mutually recursive functions we don't [54:24] have that either uh well we do have [54:26] Lambda and the answer everything is [54:27] Lambda as we know so this code here is [54:33] factorial you can see this got some [54:35] function calls and stuff like that but [54:36] it maybe you can believe the math and [54:39] then that little part up top with a [54:40] bunch of lambdas uh the part up top [54:44] basically uh is what reaches what's [54:46] called a fix point and so you can see in [54:49] scheme it works so let's see if it works [54:52] in our [54:53] interpreter I have no idea let's try it [54:56] out [55:02] yeah all right awesome well [55:08] done okay so let's look at that [55:10] interpreter real [55:11] quick and just a couple words about it [55:14] so uh the first thing I'll say is that [55:18] everything except the last three lines [55:20] is an [55:21] Abomination so we are going to remove [55:23] the Abominable [55:25] code bam bam bam bam bam bam that okay [55:32] this is the 3x5 card interpreter uh I [55:35] may have to reformat it slightly [55:37] differently for the screen but um if you [55:40] have a 3x4 meter card I guess you could [55:42] fit at this side but you can actually [55:44] write down at least on a 4x6 card and [55:47] that is the magic okay this is the key [55:49] to the universe you have everything here [55:53] you have lexical scope you have higher [55:54] order functions you have all these sorts [55:57] of things numbers you don't need them [55:59] you can do Church encoding okay uh you [56:03] don't need if you can encode if as well [56:07] you encode all those things that are [56:09] kind of nonsense yes they're useful for [56:13] efficiency and expressiveness you don't [56:16] need them this is all you need it's [56:19] turning [56:21] complete came before the turning machine [56:24] this is similar related to something [56:25] called the Lambda calculus this is a [56:28] little bit different because we're using [56:29] an environment instead of beta reduction [56:32] if you're familiar with that but a [56:35] similar idea so people would call this [56:37] The Call by value Lambda calculus [56:38] interpreter environment passing and you [56:41] can play all sorts of really interesting [56:43] games with this you can change the [56:45] representation of the environments and [56:49] the uh procedures you could use data [56:52] structures you could do lists and [56:54] pattern matching you can do all sorts of [56:55] really cool things you can add [56:57] additional arguments just like we added [57:00] the environment so now we have an [57:01] environment passing interpreter you can [57:03] add a store as well which contains uh [57:06] basically the current value of of a [57:09] variable and you can change those values [57:11] so if you have an environment and a [57:13] store that allows you to do mutation [57:15] like set bang and scheme you can also [57:18] add [57:19] continuations you can CPS The [57:21] Interpreter do another correctness [57:22] preserving program transformation CPS it [57:25] that gives you a represent of the rest [57:26] of the program at any point as a [57:29] potentially as a procedure and you can [57:31] just call that continuation anywhere you [57:32] want and you can Implement all sorts of [57:34] control structures if you CPS your [57:37] program twice you have two continuations [57:38] that gives you the limited continuations [57:40] you can do basically every control [57:41] structure at that point all sorts of [57:43] very interesting games you can play you [57:44] can change anyway I'm not going to get [57:47] into all that but what I recommend you [57:50] do is what Dan suggested to all his [57:53] students and as far as I know I'm the [57:55] only one who did it maybe other people [57:56] did he said take a 4x6 card stack of [57:59] them and spend 45 minutes writing this [58:02] down over and over again till your eyes [58:04] start [58:05] bleeding sear it into your brain and [58:08] your heart and you'll never forget it [58:11] and if you really understand it and you [58:13] try you know turning the crank and doing [58:16] a bunch of evaluations at some point [58:19] you'll start to get some idea the magic [58:21] but all of computation all of the [58:24] turnning complete processes all of you [58:28] know the notion of computable functions [58:30] are within this code the secrets there [58:33] you can do things that run forever you [58:35] know you can do all sorts of things that [58:36] are very interesting you can express [58:38] cats inside of it okay so that is sort [58:43] of like the teaser and you know you can [58:46] go off to races once you really have [58:49] this on the brain uh you can do things [58:51] like change the type of scope you have [58:54] you can go from what we have here which [58:56] is call it lexical scope or static [58:58] scoping to Dynamic scoping by changing [59:01] how the environment uh variable lookup [59:04] works and things like that I'm not going [59:06] to go into all those things if you're [59:08] interested in that there's a book called [59:10] Essentials of programming languages um [59:12] by Dan fredman and Mitchell Juan that [59:15] talks about a lot of these things and um [59:18] there lots of other resources you can [59:20] find what I want to show you uh now is [59:25] what happens when you play these these [59:29] games um in sort of a different [59:32] context [59:38] so [59:42] uh this is a a paper by John McCarthy [59:45] called a micro manual for lisp not the [59:47] whole [59:48] truth and in this he gives the [59:51] rules for an interpreter okay so you [59:54] were asking about cons well here's your [59:56] cons this is what cons does and he you [60:00] know he gives gives basically the rules [60:02] for for a lisp [60:04] evaluator and you know basically he's [60:06] calling his evaluator value that's our [60:09] Val expert um and you can see that he [60:12] has these equal signs he's saying that [60:15] expression is equal to that value now [60:19] equal the notion of equality is actually [60:21] one of the most subtle Notions in all of [60:23] mathematics and logic and computer [60:25] science anyone who thinks they [60:26] understand equality as just kind of some [60:28] throwaway idea hasn't thought about it [60:31] hard enough like homotopy type Theory [60:33] you know all these people uh trying to [60:35] understand different Notions of equality [60:37] there so it's a very deep topic and one [60:40] of the things that's interesting is that [60:42] you know we tend to read that equal sign [60:45] if we're doing programming programming [60:47] languages interpreters compilers stuff [60:49] like that basically is one directional [60:52] from left to right so we have an [60:54] expression we evaluate it we write some [60:57] function that's an evaluator we compile [60:59] it some code that's going to run it and [61:01] we're going from that expression to that [61:02] value it's not really an equal sign it's [61:04] like a right hand side Arrow if you want [61:06] to think of it that way but what if we [61:08] took the equal sign [61:10] seriously what if we seriously said all [61:13] right well this is like an [61:15] algebra right and what do you do in [61:17] algebra when you were in you know I'm [61:20] not talking about like the modern [61:22] algebra I'm talking about like you know [61:24] when you were in high school or whatever [61:25] whatever you took algebra in high school [61:27] what sort of things did you do in [61:29] algebra solve equations you put in [61:32] variables like X and Y and Z and things [61:34] like that and you're supposed to figure [61:35] out what is the value of that variable [61:38] right that makes both sides equal we're [61:40] going to do that so I've done some of [61:43] the heavy lifting for you with a bunch [61:45] of other people we spent like the last [61:47] 12 years doing it and I'm going to show [61:49] you some of the stuff that we got from [61:51] it so what we did was we [61:54] wrote um and I started this at Indiana [61:58] with Dan fredman a bunch of other [61:59] talented people I'm working right now [62:00] with a whole bunch of other people incl [62:01] including like Michael Ballentine at [62:03] Utah and Greg Rosen blat and all these [62:05] other fine folks uh we wrote an [62:08] interpreter [62:10] in what's called a logic programming [62:13] language okay or a relational [62:15] programming language I really what I [62:17] normally call [62:18] it and uh this one doesn't fit on a 3x5 [62:23] card but it's not that long actually uh [62:25] it's what 43 lines but you can fit the [62:29] 3x5 card version on here quite nicely [62:32] and actually it looks a lot like the [62:34] algebra part in fact you can write down [62:36] the [62:37] semantics you know so here are the three [62:39] lines we wrote for our [62:42] interpreter this is how you would write [62:44] it in like an operational semantics so [62:47] sort of mathy and then this is on the [62:49] right hand side is how you would express [62:50] it in this language called mini Canon [62:53] and you can see it's really not much [62:54] longer it's about the about the same [62:55] same [62:56] length Okay so anyway we took the time [62:59] and wrote this interpreter so we wrote [63:01] something equivalent to a Val X but in [63:03] fact you can see it's called a Val Expo [63:05] right we even use the same name and so [63:08] now let me see if I can figure out how [63:10] to load this thing that's the it's [63:12] always the hard [63:14] part all right here's the transcript [63:17] save that all right now let's go in here [63:23] and let's see load [63:26] MK you know it's all fine and good until [63:29] you have to do things like load a file [63:31] right there's no math for that probably [63:34] a monad or something junk for that but [63:36] anyway let's let's do full [63:39] inter all right [63:42] cool so uh in this logic programming [63:45] system called mini canron um we have the [63:48] ability to write queries and the queries [63:50] let us you could think of from a sort of [63:52] database standpoint you can think of it [63:53] as an algebra standpoint allows us to [63:55] write down um you know things where we [63:59] want to solve for the values so we have [64:01] youal [64:03] expert and uh I'm going to evaluate some [64:09] you know something and get the value of [64:12] it back let me just make sure that [64:14] worked no oh Expo yeah you think i' [64:17] learned uh incorrect number of arguments [64:19] it probably takes the empty oh I bet [64:21] it's called a [64:22] Val yeah I think see if I've gotten a [64:25] Val yeah awesome okay so I I I've hidden [64:28] the environment in this version because [64:29] I'm just starting out in the empty [64:31] environment that's why we're not seeing [64:32] an environment we could type it in if we [64:34] wanted to okay so what's happening here [64:37] is we have an interpreter written in a [64:40] somewhat different style than what we [64:42] just wrote we have an evaluator you know [64:45] and we have an expression just like the [64:48] Expressions we were passing in to uh EV [64:50] Val expert and correspondingly we have [64:54] the value so this is a little bit [64:55] different than before in that um we [65:00] actually able to specify what the the [65:02] output should be now in this case we are [65:05] putting in a variable which means we [65:07] don't know we don't know what the value [65:09] should be in fact if you want to think [65:11] of from an algebra standpoint you know [65:13] I'll call it [65:14] X or uh maybe you know another way to [65:18] call it would be you know like question [65:21] mark or something right so this is this [65:23] is an unknown and we're trying to figure [65:26] out what the value of the unknown must [65:27] be and in this case the value of the [65:30] unknown is five you know the expression [65:31] five evaluates to five great so let's [65:35] try doing something a little more [65:37] interesting let's try having a Lambda [65:39] expression let's say about Lambda [65:42] XX okay oh that's a big thing you can [65:46] see that begins with closure so closure [65:49] is one way to represent a procedure so [65:52] some representation of a procedure I'm [65:54] not going to get into the details of it [65:56] um but I can [65:59] apply that uh function [66:06] oops give myself a little more space I [66:09] can apply the the uh that [66:12] procedure to uh five for example so the [66:16] identity function applied to [66:21] five and it gives me back five okay [66:24] great [66:26] now uh this so far is just treating it [66:29] like an interpreter uh just just like [66:31] what we had before and we have all sorts [66:33] of other things like we have the ability [66:36] to create lists um you know I could and [66:40] we have this cons operator I told you [66:42] about I think we have cons let's see [66:44] cons a onto the list B yep all right so [66:50] I can I can uh build up list structures [66:52] I can do all sorts of things but what I [66:54] can also do [66:56] is um play games where maybe I don't [67:00] know the input [67:02] expression and I know an output so maybe [67:06] the output is I want [67:09] milkshake right and now what I want is [67:12] an expression and scheme that when you [67:15] evaluate it produces the list I want [67:18] milkshake okay so let's try [67:21] it quote I want milkshake is one such [67:25] expression how about two oh here is a [67:30] procedure call a procedure that takes [67:33] any number of arguments whose body is [67:35] the expression quote I want milkshake [67:38] applied to no arguments and we can do [67:40] all sorts of games like that here's [67:42] another one like's I only do like 10 see [67:45] if there any good ones oh yeah here's a [67:47] call to car which gets the first element [67:49] in the list the car of a list containing [67:51] the list I want milkshakes and uh I can [67:54] do things like that all right that's fun [67:58] so uh I work in lab of Matt might at [68:01] Utah and he has this blog post called 99 [68:07] ways not to die [68:10] to to say I love you in racket so this [68:14] is like his Valentine's Day post right [68:16] it's like a slow Valentine's Day you [68:18] write this blog post and the um it's 99 [68:22] expressions in racket or scheme or [68:24] whatever whoops that uh actually [68:26] evaluate to the list I love you okay so [68:31] uh let's let's do that so let's go ahead [68:36] back and you know uh come up with a run [68:41] 99 and say I love [68:45] you and we get all these programs uh so [68:48] here's one it's a called a list with and [68:50] it has a function call inside of it and [68:52] stuff like that and every one of these I [68:53] can evaluate and scheme and it works [68:56] just fine all [68:58] right yeah uh okay so that's kind of fun [69:02] so let's try another one going back to [69:05] John McCarthy's [69:07] paper um he has this [69:11] little uh little note says a difficult [69:15] mathematical type exercise find a list e [69:18] that means a program expression e such [69:21] that the value of e is equal to e what [69:24] is that called aine so we want to find a [69:27] program that evaluates to itself so how [69:29] can we write such a [69:35] query uh yeah well let's let's out of [69:38] respect to John McCarthy call our [69:40] variable [69:41] e we want e to evaluate the E all right [69:46] oh that's a representation of a number [69:48] five evaluates the five that's true [69:50] let's [69:51] see hasht evaluates to hasht that's true [69:56] hasf of vales to hasf let's see if [69:59] there's anything let run for a second oh [70:02] what is this [70:04] thing oh all right forget those side [70:07] conditions here's a more interesting [70:09] looking expression and that evaluates to [70:12] itself oh okay so we can do things like [70:15] generate Quin what else can we do well h [70:20] Michael Balentine at this point said [70:22] well you [70:23] know what if you had a more interesting [70:27] scheme expression that you're evaluating [70:29] so let's try something a little [70:32] more uh interesting so let's try doing [70:34] something [70:40] like writing a program that concatenates [70:43] two [70:44] lists and you know don't worry about the [70:46] syntax here it's going to look you know [70:49] um if you don't know scheme uh you may [70:52] not read every single thing but we're [70:54] going to [70:57] pend okay and we Define a function [71:00] called a pen that takes to list L [71:02] ands and is kind of have an [71:06] if make this a little [71:10] smaller if L is [71:15] empty then we return s otherwise we are [71:19] going to [71:20] conson the car of L to a recursive call [71:24] to aend [71:26] with the rest of the list that's called [71:27] the cutter and S okay so let Rec lets me [71:32] Define a recursive function and now I'm [71:35] going to have a call to append I'm going [71:36] to say append [71:38] ABC to [71:41] De and let's see if that works and sure [71:44] enough it works so it gives me AB bcde e [71:46] in a [71:48] list because we can actually produce [71:51] more than one answer so let me show you [71:52] what that would look [71:53] like what we could could do [71:58] is well actually let me show you [72:00] something else first so what if we put [72:02] in the answer first we know the answer [72:04] should be AB bcde e okay so we put in [72:06] the answer and now I can put in that [72:10] variable thing uh the question mark [72:13] anywhere I want so I can put in the [72:15] question [72:17] mark uh inside this argument so I'm [72:21] asking what list when it appended to D [72:23] de gives me ABCDE e so what list should [72:25] that [72:27] be ABC and sure enough I get that okay I [72:31] could ask for uh two things maybe I X [72:35] and Y so I could say I want X and I want [72:41] y there are all sorts of games I could [72:43] show you with this but I'm I'm just [72:44] going to show you a couple um so now I [72:47] can I can have two two lists that [72:50] appended together give me ABCDE and you [72:52] can see the empty list applied to ABCDE [72:54] is one such pair of lists and I can [72:58] actually ask for all such pairs so I can [73:00] do a [73:03] Runar and now I get all the pairs back [73:07] and so if you've seen logic programming [73:09] if you've seen languages like prologue [73:10] or Min Canin um they let you do this [73:14] sort of query but notice we didn't write [73:17] a logic program we just took a scheme [73:19] program in our interpreter so we're [73:22] taking the the equal sign seriously [73:24] we're saying that [73:25] equality really does mean equal and [73:28] there's no direction to that equal sign [73:31] we should be able to solve for any side [73:34] okay so let's try one more [73:37] example we could do something [73:41] like have ABC and [73:45] de and now we say the answer should be [73:48] ABCDE and mini canron responds with some [73:52] gibberish that means that that's [73:54] consistent [73:56] um okay so the question is where else [73:59] could we put a logic variable [74:00] representing something [74:03] unknown in the code yes yeah right all [74:08] right so I don't know let me find a [74:11] Target uh how about this s let me put [74:14] something there so I think this is the [74:16] one with I [74:19] put run star is a bad idea run one is [74:23] good and sure enough it inferred the s [74:26] that I removed and things like that now [74:30] at this point we're actually doing [74:31] program synthesis so we have the ability [74:35] to specify information um in the form of [74:39] things like the expected input and the [74:43] corresponding expected output and use [74:45] the semantics of our interpreter that we [74:47] wrote as a relation and logic [74:49] programming system to do inference do a [74:53] search basically and and do constraint [74:55] solving to try to infer the missing [74:57] values and those missing values could be [74:59] the input arguments to the function the [75:01] output to the function even code or some [75:04] mixture thereof we can put variables [75:06] anywhere we want yeah could you put [75:09] it yeah let's try that it's a good [75:12] question so let's go back to what we [75:17] had like this is it yep let me put it [75:21] where the append was what do you think [75:23] I'll get back [75:26] hopefully oh whoops sorry I I have to [75:30] change this back question mark hopefully [75:33] a pen right yeah [75:38] start [75:40] what oh like call runs [75:44] oh hilarity will [75:47] ensue oh that's the answer you expected [75:51] right a procedure that ignores this [75:53] argument and returns list AB bcde [75:57] e mini Canon's like prove me [76:01] wrong I defy you to prove me [76:06] wrong so this is a fun sort of thing you [76:08] get into so let's let's try to like so [76:12] so mini kenin is like the genie right [76:14] the genie is like tell me your wish I'm [76:17] ready to [76:19] go so what we're going to do is we're [76:22] going to create a list of calls to to [76:26] append um sorry uh I don't remember if [76:29] we have list or not I think we have list [76:32] so we'll have more than one test that's [76:34] right so let's do two tests so one will [76:36] be like empty list to empty list and [76:39] then in the output we will have a list [76:42] of expected outputs so we have the empty [76:44] list and then uh the list ABC [76:49] oops try this see if this works yeah now [76:53] I came up with a pen so I was like all [76:55] right I got to work for it okay now what [76:58] we ask for [77:00] two see what happens I don't know I have [77:02] no idea oh okay it's what that is in [77:07] case you can't read that it's a a direct [77:09] application of a VAR tic function call [77:11] with zero arguments which Returns the [77:13] procedure of [77:14] pen it's like okay well you know I'm no [77:17] dummy I'll keep doing that so uh this [77:21] version is quite slow and if you want to [77:23] synthesize code for real it can take [77:25] quite a while um but we've been working [77:30] on a new tool see if I can zoom in oh it [77:34] works today whoa nice all right uh [77:38] there's a tool called bareman that I've [77:40] been developing with Greg Rosen blat and [77:43] and Michael Ballentine and other people [77:47] and this tool is basically just an [77:50] interface it's like a I I learned a [77:52] little bit of Swift Code and I wrote [77:53] this uh you can see it's beautiful and [77:56] you know basically this is just an [77:58] interface on what you saw with some [78:00] optimizations behind Okay to it runs [78:03] about 10 million times faster than the [78:06] naive version uh when you're doing [78:08] program synthesis that's important [78:10] because you're in an exponential space [78:12] so we are going to uh write a pend uh a [78:16] slightly different way so the code in [78:19] the upper left is our definition of a [78:21] pen you can see we left we left some [78:23] parts out right right so we left the [78:26] name of the function out that's this [78:28] comma a that's a mini kenin logic [78:30] variable it's a meta variable you can [78:31] think of it's a whole in the program we [78:32] don't know what that expression is we [78:34] don't know what the arguments are to [78:36] Lambda or how many there are or anything [78:37] like that and we don't know what the [78:39] body of the Lambda is okay so we're [78:41] going to let our tool come up with that [78:44] for us and what we're going to do is [78:45] just give some examples of a pen so I'm [78:47] going to pend two lists the empty list [78:50] so the empty list so give me be the [78:51] empty list and baran's going to think [78:54] about it and say I've got a solution for [78:57] you you want a function called a pen [79:00] it's like yes very well that function [79:02] can take any number of arguments well [79:05] strictly schemes a pen can and it's [79:08] going to return to the empty [79:11] list right a very exciting moment like [79:15] all right well that's okay I guess how [79:17] about we have a list [79:20] containing uh two lists list a and list [79:23] B and we want to get back [79:26] AB okay we'll add another [79:29] test [79:30] oh lucky [79:33] day you want a function called a pen [79:35] which takes two arguments and doesn't [79:36] matter what the names are and if the [79:40] second argument is empty we'll return [79:42] that why not because that's the first [79:44] test otherwise we'll return to list [79:47] AB all right well that's getting a [79:49] little annoying so let's introduce A New [79:51] Concept that of the gensim the generated [79:55] symbol we don't actually care what's in [79:57] that list we just want to make sure that [80:00] that's not going to appear in the output [80:02] program as long as it doesn't appear in [80:03] the output program we're happy so we're [80:05] going to change that oh now we do have [80:08] to do a little more work two arguments [80:11] null test on the second argument turn [80:14] the second argument if is null otherwise [80:16] we have to start doing some operations [80:18] cars and and conses and things like that [80:21] but we haven't there's no recursive call [80:23] it's not going to work so [80:25] let me try one [80:27] more list of length two you know you can [80:31] see where this game [80:32] goes [80:40] and let's think about [80:46] that it's thinking is like all right [80:49] this some this is some putting in some [80:51] work oh well that looked like a [80:54] recursive call that looks perilously [80:55] close to being correct huh it's a little [80:57] hard to read so I will give it I will [81:00] use the editor part to fill in some [81:04] concrete names and see what we can get [81:07] oh that is a [81:09] pend well that's nice it's example based [81:12] program synthesis furthermore I can do [81:15] some other things that are interesting [81:16] like I could add a few more [81:19] tests so I could say append of list a to [81:24] the empty list should be the empty list [81:26] and I could say [81:29] aend oh uh oh yeah yes yeah garbage in [81:34] garbage [81:35] out good [81:43] call anyone would like a job as a QA [81:46] tester for [81:48] bman okay so uh I wrote some more tests [81:51] and of course Parliament could already [81:52] synthesize it so it's not really [81:53] necessary but imagine for a second that [81:57] um maybe this program is too hard for [82:00] bareman to synthesize so instead of [82:02] having baramin synthesize the program [82:04] from the examples we're going to do test [82:06] driven development right I mean this is [82:09] real test driven [82:11] development um so we wrote our test [82:13] first and now we're going to write our [82:14] code right so I'm going to call it a pen [82:17] if I call it like you know you know [82:21] concat uh Min kenan's like or he like no [82:24] wrong computer says no fail all right so [82:28] let's call it a [82:29] pend and let's say we're going to take [82:32] two arguments L ands like before great [82:36] and we probably want an if and a null [82:39] check on L and you know we can start uh [82:44] kind of filling in the structure here [82:46] and uh bman can probably synthesize that [82:49] fine but let's pretend we're working on [82:51] something a little more complicated and [82:53] Parliament can't do it [82:55] um so now I'm typing and notice I've got [82:58] some holes in my program so I don't know [82:59] what those are and those are arbitrary [83:01] Expressions those could be you know [83:02] gigantic right I could have a scheme [83:03] compiler is a or something fter it is [83:07] solving it faster because I filled in [83:09] more uh the current version of barlin [83:11] sometimes you fill in more and it's like [83:13] really slow it goes get slower so we're [83:15] working on that but anyway um so let me [83:18] put in L that's one of my arguments so [83:20] I'm going to think hey L is probably the [83:22] right one oh bman like no computer says [83:26] no that particular test is incompatible [83:30] with the partially specified program [83:31] you've written so what we can do is [83:34] write our tests try to use it for [83:35] synthesis but if it's too slow for [83:37] synthesis we can just use this as an [83:39] editor and is constantly in the [83:41] background taking up all your cores and [83:43] heating your apartment and desperately [83:46] trying to prove and this is a proof [83:49] because mini Canon is a theorem prover [83:51] that the partially specified code you've [83:53] written is actually incompatible with [83:55] one of your tests it doesn't mean your [83:57] test is wrong maybe your code is wrong [83:59] maybe they're both wrong maybe the [84:00] semantics for The Interpreter underlying [84:02] bman is wrong but they're certainly [84:05] inconsistent right um and and I think [84:08] this this sort of technology is you know [84:12] um getting ready at this point to to be [84:15] practical for at least some use cases I [84:17] should also point out that there are [84:19] many other people working on program [84:20] synthesis and there's I think a [84:22] Renaissance in that area right now uh [84:25] but I do think that one thing that's [84:26] interesting is sort of the way we're [84:28] doing synthesis which is by taking that [84:32] interpreter that I showed you in the [84:34] beginning this beautiful piece of code [84:36] and looking at the original description [84:38] of it and those equal signs and taking [84:40] the equal signs seriously we're going [84:42] back and revisiting this artifact that [84:45] uh people had an understanding of and [84:48] we're trying to actually execute you [84:50] know another way of of looking at it [84:53] this relational sematic VI and people [84:55] people know relational semantics I mean [84:57] the way that the math was written down [84:59] is as relations um but the whole point [85:02] is we've designed this language mini [85:04] canron to let us encode these relations [85:07] in a nice way and then did a bunch of [85:09] optimization so when you write an [85:10] interpreter as a relation you can do [85:12] this fill-in-the blank game right and [85:15] there are all sorts of other examples I [85:16] could show you um with mini Canon there [85:19] some some really neat things if you're [85:20] interested in that you might check out [85:22] the closure con talk that I gave with [85:25] Greg rosenblat um at the con at last [85:28] year's con and we show off a whole bunch [85:30] of examples of this sort of thing and uh [85:32] you know we're we're trying to actively [85:34] improve it and explore other ways to to [85:36] do things and we can take things like a [85:38] a proof Checker and turn into a theor [85:40] improver by making it a relation all [85:42] sorts of fun games so if this appeals to [85:44] you uh let me know you might check out [85:46] the web page mini.org that has a [85:49] description of of uh a lot of the work [85:51] we've been doing and also I run Hangouts [85:53] on Saturdays and Sundays an intro [85:56] hangout series and advanced hangout [85:58] series um to talk about some of these [86:00] technology just send me an email drop my [86:02] my line hang out we'll get a milkshake [86:04] and we can talk about these things if [86:05] this thing you're interested in you want [86:06] to actually do some research work on it [86:08] hacking whatever you could probably [86:10] improve the user interface of parlament [86:12] if nothing else right so uh anyway uh [86:16] this is why I think The Interpreter that [86:19] interpreter written in lisp that's [86:21] higher order is so beautiful the such a [86:24] beautiful object that not only is it [86:27] very very dense and and an interesting [86:30] amalgam of very important ideas core [86:32] ideas but you can look at that object [86:34] from many different standpoints like I [86:36] said that infinite Tower of interpreters [86:39] that met it and or um any number of [86:42] other ways from program transformation [86:44] standpoint from a relational semantic [86:46] standpoint and so forth and each time [86:48] you look at that object that like feline [86:51] core program from a different standpoint [86:54] it gives you it yields some more secrets [86:58] right in some sense we know everything [86:59] about the interpreter but in some other [87:01] real sense like I would not have guessed [87:03] that you could do this sort of thing [87:05] just by taking that program and encoding [87:07] it in a logic programming language but [87:09] you can turns out you know I think [87:11] that's really amazing so um that's why I [87:15] think that's that's a really beautiful [87:16] artifact and and I hope everyone will [87:18] take the time to really study it and get [87:20] to know it and find their own ways of of [87:23] looking at and new ways to to consider [87:26] how that thing works [87:28] okay thank you thank you very much Round [87:32] of [87:36] Applause we have time for like two very [87:39] short questions and then we have to get [87:41] out of here so uh we have one right in [87:43] front here real [87:45] fast uh if you treat these tests as [87:47] constraints to the program that is [87:49] trying to guess can you apply like meta [87:51] constraints can you say like I want this [87:52] to be like a constant time algorithm or [87:55] I want it to be you know o of memory or [87:57] something like that uh that's a good [87:59] question so you know part of the issue [88:01] is how do you specify what it is you [88:04] want the program to do and so one way is [88:07] with these tests you could also use [88:09] something like types because we going [88:10] write type inferences in the same style [88:12] you can also write high level properties [88:14] and logic there a whole bunch of ways [88:16] you could do it and you could also say [88:17] something about the expected running [88:19] time or desired running time and so [88:20] forth we we're not at the point where we [88:23] can do things like like talk about the [88:24] desired run time although it is [88:26] something I'd like to be able to do [88:29] um and so so no you can't you can't do [88:32] that yet but one of the areas we're very [88:34] interested in is trying to do more [88:35] expressiveness the probably the most [88:37] recent thing that we've been playing [88:38] with that's interesting is just uh just [88:41] yesterday I [88:43] started um I basically wrote a version [88:46] of this technology where you can take [88:49] scheme programs look at common patterns [88:52] in scheme in terms very simple just [88:54] looking at what the parent is for an [88:56] expression like what you know if you see [88:59] a Define it turns out there's usually a [89:02] Lambda inside of it if you see a Lambda [89:04] there's usually an if or a cond inside [89:06] of it and looking for those sorts of [89:08] simple patterns and specializing the [89:10] relational interpreter um based on that [89:13] very very simple knowledge so instead of [89:15] just having the semantics the system [89:17] also would know a little bit about sort [89:19] of standard human style or things like [89:22] that uh and that alone uh looks like it [89:24] speeds up synthesis many orders of [89:26] magnitude and we're trying to figure out [89:27] can we apply that to sort of the [89:29] optimizations we've already made so I [89:31] think the the bottom line is like [89:33] there's a whole bunch of things that we [89:34] just haven't explored yet but I think [89:37] it's definitely possible and there are [89:38] other people in this program sensus [89:40] Community who particularly work on that [89:42] problem of trying to synthesize programs [89:45] that have you know different expected uh [89:49] you know running times and things like [89:50] that that's a very cool [89:52] problem more questions [89:55] a lot to take in I know [89:58] short um when you gave the example of um [90:02] coming up with the answer a pend yeah um [90:04] how does it how do you see the search [90:06] space like how did it know to find a [90:08] pend how did a pend get into the search [90:10] space well I mean it didn't find a pen [90:12] first right it cre a function that just [90:14] Returns the list um well because we have [90:17] an interpreter The Interpreter has a [90:20] notion of scoping just like we [90:22] implemented variable lookup we [90:24] implemented variable lookup in that [90:26] interpreter and the semantics of letre [90:28] The Binding structure of letre means [90:30] that within that call you know so the [90:33] call to aend was inside the definition [90:35] of aend so therefore in the environment [90:37] aend is there because we Define the [90:39] function and so one of the things it's [90:42] going to try to do The Interpreter is [90:43] going to try to do is look up the [90:45] variables that are currently Bound in [90:46] the environment and try all of those and [90:48] see if that will help lead to a solution [90:54] anyone [90:56] else [90:58] no all right thank you so much