7

型指定されていないラムダ計算で次のベータ削減が許可される理由がわかりません。

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

u具体的には、2 つのパラメーターをパーツ内のv1つのパラメーターに渡す方法を理解できません。上記を許可するには、カリー化を使用して2つのパラメーターを使用する必要はありませんか? このような-xλx.x

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

1 に答える 1

11

具体的には、u と v の 2 つのパラメーターを渡す方法がわかりません

u2 つのパラメーターとを渡していませんv。(u v)単一の値、または用語であるを渡しています:u適用されるの値ですv。

これを通常の算術演算と比較してください。2 つの引数およびへの関数の適用であっても、 は単一の値を表すので、 のsinような複合項に などの関数を適用できます。sin(x + 1)x+1+x1

于 2011-12-07T14:20:34.503 に答える