Hey There Buddo!

RSS: https://philipzucker.com/feed.xml
Philip Zucker 的博客，关于编程、数学、逻辑与物理的技术写作。

一个用 Lean 打印 Python 并查集的证明

Philip Zucker 写了一篇偏实验性的博客，核心是“证明即搜索过程 trace”这一原则。作者先把并查集（union find）的路径压缩解释为对等式传递性的应用，把 e-graph 的 memo 表解释为节点与 e-id 之间的等式，然后直接把执行过程中产生的步骤以 Lean 的 let 绑定流式写出，生成一个可被 Lean 检查的证词。 文中给出一版带证明输出的 Python 并查集（FatId 把证明 id 和普通 id 打包），用 lake env lean --stdin 做子进程验证，并展示了 union(a,b)、union(b,c) 后 a=c 的 Lean 证明。 作者还讨论了 rerooting、2-union find、Knut-Bendix、proof producing congruence closure（Nieuwenhuis & Oliveras）、Z3 的 proof cert 讨论、以及 Graham 在 Aufbau 里 “vibe code” 出的 proof-producing egraph。 属于偏研究/工程随笔风格，有真实代码、有观点、也留了不少开放问题，对关注 e-graph、定理证明、形式化验证的读者有较强吸引力。
评论点赞收藏4 天前

Lambda MicroEgg：一个支持良好作用域 α 等价绑定器的 e-graph

作者 Philip Zucker 发布了一个名为 Lambda MicroEgg 的项目，核心是一个支持 well-scoped alpha-aware binders 的 e-graph（等价图）。 e-graph 在程序分析与编译优化中常用于表达程序等价性，而"well-scoped alpha-aware binders"意味着它能在等价类上正确处理变量绑定与作用域，这在实现 lambda 演算、类型理论或程序变换时通常是难点。 文章本身很短，仅给出项目名与定位，缺乏使用示例、性能数据或与传统工具（如 Rust e-graphs 库）的对比，但方向明确、目标用户（编译器/程序分析研究者）清晰。
评论点赞收藏10 天前

Lean 元编程练习：执行即推导细化

作者记录自己在 Lean 元编程上的一个"顿悟时刻"：执行本质上是 elaboration（细化/推导）。这个视角把 Lean 的类型检查、宏展开、程序执行统一到一个心智模型里，对熟悉纯函数语言或形式验证的读者是有信息增量的认知重构。 个人一手经验、明确的"aha"叙事，容易引起做语言实现、形式化或 PL 圈读者的共鸣和讨论。
评论点赞收藏17 天前

用 TLA+ 规格验证 GDB 中断追踪

用 TLA+ 形式化规格验证 GDB 中断追踪结果。作者长期做汇编验证，将 GDB 捕获的中断 trace 与 TLA+ 模型对照，检查实际硬件行为是否符合形式化规范。
评论点赞收藏26 天前

半环上的Grobner基、Buchberger算法与七树同构

7棵树与1棵树之间存在同构关系，博客文章将其与Grobner基和半环算法相联系。 Philip Zucker引用了1994年经典论文《Seven Trees in One》，探讨Grobner基方法和Buchberger算法如何推广到半环结构，以及Knuth-Bendix完备化在此框架下的应用。
评论点赞收藏40 天前

用字典实现有限代数效应

作者用 Python 字典实现有限代数效应，展示如何用简单数据结构建模副作用和计算上下文。文章通过具体代码示例说明代数效应的组合与处理机制，适合对编程语言理论和实践感兴趣的读者。
评论点赞收藏63 天前

通过 Z3Py 让 TLA+ 与 x86 协同工作

作者尝试将 TLA+ 规范翻译为 Z3Py，以连接 Verus、CBMC 及汇编检查器，并探索交互式定理证明。这为形式化验证工程师提供了具体的工具链集成思路，特别是如何桥接高层规范与底层硬件验证。
评论点赞收藏75 天前

提升项：让作用域清晰的语法更“笨”一点

Philip Zucker 提出将“作用域提升（lifting）”概念从 egraph 简化到基础项（term）层面，通过引入 Thinning 结构让作用域成为项的内生属性而非隐式上下文。 文章展示了如何用 Python 实现带作用域信息的 Smart Constructor 和模式匹配，解决了变量捕获和替换时的作用域对齐问题。这种“去抽象化”的设计思路对构建形式化验证、编译器中间表示或符号计算引擎有直接参考价值，特别是处理高阶逻辑和依赖类型时的工程实践。
评论点赞收藏81 天前

数组理论（ToA）并查集：支持破坏性存储的新数据结构

Philip Zucker 提出了一种将“数组理论”（Theory of Arrays）与并查集（Union Find）结合的新数据结构。通过在半持久化数据结构的 rerooting 技术上引入非可逆的边缘注解，实现了对破坏性存储（destructive store）的支持。 文中提供了 Python 实现，展示了如何在并查集中维护映射关系，并讨论了其与 SMT 求解器中数组理论的关联及在扩展实数中的应用。这对构建高效的符号执行引擎或约束求解器有直接参考价值。
评论点赞收藏87 天前

TD4 4位DIY CPU组装与编程完全指南

作者购买并组装了TD4这款4位DIY CPU套件。文章详细记录了焊接过程中的坑（如二极管方向、USB接口焊接顺序），深入解析了CPU内部原理（地址解码、指令集、寄存器、进位触发器等）。 作者还分享了从简单LED闪烁到复杂上下计数程序的编写过程，并提供了自己写的Python汇编器和模拟器代码。最后提到了Nand2Tetris课程和Ben Eater项目作为延伸学习资源。 这是一篇非常适合计算机组成原理爱好者和DIY硬件玩家的实战指南。
评论点赞收藏103 天前

域、循环项与扁平方程系统

作者介绍了近期与Cheng Zhang等人关于将循环无限流式结构整合进e-graphs的讨论，并回顾了自己几年前在类似方向（coegraph）的工作。 涉及前沿的图论与代数系统交叉研究，具有较强的一手交流性质。
评论点赞收藏121 天前

提升 E-Graphs：一篇被 PLDI 2026 接收的论文

作者宣布其关于 Lifting E-Graphs 的论文被 PLDI 2026 的 EGRAPHS Workshop 接收。这是一个重要的学术认可信号，E-Graphs 是当前编译器和程序分析领域的热点话题，具有较高关注度。
评论点赞收藏128 天前

面向家庭的Python FrozenSet依赖类型理论

作者表达了将抽象事物“有限化”并放入日常框架（如Python的Frozenset）中处理依赖类型理论的尝试。这是一种将高阶类型理论与具体编程语言特性结合的个人实验性观点。
评论点赞收藏143 天前

使用 Dump Calculus 进行函数的提升与降低

作者探讨如何构建无名 De Bruijn e-graph，并由此引出用于函数提升和降低的组合子设计。这是一篇涉及底层编译器理论、图重写系统和函数式编程组合子的深度技术思考，适合对形式化方法和 e-graphs 感兴趣的工程师。
评论点赞收藏152 天前

为 Alpha 等价性简化/提升 E-图：第一阶段检查点

作者正在构建支持 Alpha 等价性的 e-graph（E-图）。在实现过程中，发现原本以为复杂度会失控，但随着理解加深，代码反而变得更简洁。 本文是该项目的阶段性检查点记录，分享了从复杂到简化的认知过程。
评论点赞收藏165 天前

带 Thinnings 的 Alpha 等价哈希共享

探讨在 egraph 技术中引入 thinnings 以实现 Alpha 等价哈希共享的技术步骤。这是编译器优化和符号计算领域的一个具体算法改进点。
评论点赞收藏188 天前

Monus、Factor与稀疏并查集发现

作者分享了一种思考广义e-graphs或模理论的“食谱”，核心思路是将常规的并查集（Union Find）替换为某种广义的并查集概念。这是关于底层数据结构与等价关系建模的工程/理论探索。
评论点赞收藏200 天前

Thinnings：子列表见证与 de Bruijn 索引移位聚类

作者受 Mastodon 上 Conor McBride 关于 Thinnings 的讨论启发，认为这是首次见到去除了复杂理论包装的直观解释。这一概念帮助作者理清了思路，并激发了关于 Lambda Egraphs 和广义并查集的大量新想法，计划后续深入展开。
评论点赞收藏206 天前

把 SMTLIB 当作编译器中间表示(IR)：SSA 即函数式编程的工程实践

作者提出利用 Z3 SMT 求解器的 AST 直接作为编译器中间表示(IR)。核心观点是 SSA 形式与函数式编程高度同构，通过将控制流图(CFG)的每个块映射为递归定义的函数，并利用 SMT 的 substitute_funs 进行展开和简化，从而在逻辑层面实现编译优化和验证。 文章展示了从 Python 代码到 SMT 定义再到类汇编 IR 打印的完整转换过程，并探讨了将其应用于 QBE 解析和二进制分析的可能性。这是一种利用定理证明器特性来简化编译器前端设计的工程实践。
评论点赞收藏232 天前

登录芦苇

登录后关注作者、收藏内容和参与讨论。

热门话题

人工智能12,865 人关注AI 会怎样改变日常工作？产品思考8,243 人关注怎样判断一个产品值得长期做？独立开发5,917 人关注一个人如何持续完成作品？
关于芦苇 · 联系我们 · © 2026 芦苇