λ-演算中的Böhm树 基本定义与动机 Böhm树是λ-演算中描述项行为结构的工具，通过无限树展现项的“观察等价性”。其核心思想是：若两个λ项在任意上下文中的行为一致，则它们具有相同的Böhm树。具体定义如下： 对于一个λ项 M ，若 M 可被弱头归约（即不断对最外层的可归约式进行β归约）到形如 λx₁...xₙ.y M₁...Mₘ 的项（称为 头部正规形式 ），则其Böhm树根节点标记为 λx₁...xₙ.y ，子节点依次为 M₁,...,Mₘ 的Böhm树。 若 M 无弱头正规形式（如发散项 (λx.xx)(λx.xx) ），则其Böhm树为单节点 ⊥ ，表示不可观测。 构建方法与示例 通过迭代展开头部正规形式构建无限树： 例1：项 I = λx.x 的Böhm树为单层节点 λx.x 。 例2：项 Ω = (λx.xx)(λx.xx) 的Böhm树为 ⊥ 。 例3：项 Y = λf.(λx.f(xx))(λx.f(xx)) （不动点组合子）应用于 F 时，若 F 的Böhm树为 λx.x ，则 Y F 的树会无限展开为 λx.x 的重复结构。 与语义模型的关联 Böhm树是 可观察性等价 的完全特征：两个λ项上下文等价当且仅当它们的Böhm树相同。这一性质源于Böhm分离定理：若两个闭项具有不同的Böhm树，存在上下文能将它们分别归约为不同的范式（如 λxy.x 与 λxy.y ）。 扩展与应用场景 非严格语言 ：在惰性求值语言（如Haskell）中，Böhm树可描述程序的可能输出结构。 程序分析 ：通过有限逼近Böhm树（如截断到深度k），可设计静态分析工具推断程序行为。 并发系统 ：在进程演算中，类似的树结构被用于刻画进程的通信拓扑。 技术深化：Böhm变换 利用Böhm树可构造一种转换，将任意两个非β等价的闭项嵌入特定上下文，使其分别归约到 True 和 False 。此方法成为λ-演算可分离性的核心工具，并推动了后续关于不可扩展性的研究。