Lambda Calculus評価

Question

これは簡単な質問であることは知っていますが、誰かが$（ lambda y。 lambda x。 lambda yy）（ lambda x。 lambday。y）$を$ lambda xに削減する方法を教えてもらえますか。 lambda y。 y $。

Answer 1

$（ lambda y。 lambda x。 lambda yy）（ lambda x。 lambday。y）$が$ lambda xに削減された理由。 lambda y。 y $、$ lambda xではありません。 lambda y。 lambda x。 lambda yy $は、$ lambda y。 lambda x。 lambda yy $のボディの$ y $が、最初ではなく3番目のラムダの議論を指します。

引数の名前を明確な名前に変更すると、$ lambda y。 lambda x。 lambda yy $は$ lambda y_1。 lambda x。 lambda y_2.y_2 $として記述されます。したがって、その関数を引数に適用する場合、それは$ lambda x。 lambda y_2.y_2 $の$ y_1 $のすべての発生を引数に置き換える必要があることを意味します。ただし、$ y_1 $はその式ではまったく表示されないため、引数は単に無視され、結果は$ lambda x。 lambda y_2.y_2 $です。