gistfile1.txt

「抽象除去」は、ラムダ抽象をSKIコンビネータによる表現にする手続きのことである。

式Eに対して抽象除去を行った結果を、T[E]と表記する。
抽象除去の規則は以下の通りである。
0.T[x] → x
1.T[f g] → T[f] T[g]
2.T[λx.x] → I
3.T[λx.f g] → S T[λx.f] T[λx.g]
4.T[λx.λy.z] → T[λx.T[λy.z]]
5.T[λx.e(それ以外)] → K e

チャーチ数3に相当するλf.λx.f (f (f x))は、以下のような手続きによって抽象除去される。

λf.λx.f (f (f x))
= T[λf.T[λx.f (f (f x))]] 規則4を適用
= T[λf.S T[λx.f] T[λx.f (f x)]] 規則3を適用
= T[λf.S (K f) T[λx.f (f x)]] 規則5を適用
= T[λf.S (K f) (S T[λx.f] T[λx.f x])] 規則3を適用
= T[λf.S (K f) (S (K f) T[λx.f x])] 規則5を適用
= T[λf.S (K f) (S (K f) (S T[λx.f] T[λx.x]))] 規則3を適用
= T[λf.S (K f) (S (K f) (S (K f) T[λx.x]))] 規則5を適用
= T[λf.S (K f) (S (K f) (S (K f) I))] 規則2を適用
= S T[λf.S (K f)] T[λf.S (K f) (S (K f) I)] 規則3を適用
= S (S T[λf.S] T[λf.K f]) T[λf.S (K f) (S (K f) I)] 規則3を適用
= S (S (K S) T[λf.K f]) T[λf.S (K f) (S (K f) I)] 規則5を適用
= S (S (K S) (S T[λf.K] T[λf.f])) T[λf.S (K f) (S (K f) I)] 規則3を適用
= S (S (K S) (S (K K) T[λf.f])) T[λf.S (K f) (S (K f) I)] 規則5を適用
= S (S (K S) (S (K K) I)) T[λf.S (K f) (S (K f) I)] 規則2を適用
= S (S (K S) (S (K K) I)) (S T[λf.S (K f)] T[λf.S (K f) I]) 規則3を適用
= S (S (K S) (S (K K) I)) (S (S T[λf.S] T[λf.K f]) T[λf.S (K f) I]) 規則3を適用
= S (S (K S) (S (K K) I)) (S (S (K S) T[λf.K f]) T[λf.S (K f) I]) 規則5を適用
= S (S (K S) (S (K K) I)) (S (S (K S) (S T[λf.K] T[λf.f])) T[λf.S (K f) I]) 規則3を適用
= S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) T[λf.f])) T[λf.S (K f) I]) 規則5を適用
= S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) T[λf.S (K f) I]) 規則2を適用
= S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (S T[λf.S (K f)] T[I])) 規則3を適用
= S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (S (S T[λf.S] T[λf.K f]) T[I])) 規則3を適用
= S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (S (S (K S) T[λf.K f]) T[I])) 規則5を適用
= S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (S (S (K S) (S T[λf.K] [λf.f])) T[I])) 規則3を適用
= S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) [λf.f])) T[I])) 規則5を適用
= S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) T[I])) 規則2を適用
= S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) I)) 規則0を適用