Lambda 演算函数归约步骤答案

【问题标题】：Lambda Calculus Function Reduction stepsLambda 演算函数归约步骤
【发布时间】：2019-09-05 18:32:15
【问题描述】：

我正在学习 Lambda 微积分。有人可以帮忙减少吗？

(λa.((aλb.λc.c)λd.λe.d))(λf.λg.f)

实际结果是λb.λc.c。但我需要解决它的步骤

我已经完成了这些步骤，但我卡住了：

(λa.((aλb.λc.c)λd.λe.d))(λf.λg.f)
(λa.(aλb.λd.λe.d))(λf.λg.f)
(λf.λg.f)(λb.λd.λe.d)
(λg.λb.λd.λe.d)

我做错了吗？有什么我不知道的规则吗？

【问题讨论】：

你试过什么？你在哪里卡住了？向我们展示你自己的努力！
@lemontree 我已经添加了我已经完成的步骤
我迷路了；）刚刚修复了 assume 部分的错误。现在应该是正确的。哦，如果我的帖子回答了你的问题，请随时点赞；）
@Pater 对您的术语括号所做的更正 rsm 是错误的，您所说的带有括号的起始术语是正确的。（rsm 显示的归约数列也是正确的。）

标签： lambda-calculus

【解决方案1】：

视觉评估

仅使用文本构建步骤的可视化模型可能具有挑战性。正如其他答案所述，您的 () 以一种奇怪的方式使用。我希望这个答案有帮助-

fix parens:
(λa.((a λb.λc.c) λd.λe.d)) (λf.λg.f)

eval:
(λa.a (λb.λc.c) (λd.λe.d)) (λf.λg.f)
                           =========
    __________________________/
   /
(λa.a (λb.λc.c) (λd.λe.d))
    =    \         \
    |     \         \ 
    |      \         \
(λf.λg.f) (λb.λc.c) (λd.λe.d)
          =========    /
    _________/  ______/
   /           /
(λf.λg.f) (λd.λe.d)
       =     \__
       |        \
(λg.(λb.λc.c)) (λd.λe.d)
               =========
   _______________/
  /
(λg.λb.λc.c)
    =======
     /
    /
λb.λc.c

更高的直觉

顺便说一句，λb.λc.c 相当于 Church's FALSE、λa.λb.b。回到原来的程序，给定 Church 的布尔值 -

true := λa.λb.a
false := λa.λb.b

取原来的表达式-

(λa.a (λb.λc.c) (λd.λe.d)) (λf.λg.f)

使用true 和false 重写-

(λa.a false true) true

评估为 -

true false true

评估为 -

false

我们认为(λa.a false true) 为我们提供了布尔值的逆。我们可以将其命名为not -

true := λa.λb.a
false := λa.λb.b
not := λp.p false true

它是这样工作的 -

not true //=> false
not false //=> true

【讨论】：