纯Lambda演算中重定义cond后的布尔值编码是否有效？

要搞清楚这个问题，得先抓住Lambda演算布尔值编码的核心：true的作用是选中第一个参数，false的作用是选中第二个参数，而cond的本质就是让布尔值完成这个选择动作。我们直接通过推导验证新cond的行为：

1. 验证cond true x y的执行逻辑：

   cond true x y = (λx.x) true x y
   -- 恒等函数直接返回传入的第一个参数true
   → true x y
   -- 结合true的定义λx.λy.x，应用x和y后返回x
   → x
   

   这和原cond的行为完全一致：原cond true x y = (λb.λx.λy.b x y) true x y → true x y → x。

2. 验证cond false x y的执行逻辑：

   cond false x y = (λx.x) false x y
   -- 恒等函数直接返回传入的第一个参数false
   → false x y
   -- 结合false的定义λx.λy.y，应用后返回y
   → y
   

   这也和原cond的行为完全匹配：原cond false x y → false x y → y。

说白了，原来的cond是给布尔值套了一层“调用包装”，现在把cond改成恒等函数，只是去掉了这层多余的包装——因为布尔值本身就是一个天然的选择函数，直接让它接收两个分支参数，就能完成原本cond要做的选择工作。只要true和false的定义不变，它们的核心功能就没被破坏，整个布尔值编码依然有效。

内容的提问来源于stack exchange，提问作者Student