ラムダ計算：次のベータの減少は型なしラムダ計算に許可されている理由を私は理解できない

Question

をカリー化することなく、単一のパラメータに2つの値を渡す：

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

具体的に私は1つ、2つのパラメータuとvを渡すことができる方法を理解することはできませんλx.x部分の単一のパラメータxに変換します。 上記を許可するには、カリングを使用して2つのパラメータを使用しないでください。この—

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

Answer 1

のように、特に私は1つは、uとv

は、次の2つのパラメータuとvを渡していない2つのパラメータを渡すことができる方法を理解することはできません。単一の値または用語である(u v)を渡しています。uの値がvに適用されています。

は、通常の算術とこれを比較しますx+1は、2つの引数xと1に機能+のアプリケーションであっても、単一の値を示しているため、あなたはsin(x + 1)のような化合物の項に、このようなsinとしての機能を適用することができます。