# λ to SKI, logarithmically

{-# LANGUAGE CPP #-}
#ifdef __HASTE__
import Haste.DOM
import Haste.Events
#endif
import Data.List
import Text.Parsec

data Deb = Zero | Succ Deb | Lam Deb | App Deb Deb deriving Show
infixl 5 :#
data Com = Com :# Com | S | I | C | K | B | Sn Int | Bn Int | Cn Int
ski :: Deb -> (Int, Com)
ski deb = case deb of
Zero                           -> (1,       I)
Succ d    | x@(n, _) <- ski d  -> (n + 1,   f (0, K) x)
App d1 d2 | x@(a, _) <- ski d1
, y@(b, _) <- ski d2 -> (max a b, f x y)
Lam d | (n, e) <- ski d -> case n of
0 -> (0,       K :# e)
_ -> (n - 1,   e)
where
f (a, x) (b, y) = case (a, b) of
(0, 0)             ->         x :# y
(0, n)             -> Bn n :# x :# y
(n, 0)             -> Cn n :# x :# y
(n, m) | n == m    -> Sn n :# x :# y
| n < m     ->                Bn (m - n) :# (Sn n :# x) :# y
| otherwise -> Cn (n - m) :# (Bn (n - m) :#  Sn m :# x) :# y

It relies on memoizing the bulk variants of the B, C, and S combinators:

\begin{align} B_n f g x_n ... x_1&= f &(g x_n ... x_1) \\ C_n f g x_n ... x_1&= (f x_n ... x_1)& g \\ S_n f g x_n ... x_1&= (f x_n ... x_1)&(g x_n ... x_1) \\ \end{align}

In particular, $$B_1, C_1, S_1$$ are the standard $$B, C, S$$ combinators. Linear complexity is implied by:

linBulk :: Com -> Com
linBulk b = case b of
Bn n   -> iterate ((B:#        B):#) B !! (n - 1)
Cn n   -> iterate ((B:#(B:#C):#B):#) C !! (n - 1)
Sn n   -> iterate ((B:#(B:#S):#B):#) S !! (n - 1)
x :# y -> linBulk x :# linBulk y
_      -> b

## Bulk discount

\begin{align} B_{m+n} f &= B_m (B_n f) \\ C'_{m+n} f &= C'_m (C'_n f) \\ S'_{m+n} f &= S'_m (S'_n f) \\ \end{align}

where

\begin{align} C'_n c f g x_n ... x_1 &= c (f x_n ... x_1)&g \\ S'_n c f g x_n ... x_1 &= c (f x_n ... x_1)&(g x_n ... x_1) \\ \end{align}

Hence we can build up the bulk combinators in a manner analogous to repeated squaring when exponentiating, resulting in a logarithmic factor in lieu of a linear one. In short: binary, not unary.

Define the following combinators:

\begin{align} b_0 c x y &= c (B x x) y \\ b_1 c x y &= c (B x x) (B x y) \\ X x y &= y I \\ \end{align}

To compute $$S_{50}$$ for example, write 50 in binary: 11010. Then chain together $$b_0$$ or $$b_1$$ depending on the bits:

$S_{50} = b_1(b_1(b_0(b_1(b_0 X)))) S'_1 I$

Similarly for the other bulk combinators.

logBulk :: Com -> Com
logBulk b = case b of
-- C' = \cfgx.c(fx) g   = B(BC)B
-- S' = \cfgx.c fx (gx) = B(BS)B
Bn n   -> go n (K:#I)         :# B              :# I
Cn n   -> go n (K:#(C:#I:#I)) :# (B:#(B:#C):#B) :# I
Sn n   -> go n (K:#(C:#I:#I)) :# (B:#(B:#S):#B) :# I
x :# y -> logBulk x :# logBulk y
_      -> b
where
go n base = foldr (:#) base $([b0, b1]!!) <$> bits [] n
bits acc 0 = reverse acc
bits acc n | (q, r) <- divMod n 2 = bits (r:acc) q
b0 = C:#B:#(S:#B:#I)
b1 = C:#(B:#S:#(B:#(B:#B):#(C:#B:#(S:#B:#I)))):#B

Therefore, if memoization is forbidden, we can easily transform a lambda term of length N to a combinatory logic term of length O(N log N).

## Show Me

instance Show Com where
show S = "S"
show I = "I"
show C = "C"
show K = "K"
show B = "B"
show (l :# r) = (show l ++) $case r of _ :# _ -> "(" ++ show r ++ ")" _ -> show r show (Bn n) = "B_" ++ show n show (Cn n) = "C_" ++ show n show (Sn n) = "S_" ++ show n For example: λ> print$ logBulk $Sn 1234 CB(SBI)(C(BS(B(BB)(CB(SBI))))B(CB(SBI)(CB(SBI)(C(BS(B(BB)(CB(SBI))))B(CB(SBI)(C(BS(B(BB)(CB(SBI))))B(C(BS(B(BB)(CB(SBI))))B(CB(SBI)(CB(SBI)(C(BS(B(BB)(CB(SBI))))B(K(CII))))))))))))(B(BS)B)I λ> print$ logBulk $Bn 1234 CB(SBI)(C(BS(B(BB)(CB(SBI))))B(CB(SBI)(CB(SBI)(C(BS(B(BB)(CB(SBI))))B(CB(SBI)(C(BS(B(BB)(CB(SBI))))B(C(BS(B(BB)(CB(SBI))))B(CB(SBI)(CB(SBI)(C(BS(B(BB)(CB(SBI))))B(KI)))))))))))BI ## Demo source :: Parsec String [String] Deb source = term where term = lam <|> app lam = do orig <- getState vs <- between lam0 lam1 (many1 v) modifyState (reverse vs ++) t <- term putState orig pure$ iterate Lam t !! length vs
where lam0 = str "\\" <|> str "\0955"
lam1 = str "->" <|> str "."
v   = many1 alphaNum <* ws
app = foldl1' App <$> many1 ((ind =<< v) <|> between (str "(") (str ")") term) ind s = (iterate Succ Zero !!) . maybe (error$ s ++ " is free") id . elemIndex s <$> getState str = (>> ws) . string ws = many (oneOf " \t") >> optional (try$ string "--" >> many (noneOf "\n"))

#ifdef __HASTE__
main = withElems ["input", "lin", "log", "skiB"] $\[iEl, linEl, logEl, skiB] -> do skiB onEvent Click$ const $do s <- getProp iEl "value" let v = snd . ski <$> runParser source [] "" s
setProp linEl "value" $either (("error" ++) . show) show v setProp logEl "value"$ either (("error" ++) . show) show $logBulk <$> v
#else
amain = print $logBulk$ Sn 1234
main = do
let
s = "\\l.l(\\h t x.t(\\c n.c h(x c n)))(\\a.a)(\\a b.b)"
Right out = logBulk <$> snd . ski <$> runParser source [] "" s
print out
#endif

Ben Lynn blynn@cs.stanford.edu 💡