η-簡約
出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2021/09/10 14:50 UTC 版)
T[ ]変換によって生成されたコンビネータはη-reductionによって小さくなりうる。 T[λx.(E x)] = T[E] (if x is not free in E) λx.(E x)はxを引数にとり、Eを適用する関数である。それは外延的にはE自身と同値である。それはつまりEをコンビネータの形にすれば十分である。この例は、この簡略化を根拠付ける。 T[λx.λy.(y x)] = ... = (S (K (S I)) T[λx.(K x)]) = (S (K (S I)) K) (by η-reduction) このコンビネータはより早く、長いものと同値である。 (S (K (S I)) K x y) = (K (S I) x (K x) y) = (S I (K x) y) = (I y (K x y)) = (y (K x y)) = (y x) 同様に、もとのT[ ]はλf.λx.(f x)を(S (S (K S) (S (K K) I)) (K I))に変換したが、η-簡約を用いればλf.λx.(f x)はIに変換される。
※この「η-簡約」の解説は、「コンビネータ論理」の解説の一部です。
「η-簡約」を含む「コンビネータ論理」の記事については、「コンビネータ論理」の概要を参照ください。
- η-簡約のページへのリンク