树演算

Hacker News Top 论文

摘要

本文提供了树演算的可视化介绍,这是理论计算机科学中的一个最小化、模块化、图灵完备且反射性的演算系统,强调其简单性和可教学性。

暂无内容
查看原文
查看缓存全文

缓存时间: 2026/09/13 02:35

# 树演算的可视化入门 来源:https://olydis.medium.com/a-visual-introduction-to-tree-calculus-2f4a34ceffc2 按回车键或点击查看完整图片 **三元演算**的归约规则(https://github.com/barry-jay-personal/blog/blob/main/2024-12-12-calculus-calculi.md)。黑色/实心节点是普通树节点,彩色三角形代表任意子树,“@”节点表示程序(左子节点)对其输入(右子节点)的**应用**。只要还有应用(application)存在,这些规则就适用。特别感谢 **Timur Latypoff**,他率先撰文可视化了这些规则(https://latypoff.com/tree-calculus-visualized/)! ## 为何有用?它如何工作? Johannes Bader(https://olydis.medium.com/?source=post_page---byline--2f4a34ceffc2-----------------------------------------) 树演算是一种**极简、模块化、图灵完备且具反射性**(https://treecalcul.us/)的演算。本文的目标是快速且直观地传达这一点。我强烈建议阅读 Barry 的著作(https://github.com/barry-jay-personal/tree-calculus/blob/master/tree_book.pdf)、博客(https://github.com/barry-jay-personal/blog)或近期论文(https://github.com/barry-jay-personal/typed_tree_calculus),以更深入和广泛地钻研! 我喜爱树演算的一点在于,虽然它在理论上推动了某些技术边界,令理论家的我无比兴奋,但同时**其规范极为紧凑且自包含**。这应使其非常易于教授。我在我妈妈身上测试了这个理论。在我不到一小时的解释和用纸笔草图说明后,她成功演算了“not false → true”和“not true → false”的归约过程,并理解了其中原理。哇!我妈妈非常聪明,但她从未听说过 λ-演算、组合逻辑(https://github.com/barry-jay-personal/blog/blob/main/2024-12-12-calculus-calculi.md)或项重写系统。而这至今仍然成立,因为树演算可以在没有任何希腊字母或括号的情况下进行解释和使用——因为它完全是关于树的。感谢妈妈自愿充当我的测试对象!❤ ## 领域与动机 在深入树演算如何工作之前,让我们先谈谈它是什么以及它能实现什么。现实世界是复杂的,因此计算机科学家和软件工程师都喜欢抽象地看待事物:从简单的假设或标准出发,层层构建复杂性。绝大多数人可以在顶层游刃有余,开发出强大的应用程序或推动科学进步。大致如此: 按回车键或点击查看完整图片 按回车键或点击查看完整图片 按回车键或点击查看完整图片 **左图**:真实的处理器形态各异,但像 x86 这样的标准化指令集有助于驯服这种混乱。高级语言/运行时可以针对这个标准,而无需过多担心底层硬件细节。**中图**:理论计算机科学中做了类似的事情。λ-演算相对简单但图灵完备,这使其成为进行科学研究的激动人心的起点!**右图**:树演算甚至更简单(https://treecalcul.us/#minimal),并且还具有反射性(https://treecalcul.us/#reflective),这使得它能够直接且安全(https://github.com/barry-jay-personal/blog/blob/main/2024-12-20-infinity.md)地完成令人兴奋的事情(https://github.com/barry-jay-personal/blog/blob/main/2024-12-14-logic.md)。 深入了解链接的资源,以确切了解如何实现以及原因,但要点是:树演算是**极简的**(https://treecalcul.us/#minimal)(注意漏斗那狭窄、几乎奇点般的“基底”),这使其易于推理,并且在任何环境中(https://treecalcul.us/implementation/)——包括纸笔——都易于运行。它比λ-演算具有更多原生能力(反射性(https://treecalcul.us/#reflective),递归程序的有限正规形(https://github.com/barry-jay-personal/blog/blob/main/2024-12-20-infinity.md)),这也缩短了核心演算与高级应用之间的距离。我们的网站(https://treecalcul.us/)托管了一些完全自包含的交互式演示,旨在传达这一点。 背景介绍够了,我们开始吧! ## 树演算 将程序和值视为**未标记的二叉树**。每个节点要么是**叶子**、**茎**(有一个子节点)或**叉**(有两个子节点)。 一个简单的程序示例(逻辑“非”,接受一个布尔参数并对其取反),有 4 个叶子、1 个茎和 3 个叉,总体大小为 8。程序作用于值。树演算提供了规则(https://treecalcul.us/specification/),描述一棵树(程序)如何作用于另一棵树(参数值)并归约为一棵新树(结果值)。程序也是一种值,因此程序也可以消费和生产程序。 ### 数据表示 如果所有值都是未标记的二叉树,我们需要决定表示它们的方式。树演算的归约规则规定了如何将特定程序表示为树,但对于表示“惰性”数据如数字、列表等,选择权在我们。例如: 按回车键或点击查看完整图片 如何表示布尔值或列表的建议,元素由各自的子树表示。可以想象将小自然数 k 表示为有 k 条边的链,或更大的整数表示为布尔值列表等。 ### 运行程序 > 在他的2021年著作(https://github.com/barry-jay-personal/tree-calculus/blob/master/tree_book.pdf)中,Barry 提出了一套仅三条规则来描述如何归约树。2024年,我提出了另一套规则,似乎让一些事情变得更直接(https://github.com/barry-jay-personal/blog/blob/main/2024-12-12-calculus-calculi.md)。本文和我们的网站(https://treecalcul.us/)使用的是后一套规则,我们称之为**三元演算**。 为了可视化描述树如何作用于树并归约为另一棵树的规则,将这个“作用于”步骤显式地表示为另一种节点类型是很方便的。让我们绘制一个“@”节点: 表达式“not true”(即“非”作用于“真”)的可归约表达式表示。请注意,程序/值仍然只有一种节点。上图是我们表示*表达式*的方式,这些表达式只有在归约*之后*才*成为*值。以下是归约规则: 按回车键或点击查看完整图片 **三元演算**的归约规则(https://github.com/barry-jay-personal/blog/blob/main/2024-12-12-calculus-calculi.md)。规则 0a-b 描述叶子和茎如何简单地“吸收”其参数。只有叉才是“做事”的程序。规则 1 和规则 2 对未经怀疑的读者来说似乎很任意,但其行为类似于组合逻辑中的 K 和 S 算子,这足以引导 λ-演算(https://en.wikipedia.org/wiki/Combinatory_logic#Completeness_of_the_S-K_basis)。规则 3a-c 根据参数树是叶子、茎还是叉来“分流”(triage)接下来发生的事情。这允许编写反射性程序。 请读者自行练习,运用这些规则用纸笔归约“not true”(见前图)和“not false”。 ### 构造程序 从这里开始,为越来越有用和复杂的程序想出相应的树是一个*工程*挑战。例如,这里有一个计算其参数大小(节点数)的程序。因此,当应用于之前的“非”程序时,它返回 8。当应用于自身时,它返回 180。 按回车键或点击查看完整图片 “size”程序。颜色仅用于提高可读性,没有语义含义。树的橙色部分提供了对参数树进行**递归**的能力(不动点)。绿色/蓝色/紫色子树是一个**分流**的三个子树(分别为 w/x/y,见规则 3a-c),根据遇到的节点类型进行适当的计算和递归。我们的网站(https://treecalcul.us/)托管了各种更高级的演示,例如程序优化器(https://treecalcul.us/live/?example=demo-fusion)或将树作为其他语言程序发出的程序(https://treecalcul.us/live/?example=demo-portability)。这些演示中构造的树可能太大而无法合理渲染——但它们都*只是树*!编译交互式游乐场(https://treecalcul.us/live/)所用伪语言的编译器本身就是一个大小约 200k 的树。 ### 结论 希望这篇可视化入门文章传达了关于树演算动机和工作原理的直觉。希望你足够兴奋去点击所有链接深入探索!让我们回顾一下本文第一句承诺的属性: - **极简**(https://treecalcul.us/#minimal):程序就是树,少数归约规则引导一切。 - **模块化**(https://treecalcul.us/#modular):程序可以组合成更大的程序。 - **图灵完备**(https://treecalcul.us/#turing-complete):树演算可以通过规则 1 和 2 来建模 λ-演算。 - **反射性**(https://treecalcul.us/#reflective):规则 3 允许对程序进行反思,例如优化它们(https://treecalcul.us/live/?example=demo-fusion)。 ### 附录:思考表达式和归约的另一种方式 本文将应用显式地可视化为“@”节点。我认为这强调了*可归约表达式*和*值*之间的区别。然而,也可以将可归约表达式表示和思考为*非二叉*树。从一个表示程序的二叉树开始,我们可以将参数作为新的、最右侧的子树附加到它上面。然后归约规则就是关于如何将非二叉树转换为二叉树: 按回车键或点击查看完整图片 表示规则 1、2 和 3a-c 的另一种方式。 请注意,规则 0a-b 变得不再必要,因为它们也只是将参数作为最右侧子树附加到程序上。注意:在规则 3c(以及类似的规则 3b 和规则 2)中,“y”是一个任意子树,但同时又具有子节点“u”和“v”,这意味什么?阅读方式是:“u”和“v”作为*额外*的最右侧子树附加到“y”上。这就是应用在此处的隐式编码方式,与显式的“@”节点相比。尽管不需要规则 0a-b,但我觉得这有点令人困惑。不过,如果你有不同的看法请告诉我! ### 附录:实现 如果你是一名软件工程师,你可能正在考虑用你最喜欢的编程语言或平台来实现它。如果你创建了什么很酷的东西,请毫不犹豫地联系我,我很乐意链接它! 查看网站获取参考实现(https://treecalcul.us/implementation/)。你会找到 OCaml 版本,它严格按照本文中可视化的方式实现了规则,函数 “apply” 扮演了 “@” 节点的角色。JavaScript 版本采用了上文介绍的另一种视角:归约规则实现为*修改*树直到它们变成二叉树。更多的修改而不是分配让垃圾收集器感到高兴。 ### 附录:表示法 图片对于大规模的树来说不易扩展。精确地讨论它们需要某种表示法甚至伪语言。Barry 恰当地选择了 △ 来表示树节点。之前的“非”程序将写成 “△ (△ (△ △) (△ △ △)) △”,应用写法就像在 λ-演算或组合逻辑中一样标准(左结合)。请查看 Barry 的近期论文(https://github.com/barry-jay-personal/typed_tree_calculus)或我们的网站(https://treecalcul.us/specification/)以获取使用此表示法的规范形式和归约规则。 出于可读性和简洁性,给树分配名称是有意义的。例如: `` // 如果我们定义 not = △ (△ (△ △) (△ △ △)) △ false = △ true = △ △ // 那么我们可以说 not true --> false not false --> true `` 网站上的交互式游乐场(https://treecalcul.us/live/)允许像这样为树分配名称,并为了方便提供了额外的语法糖。

相似文章

简化与重构初等微积分

Hacker News Top

该论文提出重构初等微积分,通过减少冗余和重新排序主题来简化教学,并借鉴计算机编程中代码重构的类比。

文档的核心演算

Lobsters Hottest

提出了一个正式的文档核心演算,可能探讨了文档处理的类型系统或语义。

直觉主义类型论 (2024)

Lobsters Hottest

本文概述了直觉主义类型论,这是一种基于依赖类型和λ演算的逻辑框架,源于Brouwer的直觉主义和Russell的类型论,并在证明助手和构造性数学中有应用。

Treap(笛卡尔树)

Hacker News Top

cp-algorithms 上关于 Treap(笛卡尔树)的算法文档,介绍了这种结合二叉搜索树与二叉堆特性的随机化数据结构及其插入、删除、合并等操作的复杂度与实现思路。

计算作为普遍且基本的概念

Hacker News Top

本文宣布了Tim Roughgarden开设的一门免费在线课程,涵盖计算机科学的基本概念,包括图灵机、停机问题、算法效率、NP完全性以及P与NP问题。