currying - λ演算 : passing two values to a single parameter without currying

Question

我不明白为什么在无类型的 lambda 演算中允许以下 beta 减少:

(λx.x y) (u v) -> ((u v) y)

具体来说，我无法理解如何传递两个参数 u和 v到单个参数 x在 λx.x部分。
为了允许上述情况，我不应该使用柯里化(Currying)并有两个参数吗？像这样-

(λx.(λy.(x y))) (u v)

Answer 1

specifically I cannot understand how one can pass two parameters u and v

您没有传递两个参数 u和 v .你正在通过 (u v) ，它是单个值或术语: u 的值申请 v .

将此与普通算术进行比较:您可以应用 sin 等函数像 sin(x + 1) 这样的复合词因为 x+1表示单个值，即使它是函数 + 的应用两个参数 x和 1 .