【发布时间】：2020-04-18 13:49:28
【问题描述】：
(λw.w)(λu.λv.u)(λu.λv.v)(λu.λv.u)
谁能给我这个示例的逐步 Beta 缩减？ 我真的很困惑
【问题讨论】：
-
你坚持哪一部分？你一个人能走多远？你知道如何减少任何东西吗？你知道什么是 alpha 转换吗？
标签： lambda-calculus
【发布时间】：2020-04-18 13:49:28
【问题描述】：
(λw. w) (λu. λv. u) (λu. λv. v) (λu. λv. u)
将 (λw. w) 应用于 (λu. λv. u)。由于这是恒等函数，因此没有任何变化。
(λu. λv. u) (λu. λv. v) (λu. λv. u)
将 (λu. λv. u) 应用于 (λu. λv. v)。它在表达式中替换了 u。由于我们现在可能对第一个表达式中的多个 v 感到困惑，我们可以将内部表达式中的 v 重命名为另一个变量 x。
(λv. (λu. λx. x)) (λu. λv. u)
将 (λv. (λu. λx. x)) 应用于 (λu. λv. u)。由于 v 没有出现在 lambda 的主体中，因此该参数被有效地丢弃。
(λu. λx. x)
我们现在可以（可选地）再次 alpha 重命名以恢复原始变量名称。
(λu. λv. v)
【讨论】：