Lambda 演算 - 为什么不能在这里再做一次 beta 减少？

Question

有人告诉我这个词

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

已经是正常形式了——但我不明白为什么。不能在这种状态下进行另一次 beta-reduction 并将术语 (λy.z x) 中所有出现的 y 替换为 (λy.y z)，以便评估为：

(z (λy.z x) (λy.y z)) ==> (z z x)

Answer 1

应用程序通常被认为是左关联的。也就是说，

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

不是

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

是的

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

这需要 z 的值进行 beta-reduce。