Сел на выходных побаловаться с комбинаторной логикой, повыражать одни комбинаторы в базисе других. Быстро достался пользоваться бумажками и ручкой, написал такую штуку (наверняка велосипед):

module Cmb where

data Cmb = Cmb String   -- комбинатор
         | (:#) Cmb Cmb -- применение есть комбинатор (инфиксный конструктор)
  deriving Eq

instance Show Cmb where
  show (Cmb x)   = x
  show (ts :# t) = case t of _ :# _ -> show ts ++ "(" ++ show t ++ ")"
                             _      -> show ts ++ show t

-- лень писать instance Read Cmb, поэтому делаю инфиксный конструктор применения левоассоциативным,
-- чтобы записывать (SK)K==SKK как s:#k:#k (без лишних скобок)
infixl 5 :#

-- Основные комбинаторы
b = Cmb "B" -- композитор
w = Cmb "W" -- дубликатор
k = Cmb "K" -- канцелятор
i = Cmb "I" -- бездельник
s = Cmb "S" -- коннектор
c = Cmb "C" -- пермутатор

-- Неспецифицированные комбинаторы
x = Cmb "x"
y = Cmb "y"
z = Cmb "z"
t = Cmb "t"
u = Cmb "u"
v = Cmb "v"

-- Пошагово выводит в строку применение комбинаторов, до тех пор пока что-то меняется
modN  :: Cmb -> String
modN  cmb = let res = mod1 cmb 
             in if res == cmb then (show cmb) 
                             else ((show cmb) ++ " ~> " ++ modN res)


-- Применяет самый левый из годных к применению комбинаторов
mod1 :: Cmb -> Cmb
mod1 (Cmb c)  = (Cmb c)
mod1 ((Cmb c) :# t) 
  | c == "I"   = t                        -- применяем I
  | otherwise  = (Cmb c) :# mod1 t
mod1 ((Cmb c) :# t :# s)
  | c == "W"   = t :# s :# s              -- применяем W
  | c == "K"   = t                        -- применяем K
  | otherwise  = mod1' ((Cmb c) :# t) s
mod1 ((Cmb c) :#t :# s :# u)
  | c == "B"  = t :# (s :# u)             -- применяем B
  | c == "S"  = t :# u :# (s :# u)        -- применяем S
  | c == "C"  = t :# u :# s               -- применяем C
  | otherwise  = mod1' ((Cmb c) :# t :# s) u
mod1 (ts :#t :# s :# u) = mod1' (ts :#t :# s) u

-- Пробует организовать применение в первом, если не удаётся - пробует второй и склеивает результат в один
mod1' :: Cmb -> Cmb -> Cmb
mod1' c1 c2 = let res = mod1 c1
               in if res == c1 then c1 :# mod1 c2 
                               else res :# c2

-----------------------------------------------------------------------------

-- для тестирований 

-- B в базисе SK
b_sk = s:#(k:#s):#k   :#x:#y:#z
-- W в базисе SK
w_sk = s:#s:#(k:#(s:#k:#k))    :#x:#y:#z
-- C в базисе SK
c_sk = s:#((s:#(k:#s):#k):#(s:#(k:#s):#k):#s):#(k:#k)    :#x:#y:#z
-- I в базисе SK
i_sk = s:#k:#k   :#x
-- комбинатор неподвижной точки Y (Карри)
yCurry = s:#(b:#w:#b):#(b:#w:#b)   :#x
-- комбинатор неподвижной точки Y (Тромпа)
yTromp = s:#s:#k:#(s:#(k:#(s:#s:#(s:#(s:#s:#k)))):#k)   :#x
-- не имеет нормальной формы
noNF = s:#i:#i:#(s:#i:#i)   :#x:#y

Работает так (HUGS):

Cmb> modN (s:#(k:#s):#k :#x:#y:#z)
"S(KS)Kxyz ~> KSx(Kx)yz ~> S(Kx)yz ~> Kxz(yz) ~> x(yz)"
Cmb> modN yCurry
"S(BWB)(BWB)x ~> BWBx(BWBx) ~> W(Bx)(BWBx) ~> Bx(BWBx)(BWBx) ~> 
x(BWBx(BWBx)) ~> x(W(Bx)(BWBx)) ~> x(Bx(BWBx)(BWBx)) ~> 
x(x(BWBx(BWBx))) ~> x(x(W(Bx)(BWBx))) ~> x(x(Bx(BWBx)(BWBx))) ~> 
x(x(x(BWBx(BWBx)))) ~> {Interrupted!}"

И что-то не нравится мне, что в mod1 нужен такой перебор по арностям комбинаторв. Есть идеи, как это сделать поэлегантнее?