SKS = I
なんで SKK = I なんだっけと考えていて、SKKx = Kx(Kx) = x で (Kx) は無視されるから、二つ目の K は他のコンビネータ(例えば S)でもいいよなと思ったわけです。
s x y z = x z (y z) k x y = x
というように、Haskellで定義して実行すると、上手くいきません。
S の型は (a->b->c)->(a->b)->a->c なので、第一引数は a->b->c という型でないと NG な訳です。
*Main> putStrLn $ s k k "w" w *Main> putStrLn $ s k s "w" <interactive>:1:17: Couldn't match expected type `t -> t1 -> t2' against inferred type `[Char]' In the third argument of `s', namely `"w"' In the second argument of `($)', namely `s k s "w"' In the expression: putStrLn $ s k s "w"
じゃあ、型がなければいいのかと考えて Grass でも実行。
wv : I wwWWWwwv : K wwwWWWwWWWwwWWwv : S WwwWwwWwwwwwwwwWWWWWWWw : out (SKS double)
C:\grass>runghc grass sks.txt w
今度はうまくいきました。
SKS = I と書ける「場合もある」と。
ってことは、型付きラムダ計算と型なしラムダ計算とでは、コンビネータの体系も変わってくるということなのかな。
その辺、整理した本とかないものかしら。