抽象

a.hs

infixl 5 :*
data C = S | K | I | V Char | C :* C

elemC c (x :* y) = elemC c x || elemC c y
elemC c (V c') = c == c'
elemC _ _ = False

s (v, V c)
    | v == c = I
    | v /= c = K :* V c
s (v, e@(x :* y))
    | elemC v e = S :* s (v,x) :* s (v,y)
    | otherwise = K :* e
s (_, e) = K :* e

eta (v, V c)
    | v == c = I
    | v /= c = K :* V c
eta (v, e@(x :* y))
    | case y of V c -> v == c && not (elemC v x); _ -> False = x
    | elemC v e = S :* eta (v,x) :* eta (v,y)
    | otherwise = K :* e
eta (_, e) = K :* e

ex f = f ('x', f ('y', V 'x' :* V 'y' :* V 'y'))

main = do
    putStr "*: "
    print $ ex s
    putStr "eta: "
    print $ ex eta

instance Show C where
    show (x :* y@(_ :* _)) = show x ++ "(" ++ show y ++ ")"
    show (x :* y) = show x ++ show y
    show (V c) = [c]
    show S = "S"
    show K = "K"
    show I = "I"