SKIコンビネーター@Haskell

ラムダ式をSKIコンビネーター表現するコードが発掘された（昔のコードがたまたま見つかった）．

ちなみに，SKIBCで表現することも可能．

ラムダ式のベータ簡約は前につくった．

こんな感じ．

*SKI> b
\x->\y->\z->x (y z)
*SKI> trans opt b
S (K S) K
*SKI> trans bc b
B
*SKI> omega
\f->\x->f (x x) (\x->f (x x))
*SKI> trans opt omega
S (S (S (K S) K) (K (S I I))) (S (S (K S) K) (K (S I I)))
*SKI> trans bc omega
S (C B (S I I)) (C B (S I I))

もちろん，昔のコードなので，アルゴリズムとかは不明．間違っている可能性もなきにしもあらず．

module SKI where
type Ide = String
data Expr= Var Ide | Lam Ide Expr | App Expr Expr
instance Show Expr where
show (Var x) = x
show (Lam x e) = "" ++ x ++ "->" ++ show e
show (App e e') = show e ++" "++ show1 e'
where
show1 (Var x) = x
show1 (App e e') = "(" ++show e ++" "++ show1 e' ++ ")"
show1 e@(Lam _ _) = "(" ++ show e ++ ")"
-- S(Ke)(Ke') -> K(ee')
opt (Var"S" `App` (Var"K" `App` e)`App`(Var"K" `App` e'))=Var "K" `App` (e `App` e')
-- S(Ke)I -> e
opt (Var "S" `App` (Var "K" `App` e)`App` Var "I") = e
opt any = any
-- S(Ke)(Ke') -> K(ee')
bc (Var"S" `App` (Var"K" `App` e)`App`(Var"K" `App` e'))=Var "K" `App` (e `App` e')
-- S(Ke)I -> e
bc (Var "S" `App` (Var "K" `App` e) `App` Var "I") = e
-- S(Ke)e' -> B e e'
bc (Var "S" `App` (Var "K" `App` e) `App` e') = Var "B" `App` e `App` e'
-- Se(Ke') -> C e e'
bc (Var "S"`App` e `App` (Var "K" `App` e')) = Var "C" `App`  e `App` e'
bc any = any
trans' = trans id
--trans' = trans opt -- use additional rule: opt
--trans' = trans bc -- use additional rule: bc
--trans' = trans (bc.opt) -- use additional rule: opt, bc
trans f e@(Var _) = e
trans f (Lam x e) = extract f x e
trans f (App e e') = trans f e `App` (trans f e')
extract f x e@(Var y) | x==y = Var "I"
| otherwise = Var "K" `App` e
extract f x (Lam y e) = extract f x  $ extract f y e
extract f x (App e e') = f $  Var "S" `App` (extract f x e) `App` (extract f x e')
ap x y = App x y
x  = Var "x"
y  = Var "y"
z = Var "z"
s = Lam "x" $ Lam "y"  $ Lam "z" $ x `App` z `App` (y`App`z)
k = Lam "x" $ Lam "y" x
i = Var "I"
-- T=x.y. -> yx
t= Lam "x" $ Lam "y" $ y `App` x
-- B=x.y.z -> x(yz)
b = Lam "x" $ Lam "y" $ Lam "z"  $ x `App` (y`App` z)
-- C=x.y.z -> xzy
c = Lam "x" $ Lam "y" $ Lam "z" $ x `App` z `App` y
-- x.y. -> xy
e1=Lam "x" $ Lam "y" $ x `App` y
-- suc = x -> + 1 x
suc = Lam "x" $ Var"+" `App` Var "1"`App` x
-- f = x -> * (+ x 1)(- x 1)
f = Lam"x" $ Var"x" `App` (Var"+" `App` x `App` Var"1") `App` (Var"-" `App` x `App` Var"1")
-- Y = f -> (x -> f(xx))(x -> f(xx))
omega = Lam "f" $ fxx `App` fxx
where fxx=Lam "x" $ Var"f" `App` (x `App` x)
fact = Lam "f" $ Lam "n" $ Var"if" `App` g `App` Var"1" `App` h
where
n = Var "n"
f = Var "f"
g = Var"=" `App` n `App` Var "0"
h =Var"*" `App` n `App` f `App` (Var"-" `App` n `App` Var "1")
fact' = Lam "n" $ Var "if" `App` (Var"=" `App` n `App` Var "0") `App` Var "1" `App` (Var"*" `App` n `App` Var"fact" `App` (Var"-" `App` n `App` Var "1"))
where n = Var"n"

コンテンツ