content: -- Show that `BLC` is compressible, establishing that for some k,
  -- BBU(ceil(113/114 n) + k) >= BB(n).
  --
  -- In order to do this, we exploit holes in the code left by
  -- applications of `id` (e.g. \x. id x) which are useless because
  -- there's a smaller, equivalent lambda term (e.g. \x. x).
  --
  -- The actual code will start with a 6 bit codon to create 64
  -- available prefixes to complete, followed by 113 bit blocks
  -- each encoding a 114 bit infix of the ordinary BLC encoding,
  -- finished off by another block of up to 114 bit in length.
  
  import qualified Data.Map as M
  import Control.Monad
  
  -- State machine abstracting from parsing BLC terms.
  -- The states are as follows:
  --
  -- H 0 -- final state
  -- H k -- we're between tokens, expecting `k` more terms ("holes").
  -- Z k -- H k followed by a 0 bit, so either an application or an abstraction
  -- V k -- H k followed by one or more 1 bits, so in the middle of a variable
  
  data S = H !Int | Z !Int | V !Int
      deriving (Eq, Ord, Show)
  
  step :: S -> [S]
  step (H 0) = []              -- final state
  step (H n) = [Z n, V n]      -- 0 bit or 1 = variable
  step (Z n) = [H n, H (n+1)]  -- 00 = abstraction or 01 = application
  step (V n) = [H (n-1), V n]  -- 1+0 = variable end; 1+ = continue variable
  
  -- Check that all terms fit into a prefix code... (plausible == repeat True)
  plausible :: [Bool]
  plausible = go 1 (M.singleton (H 1) 1)
    where
      -- `c` tracks the number of unused prefixes;
      -- `m` tracks the active states
  
      -- The analysis is similar to Kraft's inequality, but rather than
      -- computing various 2^-k, we multiply the number of available
      -- prefixes by 2 whenever we extend the prefixes.
      go c m
          = ((c == cost m) :) -- note: stronger than >=
          . go (2*(c - M.findWithDefault 0 (H 0) m))
          $ M.fromListWith (+) $ do
              (s, n) <- M.assocs m
              s <- step s
              pure (s, n)
  
      -- cost: each prefix is mapped directly so the cost is 1
      cost m = sum $ do
          (h, n) <- M.assocs m
          pure $ 1*n
  
  c0 :: Integer
  c0 = 64 -- 6 bits
  
  -- check whether we can compress prefixes of length 0,1,...
  -- if we start in state `s` with at least `c0` available prefixes,
  -- or `c0+1` prefixes if we are in a `V _` state
  compress :: S -> [Bool]
  compress s = go i (M.singleton s 1 : repeat M.empty)
    where
      i = case s of
          H _ -> c0
          Z _ -> c0
          V _ -> c0 + 1 -- includes extra prefix
  
      -- `c` tracks the number of unused prefixes;
      -- `m` tracks the active states
      go c ms@(m : _)
          = ((c >= cost m) :)
          . go (2*(c - M.findWithDefault 0 (H 0) m))
          . take 6
          . (: ms)
          $ M.fromListWith (+) $ do
              (s, n) <- M.assocs m
              s <- step s
              pure (s, n)
            ++ do
              -- we discard states corresponding to terms that contain
              -- an application of `id` (which takes 6 bits: 01 00 10)
              (H h, n) <- M.assocs (ms !! 5)
              guard $ h > 0
              pure (H h, -n)
  
      -- cost: We want to *compress*, so add a factor of 2 (one bit) to the cost
      cost m = sum $ do
          (h, n) <- M.assocs m
          let w = case h of
                  H _ -> 2*c0
                  Z _ -> 2*c0
                  V _ -> 2*(c0 + 1) -- include extra prefix
          pure $ w*n
  
  check :: Int -> Bool
  check n = and $ do
      let maxN = 1 + (n+1) `div` 2 -- 1 + maximum number of holes we can fill
      s <- H 0 : do
          i <- [maxN,maxN-1..1]
          [H i, Z i, V i]
      pure $ compress s !! n
  
  bound :: Int
  bound = head $ dropWhile (not . check) $ [1..]
  
  main :: IO ()
  main = print bound
  -- output: 114
  