content: Look for small bases
   
  > import System.IO
  > import Data.List
  > import Data.Tuple
  > import qualified Data.Heap as Heap
  > import Data.Function
  > -- import Debug.Trace
  > import qualified Data.Set as Set
  > import System.Environment(getArgs)
  > import Text.ParserCombinators.ReadP
  > import qualified Data.Map.Strict as Map
  
  terms with de Bruijn indices (internal: starting at 0)
  
  > data L = Var !Int | App L L | Abs L deriving (Eq, Ord)
  
  size of the binary lambda calculus encoding
  
  > size :: L -> Int
  > size (Var i)   = i + 2
  > size (App a b) = 2 + size a + size b
  > size (Abs a)   = 2 + size a
  
  printing
  
  > newtype P = P L
  >     deriving (Eq, Ord)
  
  > instance Show P where
  >     showsPrec _ (P a) = prs a
  
  > prs :: L -> ShowS
  > prs = go 0 where
  >     go :: Int -> L -> ShowS
  >     go _ (Var i)   = shows (i+1)
  >     go p (App a b) = showParen (p > 1) $ go 1 a . (' ':) . go 2 b
  >     go p (Abs a)   = showParen (p > 0) $ ('λ':) . go 0 a
  
  > instance Show L where
  >   show a = prs a ""
  
  > instance Read L where
  >     readsPrec _ = readP_to_S pL
  
  A ReadP parser for $\lambda$-expressions.
  
  > pVar :: (Read v) => ReadP v
  > pVar = do skipSpaces; readS_to_P (readsPrec 9)
  
  > schar :: Char -> ReadP ()
  > schar c = do skipSpaces; _ <- char c; return ()
  
  > pL, pLAtom, pLVar, pLLam, pLApp :: ReadP L
  > pL = pLLam +++ pLApp
  >
  > pLVar = do
  >     v <- pVar
  >     return $ Var (v-1)
  >
  > pLLam = do
  >     schar 'λ'
  >     e <- pL
  >     return $ Abs e
  >
  > pLApp = do
  >     es <- many1 pLAtom
  >     return $ foldl1 App es
  >
  > pLAtom = pLVar +++ (do schar '('; e <- pL; schar ')'; return e)
  
  de-Bruijn substitution
  
  > tmMap :: (Int -> Int -> L) -> Int -> L -> L
  > tmMap onvar = walk where
  >     walk i (Var j)   = onvar i j
  >     walk i (Abs a)   = Abs (walk (i+1) a)
  >     walk i (App a b) = App (walk i a) (walk i b)
  
  > subst :: Int -> L -> Int -> L -> L
  > subst d c = tmMap (\i j -> if d+i == j then shift i 0 c else Var (if d+i < j then j-1 else j)) -- incorporate (shift (-1) 1 a) below
  
  > shift :: Int -> Int -> L -> L
  > shift d = tmMap (\i j -> Var (if i <= j then j+d else j))
  
  number of occurrences of a variable
  
  > noccur :: Int -> L -> Int
  > noccur i (Var j)   = if i == j then 1 else 0
  > noccur i (App a b) = noccur i a + noccur i b
  > noccur i (Abs a)   = noccur (i+1) a
  
  reduction to normal form with limited expansion
  need to account for expansion in function normalization because of
  SSK (λxλy.x y SSK) @ SSK
  SSK (λxλy.x y SSK) -=-=-=> λy. (λxλy.x y SSK) y (λxλy.x y SSK)
  (λxλy.x y SSK) SSK (λxλy.x y SSK) 
  SSK (λxλy.x y SSK) SSK
  
  > lnf :: Int -> L -> Maybe (Int, L)
  > lnf n (App f b) = {-- trace ("lnf " ++ show n ++ ": " ++ show f ++ " @ " ++ show b) $ --}
  >  case lnf n f of
  >   Nothing -> Nothing
  >   Just (n', Abs a) -> if n'' < 0 then Nothing else lnf n'' a' where
  >     a' = subst 0 b 0 a -- (shift (-1) 1 a) -- TAPL: shift (-1) 0 (subst 0 (shift 1 0 b) 0 a)
  >     n'' = case b of
  >       (Var _) -> n'
  >       _       -> n' - max 0 ((noccur 0 a) - 1)
  >   Just (n',a) -> fmap (fmap (App a)) (lnf n' b)
  > lnf n (Abs a) = fmap (fmap Abs) (lnf n a)
  > lnf n a = Just (n,a)
  
  Candidate single point bases
  
  > bases :: [String]
  > bases = [
  >  "λλλ3 1 (2 (λ2))", -- minimal             level 16 cumsize 2200336	2498293
  >  "λλλ2 1 (3 (λ2))", -- sizes below in ()   level 16 cumsize 1220869
  >  "λλλ2 (λ2) (3 1)", -- generates {T,K,B,W} level 16 cumsize  577496
  >  "λλλ3 (λ2) (2 1)", -- only finds F,I      level 16 cumsize   20312
  >  "λ1(λλλ2 1 (3 1))(λλ2)",      -- <S',K>   level 16 cumsize    5817
  >  "λ1(λλ2)(λλλ2 1 (3 1))(λλ2)", -- <K,S',K> level 16 cumsize    3261
  >  "λ1(λλ2)(λλλ3 1 (2 1))(λλ2)", -- <K,S,K>  level 16 cumsize    2253
  >  "λ1(λλλ3 1 (2 1))(λλ2)",      -- <S,K>    level 16 cumsize     244
  >  "λ1(λλλ3 1 (2 1))(λλλ3)",     -- Jeroen Fokker
  >  "λλλ3 (λλ2) 1 (2 1)",         -- Johannes Bader
  >  "λλλλ2 1 (4 (λ2))",           -- C.A. Meredith 1963!
  >  ""]
  
  > main :: IO ()
  > main = do
  >   hSetBuffering stdout LineBuffering
  >   args <- getArgs
  >   -- let basis = [("A", read (bases !! (if null args then 0 else read (head args))))]
  >   let basis = [("W",read"λλ2 1 1"),("K",read"λλ2"),("B",read"λλλ3(2 1)")]
  >   putStrLn $ "Using basis " ++ show basis
  >   let lvls = levels basis
  >   findtargets 1 lvls targets
  >   -- mapM_ (mapM_ print) lvls
  >   -- findtargets 1 (levels2 basis 8 4096) targets
  
  > levels :: [(String,L)] -> [[(String, L)]]
  > levels basis = l where l = basis : map (build id  l) [1..] 
  
  > levels2 :: [(String,L)] -> Int -> Int -> [[(String, L)]]
  > levels2 basis n len = l2 where
  >   l2 = take n (levels basis) ++ map (build filt l2) [n..]
  >   filt = take len -- . sortBy (compare `on` (size.snd)) 
  
  > findtargets :: Int -> [[(String,L)]] -> [(String,L)] -> IO ()
  > findtargets _ _ [] = return ()
  > findtargets _ [] _ = putStrLn "Unexpected end of levels"
  > findtargets n (lvl:lvls) tgts = do
  >   putStrLn $ "level " ++ show n ++ " size " ++ show (length lvl)
  >   go lvl [] where
  >     go [] found = findtargets (n+1) lvls (tgts \\ found)
  >     go ((as,comb):lvl') found = case Map.lookup comb tgtmap of
  >       Just name -> do
  >         putStrLn $ name ++ " = " ++ show comb ++ " = " ++ as
  >         go lvl' ((name,comb) : found)
  >       Nothing -> go lvl' found
  >     tgtmap = Map.fromList . map swap $ targets
  
  > targets :: [(String,L)]
  > targets = [
  >   ("Y0",read"λλ  2 1 2   "), -- A A(A(A A)A) of size 6 (14)
  >   ("W",read"λλ  2 1 1   "), -- A A(A(A(A A)A)) of size 7 (9)
  >   -- A M (W N) is 8 shorter than S M N and 7 shorter than S' N M
  >   ("D",read"λ   1   1   "), -- A(A(A A)A)(A(A A)A) of size 9 (9)
  >   ("I",read"λ       1   "), -- A(A(A(A A)A))(A(A A)A) of size 10 (14)
  >   ("K",read"λλ      2   "), -- A(A A)(A(A A)A A A A A) of size 11 (15)
  >   ("F",read"λλ      1   "), -- A A A(A(A A)(A A)(A A))A of size 11 (16)
  >   ("O",read"λλ  1  (2 1)"), -- A(A(A(A A) A)(A A) A(A A)) A if size 12
  >   ("T",read"λλ  1   2   "), -- A A(A(A A)A(A(A A)A)A)(A A) of size 13 (18 or 16 with eta)
  >   ("C",read"λλλ 3 1 2   "), -- A(A A A(A A A)(A A)(A A))A A of size 13 (15)
  >   ("B",read"λλλ 3  (2 1)"), -- A(A(A(A(A A)A))(A A)A)(A(A(A A))) of size 14 (?)
  >   ("K2",read"λλλ   3 1   "), -- A A(A(A A)(A A)(A A))(A(A A) A) A A (15)
  >   ("YT",read"λλ 1 (2 2 1)"), -- 
  >   ("S'",read"λλλ 2 1(3 1)"), -- A(A(A A)A)A A A A A A(A(A A)A) of size 15 (13)
  >   ("V'",read"λλλ 1 2 3   "), -- A A(A A)(A A)(A(A A(A A)) A A)(A A) of size 15
  >   ("T1",read"λλ  1 2 2   "), -- A(A(A(A(A(A A))))(A A) A)(A(A A)(A A)) of size 15
  >   ("W0",read"λλ  2 2 1   "), -- A A(A A)(A A(A A) A)(A A(A(A(A A) A))) of size 16
  >   ("S",read"λλλ 3 1(2 1)"), -- A(A(A A(A A(A A))(A(A(A A(A A))))))A A of size 16 (18)
  >   ("T0",read"λλ  1 1 2   "), -- A(A A)(A(A(A(A(A A) A) A(A A)) A) A A A) of size 17
  >   ("Y1",read"λλ2(1 2 1)  "), -- A(A(A A A)(A A)(A(A A) A) A)(A(A(A(A A)) A)) of size 18
  >   ("V",read"λλλ 1 3 2   "), -- ((((A(A(A(A(A A)))))((((A A)A)((A A)((A A)A)))A))(A A))A)A of size 19
  >   ("X",read"λλλ2(3 2 1)  "), -- ((((A(A(((A((A(AA))A))A)A)))(AA))(A((A(A((AA)A)))A)))A)A of size 20
  >   ("B3",read"λλλλ4 (3 2 1)"), -- (((A A)(A(((A A)A)(A(A A)))))A)(((A(A((A A)A)))A)(((A A)((A A)A))A)) of size 22
  > -- 0x79714758730 ````AA`A```AAA`A`AAA```A`A``AAAA```AA``AAAA
  > -- 0x79714758730 (((A A)(A(((A A)A)(A(A A)))))A)(((A(A((A A)A)))A)(((A A)((A A)A))A))
  >   ("CB3B",read"λλλ3 (λ3 (2 1))"), --  > 22 according to Hunt.hs
  >   ("Z",read"λλλ2 (3 1)"),
  >   ("WTF",read"λλλ2"),
  >   ("I2",read"λλ21")] -- 
  
  Btw, shortest diverging is Omega = (A A A) (A (A A A)) of size 7
  
  > build :: ([(String,L)] -> [(String,L)]) -> [[(String,L)]] -> Int -> [(String,L)]
  > build filt as n = filt apps where
  >   apps = nubOrd (Set.fromList . concatMap (map snd) . take n $ as) $
  >          [(fst x ++ paren (fst y), a) | i <- [0..n-1],
  >            x <- as!!(n-1-i), y <- as!!i,
  >            Just a <- [fmap snd . lnf lim $ App (snd x) (snd y)]]
  >   lim = if n < 16 then 42 else 14
  >   paren [a] = ' ':[a]
  >   paren  s  = "(" ++ s ++ ")"
  
  > nubOrd :: Ord a => Set.Set a -> [(b,a)] -> [(b,a)] 
  > nubOrd s (it@(_,x):xs)
  >    | x `Set.member` s = nubOrd s xs
  >    | otherwise        = it : nubOrd (Set.insert x s) xs
  > nubOrd  _ _           = []
  