【发布时间】：2015-01-12 18:14:05
【问题描述】：
我在接下来的两个 lambda 表达式的 b-reduction 方面遇到了一些问题，有人可以向我解释一下如何解决它们：
(λ f . λ x . f (f x))
(λ x . x (λ x . λ y . x))
【问题讨论】：
标签： lambda beta reduction calculus
【发布时间】：2015-01-12 18:14:05
【问题描述】：
因此，lambda 演算很像在编程中使用参数。 lambda 标记一个函数，名称标记参数的名称以及传递给它的内容。其余的只是代码的输入。
所以，使用你的第一个例子：
(λ f . λ x . f (f x))
(f x) 是输入
λ f 为函数，将 f 视为参数名
f 是它的应用方式。
目前，λ x 可以忽略。
所以第一个归约是取 (f x)，意识到它是 f 的一个参数，然后将它传递给 f 函数以在第二个 f 处应用。所以在第一步之后，它看起来像
(λ f . λ x . f (f x))
(f x) 传递给 f
((f x) . λ x . f )
(f x) 应用于函数
λ x 。 fx
还有一步要做，但我会让你去做。
此外，当没有括号时，将输入视为两个不同的值。这家伙解释它真的很有帮助。 https://www.youtube.com/watch?v=S_WzF6BHadc他确实有一个系列讲座。
【讨论】：
-
我不确定，但我认为最后一步是像参数一样应用 x，所以最终结果是 f。
-
下一个，我可以从 (λ x . x (λ x . λ y . x)) 减少到 (λ x . λ y . x) （我不知道它是否正确)，但我不知道最后一个表达式中的参数是什么。
-
是的，这就是我得到的。如果有人可以验证，那就太好了。
-
是的，那个很奇怪。我觉得我忘记了一条规则。