λ演算中的Böhm定理

1. 基本概念回顾
   Böhm定理是λ演算中的一个重要结果，它涉及如何区分不同的λ项。首先需要理解：

• λ项由变量（x,y,...）、抽象（λx.M）和应用（M N）构成
• β归约规则：(λx.M)N → M[N/x]（替换x为N）
• 范式：无法再进行β归约的项
• 如果两个项可以通过α-转换（重命名绑定变量）相互转换，则称它们α-等价

2. 可分离性的定义
   在λ演算中，我们说两个项M和N是可分离的，如果存在一组参数P₁,...,Pₙ，使得：
   MP₁...Pₙ →* true 且 NP₁...Pₙ →* false
   其中true ≡ λx.λy.x，false ≡ λx.λy.y是Church布尔编码
   这意味着存在某个上下文能够区分这两个项的行为

3. Böhm树的概念
   Böhm树是λ项的某种"无限展开"，它捕捉了项的外部行为：

• 对于范式，Böhm树就是其语法树
• 对于非范式，我们逐步展开：BT(M) = λx₁...xₙ.y BT(M₁) ... BT(Mₖ)
  其中M →* λx₁...xₙ.y M₁ ... Mₖ
• Böhm树可能无限深，但每个节点只有有限多个子节点

4. Böhm定理的表述
   Böhm定理有两个主要版本：
   (1) 如果两个闭项M和N有不同的Böhm树，那么它们是可分离的
   (2) 如果两个不同的βη-范式不可通过α-转换相互转换，那么它们是可分离的

5. 定理的证明思路
   证明的关键构造分离器：

• 分析Böhm树中第一个不同的位置
• 构造特定的λ项来探测这个差异
• 利用Church数和布尔运算来设计测试
• 通过归纳构造确保分离器能区分两个项

6. 应用与意义
   Böhm定理在λ演算中有重要应用：

• 提供了判断λ项是否可转换的实用准则
• 是研究λ可定义性的基础工具
• 在函数式程序等价性验证中有应用
• 为研究λ演算的完全抽象语义提供基础

7. 推广与变体
   Böhm定理有多种推广：

• 适用于有类型λ演算的版本
• 考虑η-等价的扩展
• 在并发计算模型中的类似结果
• 与程序逻辑中的上下文等价概念的联系