Lambda 演算表达式简化

Question

我正在尝试学习和理解 lambda 演算减少的工作原理。我一直在减少一些表达，我遇到了这个：

(λ x . x (λ x . λ y . x))

我把它简化为：

(λ x . λ y . x)

但是，我不知道它是正常形式还是可以减少更多。

Answer 1

第一个表达式不能进一步简化，因为唯一应用于另一个术语的术语是一个绑定（因此是未定义的）变量。你的减少是无效的，因为x 可以是任何东西，因此我们不知道它会对(λ x . λ y . x) 做什么。