如何用β归约证明λ演算中NOT TRUE等于FALSE？

基础定义 #

• FALSE = λxy.y
• TRUE = λxy.x
• NOT = λx.x FALSE TRUE

归约步骤 #

1. 先写出NOT TRUE的初始表达式：

   NOT TRUE = (λx.x FALSE TRUE) TRUE
   

2. 第一步β归约：将函项λx.x FALSE TRUE中的绑定变量x替换为参数TRUE，得到：

   TRUE FALSE TRUE
   

3. 展开TRUE的定义代入，表达式变为：

   (λxy.x) FALSE TRUE
   

4. 对(λxy.x) FALSE进行β归约：

   - 绑定变量：x
   

• 函项体：λy.x
• 代入参数：FALSE

  归约后得到：λy.FALSE

5. 将上述结果应用到第二个参数TRUE，表达式变为：

   (λy.FALSE) TRUE
   

6. 最后一步β归约：

   - 绑定变量：y
   

• 函项体：FALSE
• 代入参数：TRUE

  由于函项体FALSE中不包含绑定变量y，归约结果直接为：

  FALSE
  

综上，通过β归约可证NOT TRUE = FALSE

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