lambda-calculus - lambda演算，扩展和压缩形式有不同的beta-reductions？

Question

给定

S=\x.\y.\z.x z (y z)

和

K=\x.\y.x

如果我从 (SKK) 形式或等效的扩展形式开始，我无法理解同一表达式 (SKK) 的两个 beta 等效形式如何在无类型 lambda 演算中产生不同的结果：

(S K K) = ((S K) K) -> ((\y.(\z.((K z) (y z)))) K) -> (\z.((K z) (K z))) ->
(\z.((\y.z) (K z))) -> (\z.z) -> 4 reductions!

(S K K) = \x.\y.\z.x z (y z) \x.\y.x \x.\y.x -> 0 reductions!

似乎压缩和扩展形式有不同的括号，实际上第一个括号为：

(S K K) = ((S K) K)

而第二个为：

\x.\y.\z.x z (y z) \x.\y.x \x.\y.x =
(\x.(\y.(\z.(((x z) (y z)) (\x.(\y.(x (\x.(\y.x)))))))))

有人对此有任何见解吗？？？谢谢

Answer 1

在 Wikipedia 上查看lambda 演算的正式定义。一个抽象和一个应用程序总是有一组括号。这意味着 S 和 K 的更正确定义是：

S = (\x.\y.\z.x z (y z))

和

K = (\x.\y.x)

将这些替换(S K K)为正确的结果。

Answer 2

在(S K K)中，一些括号是隐含的。这种形式是((S K) K)因为函数应用程序始终是二进制的并且被认为是左关联的的缩写。