ラムダ計算を減らす方法

Question

私はラムダ計算を理解し、素晴らしいarticleを読もうとします。 8ページ、表現があるに

：

(λy.(x(λx.xy))) 

私は、

(λy.(x(λx.xy))) t 

をtと左の最も外側の(λy)を代用するつもりならば、結果は可能でしょうか？

x(λx.xy) 

Answer 1

私はyはすでに、すべてのyがtで置換される入力\ yにバインドされているので、構文

(\y -> x (\x-> x y)) 
(\y -> x (\x-> x y)) t 

x (\x -> x t) 

をのhaskellするためにそれを書き換える自由を取りました。

編集：無料のxを含む場所がtの場合は、以下のコメントに記載されているように、このスコープ内のバインドされたxの名前を「フレッシュ」な名前に変更することが重要です。これは現在意味のない名前です。我々は

let t = \t -> x t 

を言うならば、適切な置換はpigworkerで述べたように、いくつかのzは無料のxを隠し防ぐために、私たちのバウンドのxを交換するために、新鮮な識別子として新鮮さのために選択されている

x (\z -> z (\t -> x t)) 

ようになります。 t。