你如何减少这个 lambda 演算表达式？答案

【问题标题】：How do you reduce this lambda calculus expression?你如何减少这个 lambda 演算表达式？
【发布时间】：2022-01-13 18:59:00
【问题描述】：

如何减少这个 lambda 演算表达式？我正在尝试使用具有给定定义的 lambda 演算将 NOT FALSE 减少为 TRUE：

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

【问题讨论】：

标签： lambda computer-science lambda-calculus

【解决方案1】：

  NOT FALSE
= { expand definitions }
  (λb.λx.λy.b y x) (λx.λy.y)
= { beta-reduce, alpha-rename to avoid capture }
  λx.λy.(λa.λb.b) y x 
= { beta-reduce inside lambda, twice }
  λx.λy.x
= { definition of TRUE }
  TRUE

【讨论】：

【解决方案2】：

给定-

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

评估 -

NOT FALSE
---
 \
(λb.λx.λy.b y x) FALSE      β [b := FALSE]
 --       -      -----
          _______/
         /
(λx.λy.FALSE y x)

我们已经可以看到NOT 只是将参数反转为FALSE，这实际上与TRUE 相同。通过对 lambda 进行归约，我们可以证明它们的计算结果相同 -

(λx.λy.FALSE y x) 
       -----
         \
(λx.λy.(λx.λy.y) y x)       β [x := y]
        --       -
         
(λx.λy.(λy.y) x)            β [y := x]
        __    _
         ____/
        /
(λx.λy.x)                   = TRUE

【讨论】：