我不明白为什么在无类型 lambda 演算中允许以下 beta 减少:
(λx.x y) (u v) -> ((u v) y)
具体来说，我无法理解如何将两个参数
u 和 v 传递给 x 部分中的单个参数 λx.x。为了允许上述内容，我不应该使用柯里化并有两个参数吗？像这样-
(λx.(λy.(x y))) (u v)
最佳答案
您没有传递两个参数 u 和 v 。您正在传递 (u v) ，它是单个值或术语:应用于 u 的 v 值。
将此与普通算术进行比较:您可以将 sin 等函数应用于 sin(x + 1) 等复合术语，因为 x+1 表示单个值，即使它是函数 + 对两个参数 x 和 1 的应用。