lambda-calculus - ラムダ計算の質問 - 具体的な

Question

私は次のものを持っています

(f.x.f(f x))(y.y+1) = x.(y.y+1)((y.y+1) x)
= x.(y.y+1)(x+1)
= x.x+1+1

なぜ最後の変換でいいのかわからないのですか？そうではないx.(y.y+1)(x+1)= y+1でしょうか？なぜ彼はそれを取り除くことができますかy

Answer 1

(y . y + 1)は引数に適用されるため、を与える(x + 1)ために置き換えられます。y((x + 1) + 1)

どうやって思いついたのかわかりませんx . (y . y + 1)(x + 1)= y + 1。y内部関数のスコープにのみ存在します。