currying - lambda演算：将两个值传递给单个参数而不进行currying

Question

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

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

具体来说，我无法理解如何将两个参数传递给零件中u的v单个参数。为了允许上述情况，我不应该使用柯里化并有两个参数吗？像这样-xλx.x

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

Answer 1

具体来说，我无法理解如何传递两个参数 u 和 v

您没有传递两个参数u和v. 您正在传递(u v)，这是单个值或术语：u应用于的值v。

将此与普通算术进行比较：您可以将函数应用于sin复合术语，例如sin(x + 1)因为x+1表示单个值，即使它是将函数+应用于两个参数x和1。