Contents

λ to SKI, logarithmically

Please see my newer notes instead. This page is kept for historical reasons.





Oleg Kiselyov describes a linear-time and linear-space algorithm for converting lambda terms to combinators:

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

How about without memoization? Observe:

\[\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
print $ logBulk $ Bn 1234

Demo

jsEval "curl_module('../compiler/Charser.ob')"
import Charser
source = ws *> term [] <* eof where
  term bnds = lam bnds <|> app bnds
  lam bnds = do
    vs <- lam0 *> many v <* lam1
    t <- term $ reverse vs ++ bnds
    pure $ iterate Lam t !! length vs
    where lam0 = str "\\" <|> str "λ"
          lam1 = str "->" <|> str "."
  v   = some alphaNumChar <* ws
  app bnds = foldl1 App <$> some (ind bnds <$> v
    <|> str "(" *> term bnds <* str ")")
  ind bnds s = go bnds where
    go = \case
      [] -> error $ s ++ " is free"
      h:t | h == s    -> Zero
          | otherwise -> Succ $ go t
  str = (<* ws) . string
  ws = many $ oneOf " \n" *> pure () <|> string "--" *> many (noneOf "\n") *> pure ()

demo = parse source "" <$> jsEval "input.value;" >>= \case
  Left _ -> jsEval "lin.value = `parse error`; log.value = `parse error`;"
  Right deb -> do
    let v = snd $ ski deb
    jsEval $ "lin.value = `" ++ show v ++ "`;"
    jsEval $ "log.value = `" ++ show (logBulk v) ++ "`;"

jsEval [r|
  skiB.addEventListener("click", (ev) => { repl.run("chat", ["Main"], "demo"); });
|]
Contents
Ben Lynn blynn@cs.stanford.edu 💡