lambda-calculus - Lambda 演算 - 为什么不能在这里进行另一个 beta 减少？

Question

有人告诉我这个词

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

已经是正常形式了——但我不明白为什么。不能在这种状态下进行另一个 beta 缩减，并将术语 (λ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。