演算：使兩個值到一個單一的參數而不討好

Question

我不理解爲什麼以下的β還原是在無類型演算允許：

(λ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)，這是一個單一值或術語：v的值爲u。

比較這與普通的算術：您可以將一個函數如sin像sin(x + 1)一個複合詞，因爲x+1表示單個值，即使它是功能+到兩個參數x和1的應用。