ラムダ抽象から同値なcombinatorial termへの変換

ウィキペディア小見出し辞書

ラムダ抽象から同値なcombinatorial termへの変換

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/09/10 14:50 UTC 版)

「コンビネータ論理」の記事における「ラムダ抽象から同値なcombinatorial termへの変換」の解説

たとえば、λx.λy.(y x)をコンビネータにしてみよう。 T[λx.λy.(y x)]= T[λx.T[λy.(y x)]] (by 5) = T[λx.(S T[λy.y] T[λy.x])] (by 6) = T[λx.(S I T[λy.x])] (by 4) = T[λx.(S I (K x))] (by 3 and 1) = (S T[λx.(S I)] T[λx.(K x)]) (by 6) = (S (K (S I)) T[λx.(K x)]) (by 3) = (S (K (S I)) (S T[λx.K] T[λx.x])) (by 6) = (S (K (S I)) (S (K K) T[λx.x])) (by 3) = (S (K (S I)) (S (K K) I)) (by 4) 任意の二つの項xとyをこのコンビネータに合成すると、以下のように簡約される。 (S (K (S I)) (S (K K) I) x y)= (K (S I) x (S (K K) I x) y) = (S I (S (K K) I x) y) = (I y (S (K K) I x y)) = (y (S (K K) I x y)) = (y (K K x (I x) y)) = (y (K (I x) y)) = (y (I x)) = (y x) (S (K (S I)) (S (K K) I))という表現は、ラムダ項としての表現λx.λy.(y x)よりもはるかに長い。これは一般的なことである。普通、T[ ]はラムダ項をΘ(n2)に展開する。