BitChanger Busy beaver/Proof
Jump to navigation
Jump to search
Proof sketch (mostly computational)
For context, see BitChanger Busy beaver and BitChanger.
- enumerate programs of the given size
- perform minimal static analysis to detect some loops that, once entered, never exit, and can thus be replaced by
[] - execute programs for a bounded number of steps
- perform cycle detection based on a repeated context (covering all cells inspected, and the whole tape in whatever direction the tape head moved in)
- for size 14 a few holdouts remain that can be checked manually.
Size 14 holdouts
The three holdouts evolve into repeating patterns:
}}<[}<}}<[<]}] }}<: 1*1 -- * indicates the tape head, so we have ... 0 0 1 to the left, 1 as the current cell, and 0 0 0 ... to the right [}<}}<: 11*1 [<]}]: 1*111 -- ! [}<}}<: 11*01 [<]}]: 111*1 [}<}}<: 1111*1 [<]}]: 1*11111 -- ! [}<}}<: 11*0111 [<]}]: 111*111 [}<}}<: 1111*01 [<]}]: 11111*1 [}<}}<: 111111*1 [<]}]: 1*1111111 -- ! ETC.
}<[}}<[<<]}}<] }<: *1 [}}<[<<]: *001 -- ! }}<]: 1*11 [}}<[<<]: 10*0 }}<]: 101*1 [}}<[<<]: *0010101 -- ! }}<]: 1*110101 [}}<[<<]: 10*00101 }}<]: 101*1101 [}}<[<<]: 1010*001 }}<]: 10101*11 [}}<[<<]: 101010*0 }}<]: 1010101*1 [}}<[<<]: *00101010101 -- ! ETC.
}<[}[<<]}}}<<] }<: *1 [}[<<]: *0 }}}<<]: 1*11 [}[<<]: *00101 -- ! }}}<<]: 1*1001 [}[<<]: 10*001 }}}<<]: 101*1 [}[<<]: 1010*0 }}}<<]: 10101*11 [}[<<]: *001010101 -- ! }}}<<]: 1*10010101 [}[<<]: 10*0010101 }}}<<]: 101*100101 [}[<<]: 1010*00101 }}}<<]: 10101*1001 [}[<<]: 101010*001 }}}<<]: 1010101*1 [}[<<]: 10101010*0 }}}<<]: 101010101*11 [}[<<]: *0010101010101 -- ! ETC.
Using Timbuk
One can use Timbuk 3.2 to verify non-termination. For example, }<[}[<<]}}}<<] can be encoded as follows:
Ops L:0 L0:1 L1:1 R:0 R0:1 R1:1 F:0 a:2 b:2 c:2 d:2 e:2 f:2 g:2 h:2 i:2 j:2 k:2 l:2 m:2 n:2 o:2 Vars x y TRS P L -> L0(L) R -> R0(R) a(x,R0(y)) -> b(L1(x),y) % } a(x,R1(y)) -> b(L0(x),y) % } b(L0(x),y) -> c(x,R0(y)) % < b(L1(x),y) -> c(x,R1(y)) % < c(x,R0(y)) -> o(x,R0(y)) % [ c(x,R1(y)) -> d(x,R1(y)) % [ d(x,R0(y)) -> e(L1(x),y) % } d(x,R1(y)) -> e(L0(x),y) % } e(x,R0(y)) -> i(x,R0(y)) % [ e(x,R1(y)) -> f(x,R1(y)) % [ f(L0(x),y) -> g(x,R0(y)) % < f(L1(x),y) -> g(x,R1(y)) % < g(L0(x),y) -> h(x,R0(y)) % < g(L1(x),y) -> h(x,R1(y)) % < h(x,R0(y)) -> i(x,R0(y)) % ] h(x,R1(y)) -> f(x,R1(y)) % ] i(x,R0(y)) -> j(L1(x),y) % } i(x,R1(y)) -> j(L0(x),y) % } j(x,R0(y)) -> k(L1(x),y) % } j(x,R1(y)) -> k(L0(x),y) % } k(x,R0(y)) -> l(L1(x),y) % } k(x,R1(y)) -> l(L0(x),y) % } l(L0(x),y) -> m(x,R0(y)) % < l(L1(x),y) -> m(x,R1(y)) % < m(L0(x),y) -> n(x,R0(y)) % < m(L1(x),y) -> n(x,R1(y)) % < n(x,R0(y)) -> o(x,R0(y)) % ] n(x,R1(y)) -> d(x,R1(y)) % ] o(x,y) -> F Set I a(L,R) Patterns F Equations Approx Rules % 42 steps L0(L1(L0(L1(x)))) = L0(L1(x)) R0(R1(R0(x))) = R0(x)
And timbuk 42 <file> will report Proof done!.
Any larger number instead of 42 will also work.
In this encoding, the left part of the tape is represented as a stack using L for the end of the stack, L0 for 0, and L1 for 1.
The right part uses R, R0, and R1 analogously, and includes the current cell.
Note that the first two rules allow the tape to be expanded to both sides.
Each program position becomes a state that's represented as a binary function symbol with left stack and right stack as arguments.
The F symbol captures program termination.
Using automata techniques, Timbuk can check that we cannot reach the (forbidden) pattern F from the initial state a(L,R).
The final section specifies approximations that help Timbuk construct a finite automaton; in this example they encode that a sequence 1010 to the left can be collapsed to 10 and the sequence 010 to the right can be collapsed to 0.
Size 14 holdouts
We only list the approximation rules; the transition rules can be generated automatically.
%%% }}<[}<}}<[<]}] (23 steps) L1(L1(L1(x))) = L1(x) R1(R1(R1(x))) = R1(x) %%% }<[}[<<]}}}<<] (42 steps) L0(L1(L0(L1(x)))) = L0(L1(x)) R0(R1(R0(x))) = R0(x) %%% }<[}}<[<<]}}<] (45 steps) L0(L1(L0(x))) = L0(x) R0(R1(R0(x))) = R0(x)
Size 15 holdouts
%%% }}<[}[<<]}}}<<] (38 steps) L1(L0(x)) = x R0(R1(R0(x))) = R0(x) %%% }}<[}}<[<<]}}<] (34 steps) L0(L1(L0(x))) = L0(x) R0(R1(R0(x))) = R0(x) %%% }<[[}}]<[<<]}}] (29 steps) L0(L) = L L0(L1(L)) = L L1(L1(x)) = x R1(R0(R1(x))) = R1(x) R1(R1(R1(x))) = R1(x) %%% }<[[<<]}}[}}]<] (28 steps) L0(L) = L L0(L1(L)) = L L1(L1(x)) = x R1(R0(R1(x))) = R1(x) R1(R1(R1(x))) = R1(x) %%% }<[[<<]}<[}}]<] (30 steps) L1(L0(L1(x))) = L1(x) R1(R0(R1(x))) = R1(x) %%% }<[[}}<[<]<]}}] (35 steps) L1(L1(x)) = x R1(R1(R1(x))) = R1(x) %%% }<[[[<]}}<}}]<] (30 steps) L1(L1(x)) = x R1(R1(R1(x))) = R1(x) %%% }<[[[<<]}}}}]<] (131 steps) L1(L1(L1(L1(x)))) = L1(L1(x)) R1(R1(R1(x))) = R1(x) %%% }<[}}<[[<]<]}}] (40 steps) L0(L) = L L1(L1(L0(L1(x)))) = L1(x) R1(R1(R0(x))) = x
Size 16 holdouts
%%% }}}}<[}<}}<[<]}] (25 steps) %%% }}<[[}}<<]}[<]}] (28 steps) %%% }}<[[}<}}<[<]]}] (25 steps) %%% }}<[[}<}}<[<]}]] (24 steps) %%% }}<[}<[]}}<[<]}] (25 steps) %%% }}<[}}<<[]}[<]}] (27 steps) %%% }}<[}<}}<[<][]}] (24 steps) %%% }}<[}<}}<[[<]]}] (24 steps) %%% }<[[<]}[}<}]}}<] (38 steps) %%% }<[[}<}]}<[<<]}] (33 steps) %%% }<[[}<}]}}<[<]}] (35 steps) %%% }<[[[<]}}]<}}}<] (40 steps) %%% }<[[<[<<]}}]<}<] (56 steps) %%% }<[[<[<]}}<}}]<] (29 steps) L1(L1(L1(x))) = L1(x) R1(R1(R1(x))) = R1(x) %%% }}<<[}[<<]}}}<<] (47 steps) %%% }<[[}}<[<<]]}}<] (53 steps) %%% }<[[}}<[<<]}}<]] (46 steps) %%% }<[}[<[]<]}}}<<] (42 steps) %%% }<[}}<[<<][]}}<] (48 steps) %%% }<[}}<[<<<<]}}<] (47 steps) %%% }<[}}<[[<]<]}}<] (50 steps) %%% }<[}}<[[<<]]}}<] (48 steps) %%% }<[}}<[<[]<]}}<] (47 steps) L0(L1(L0(x))) = L0(x) R0(R1(R0(x))) = R0(x) %%% }<[[}[<<]]}}}<<] (52 steps) %%% }<[[}[<<]}}}<<]] (46 steps) %%% }<[}[<<][]}}}<<] (48 steps) %%% }<[}[<<<<]}}}<<] (55 steps) %%% }<[}[[<]<]}}}<<] (54 steps) %%% }<[}[[<<]]}}}<<] (48 steps) %%% }<[}}[]<[<<]}}<] (34 steps) L1(L0(L1(L0(x)))) = L1(L0(x)) R0(R1(R0(x))) = R0(x) %%% }<[[}[<<]}}}]<<] (52 steps) %%% }<[}[<<]}}}[]<<] (48 steps) L1(L0(L1(L0(x)))) = L1(L0(x)) R1(R0(R1(R0(x)))) = R1(R0(x)) %%% }}<[<[}[<<}]}]<] (45 steps) %%% }<[[}}]<[<<]}}<] (47 steps) L0(L1(L0(x))) = L0(x) R1(R0(R1(R0(x)))) = R1(R0(x)) %%% }}<[[}}]<[<<]}}] (23 steps) %%% }}<[[<<]}}[}}]<] (29 steps) L0(L) = L L1(L1(L1(x))) = L1(x) L1(L0(L0(L1(x)))) = L1(L1(x)) L0(L1(L0(x))) = L0(x) R1(R0(R1(x))) = R1(x) R1(R1(R1(x))) = R1(x) %%% }<[[<<}]}[}]}}<] (51 steps) L0(L0(L0(x))) = L0(x) R1(R1(R1(x))) = R1(x) %%% }}<[[}<]}}<[<]}] (26 steps) L1(L1(L1(L))) = L1(L) R1(R1(R1(R))) = R1(R) %%% }}<[[<<]}<[}}]<] (60 steps) L1(L0(L1(x))) = L1(x) R1(R0(R1(x))) = R1(x) %%% }<[}}<[<[<]<]}}] (46 steps) L0(L1(L1(L0(x)))) = L0(x) R0(R1(R1(R0(x)))) = R0(x) %%% }<[[<]}<[}<}]<<] (46 steps) L1(L1(L1(x))) = L1(L1(x)) R1(R1(R1(x))) = R1(R1(x)) %%% }}<<[}}<[<<]}}<] (46 steps) L0(L1(L0(L1(x)))) = L0(L1(x)) R0(R1(R0(R1(x)))) = R0(R1(x)) %%% }<[}}<[<<]}[<]}] (80 steps) L1(L1(L1(x))) = L1(x) R1(R1(R1(R1(x)))) = R1(R1(x)) %%% }<[<}<[[}<}]}]<] (44 steps) L1(L1(L1(x))) = L1(x) R1(R0(R1(R0(x)))) = R1(R0(x)) %%% }}<[[[<<]}}}}]<] (83 steps) L1(L1(L1(L1(L1(x))))) = L1(L1(L1(x))) R1(R1(R1(R1(x)))) = R1(R1(x)) %%% }<[}[<<<]}}}}<<] (70 steps) L1(L1(L0(L0(L1(L0(L1(L1(L)))))))) = L1(L1(L)) R0(R1(R0(R0(R1(R1(R0(R1(R)))))))) = R0(R1(R)) %%% }}<[[<}<<]}[}]}] (60 steps) L0(L0(L0(x))) = L0(x) L0(L1(L0(L1(x)))) = L0(L1(x)) R1(R1(R1(x))) = R1(x) %%% }<[[<]}<[<}}]<<] (27 steps) L1(L1(L1(x))) = L1(L1(x)) R0(R) = R R1(R1(x)) = R1(x) %%% }<[<<[<]}[}]}<}] (48 steps) L0(L0(x)) = L0(x) L1(L0(L1(x))) = L1(x) L1(L1(L1(x))) = L1(L1(x)) R1(R1(R1(x))) = R1(R1(x)) %%% }<[}}<[<<<]}}}<] (59 steps) L1(L1(L0(L1(L1(L))))) = L1(L1(L)) L0(L1(L0(L1(L1(L))))) = L1(L1(L)) R0(R1(R1(R0(R1(R))))) = R0(R1(R)) R0(R1(R0(R0(R1(R))))) = R0(R1(R)) %%% }<[}}}<[<<<]}}<] (60 steps) L0(L1(L1(L0(L1(L))))) = L0(L1(L)) L0(L1(L0(L0(L1(L))))) = L0(L1(L)) R1(R1(R0(R1(R1(R))))) = R1(R1(R)) R0(R1(R0(R1(R1(R))))) = R1(R1(R))
Haskell Code
-- Find small BitChanger busy beavers
--
-- - candidates are normalized (using only one version of equivalent sequences of <,})
-- - initialization is minimal
-- - no trailing moves after final loop
--
-- Note that we miss candidates obtained by padding with < at the front.
-- For example, the size 15 candidate with 252 steps, }<[}}<[<<<}]}},
-- can be padded to a size 16 candidate with 253 steps, >}<[}}<[<<<}]}},
-- but the size 16 calculation omits it.
import Control.Monad
import qualified Data.Array as A
import qualified Data.Map as M
import Data.Bits
import Data.Word
import Data.List
-- convention 1: ] branches
-- convention 2: ] jumps to matching [, incurring an extra step
convention = 1
ref | convention == 1 = zip [0..] [0,1,2,3,4,5,8,11,14,17,22,27,36,45,58,252,101]
| convention == 2 = zip [0..] [0,1,2,3,4,6,10,14,18,22,26,35,47,59,71,295,123]
-- programs
data I = L | R | B !Int | E !Int
type P = A.Array Int I
instance Show I where
showsPrec _ L = ('<':)
showsPrec _ R = ('}':)
showsPrec _ B{} = ('[':)
showsPrec _ E{} = (']':)
showList = foldr (.) id . map shows
-- generate normalized programs of given length
prog :: Int -> [P]
prog n = map (\p -> A.listArray (0,n-1) p) $ replicate n R : loopy n
where
-- minimal left excursion, returns to origin
le n
| odd n = []
| n == 0 = [[]]
| n == 2 = [[L,R]]
| n == 4 = [[L,L,R,R]]
| otherwise = [[L] ++ p ++ [R] | p <- le (n-2)] ++ [[L] ++ p ++ [R,L,R] | p <- le (n-4)]
-- minimal right excursion, returns to origin
re n = reverse <$> le n
-- minimal-ish initialization
ini n
| n < 2 = []
| otherwise = [p ++ [R] ++ q ++ [L] | i <- [0,2..n-2], p <- jini (n-2-i), q <- re i]
++ [[R] ++ p ++ [L] ++ q ++ [L,R,L] ++ r | i <- [0,2..n-6], j <- [0,2..n-6-i], p <- re i, q <- ll (n-5-i-j), r <- le j]
jini 0 = [[]]
jini n = (R:) <$> rr (n-1)
-- loopy program: initialization, then non-empty loops
loopy n
| n < 5 = []
| otherwise = [p ++ [B (j+2)] ++ q ++ [E j] ++ r
| j <- [1..n-4], k <- [0..n-4-j], p <- ini (n-2-j-k), q <- body j, r <- loopy' k]
loopy' n
| n < 4 = [[] | n == 0]
| otherwise = [p ++ [B (j+2)] ++ q ++ [E j] ++ r
| j <- [1..n-3], k <- [1..n-3-j], p <- move (n-2-j-k), q <- body j, r <- loopy' k]
rr n
| n <= 2 = [replicate n R]
| otherwise = ((++ [R]) <$> rr (n-1)) ++ ((++ [R,L,R]) <$> rr (n-3))
ll n
| n <= 2 = [replicate n L]
| otherwise = ((++ [L]) <$> ll (n-1)) ++ ((++ [L,R,L]) <$> ll (n-3))
-- minimal code consisting just of < and }
move n = [p ++ q ++ r | i <- [0,2..n], j <- [0,2..n-i], p <- le i, q <- rr (n-i-j), r <- re j]
++ [p ++ q ++ r | i <- [0,2..n-1], j <- [0,2..n-1-i], p <- re i, q <- ll (n-i-j), r <- le j]
-- loop body
body n = move n
++ [p ++ [B (j+2)] ++ q ++ [E j] ++ r | i <- [0..n-2], j <- [0..n-2-i], p <- move i, q <- body j, r <- body (n-2-i-j)]
++ [[L,R,L,R] ++ p | n >= 4, p <- body (n-4)]
-- cell values (False = 0, True = 1)
type V = Bool
-- program stack for loops, position, tape
type S = (P, Int, Int, Int, [V], V, [V])
-- initial state
s0 :: P -> S
s0 p = (p, 0, 0, 0, [], False, [])
-- single step
step :: S -> Maybe S
step (p, i, _, _, _, _, _)
| not (A.inRange (A.bounds p) i) = Nothing
step (p, i, c, o, l, x, r) = Just $ case (p A.! i, l, x, r) of
(L, [], x, r) | !o <- o-1 -> (p, i+1, c+1, o, [], False, cons x r)
(L, y:l, x, r) | !o <- o-1 -> (p, i+1, c+1, o, l, y, cons x r)
(R, l, x, []) | !o <- o+1, !x <- not x -> (p, i+1, c+1, o, cons x l, False, [])
(R, l, x, y:r) | !o <- o+1, !x <- not x -> (p, i+1, c+1, o, cons x l, y, r)
(B d, l, True, r) -> (p, i+1, c+1, o, l, x, r)
(B d, l, False, r) -> (p, i+d, c+1, o, l, x, r)
(E d, l, True, r) -> (p, i-d, c+convention, o, l, x, r)
(E d, l, False, r) -> (p, i+1, c+convention, o, l, x, r)
-- helper: always compress all-0 list to []
cons False [] = []
cons x xs = x:xs
-- execution: run up to 32 steps, return number of steps if it
-- terminates, -1 if non-termination is detected; pass on to `run1` otherwise
run0 p = go (s0 p)
where
go s@(_,_,i,_,_,_,_)
| i >= 32 = run1 64 s
| Just s <- step s = go s
| otherwise = i
-- execution: run up to 2^16 steps, trying harder to detect non-termination:
-- we keep track of a previously seen state, and how much context the
-- program looked at since seeing that state; the program loops if the
-- program state and context repeats, and furthermore, if the tape head
-- moved, the tape looks the same in the direction we moved in.
run1 l (p, ip0, i, _, l0, x0, r0)
| l > 2^16
= i
| l > 2^10 && window p ip0 l0 x0 r0
= -1
| otherwise
= go 0 0 (p, ip0, i, 0, l0, x0, r0) -- reset position to 0
where
go ol oh s@(_,_,i,_,_,_,_)
| i >= l = run1 (2*l) s
| Just s@(_, _, _, o, _, _, _) <- step s
, !ol <- min o ol
, !oh <- max o oh
= go' ol oh s
| otherwise
= i
go' ol oh s@(_, ip, i, o, l, x, r)
| ip0 /= ip || -- different state
x /= x0 || -- different current cell
take (-ol) l /= take (-ol) l0 || -- different left context
take oh r /= take oh r0 -- different right context
= go ol oh s
| o == 0 -- position unchanged
= -1
| o < 0, l == l0 -- moved left
= -1
| o > 0, r == r0 -- moved right
= -1
| otherwise
= go ol oh s
-- Static non-termination check based on moving window:
-- For each program location, compute whether we can see a 0-bit or a 1-bit
-- for ~30 positions around the current position. when moving, unknown bits
-- (allowing either 0 or 1 bits) are shifted in at the end of the window.
type M = M.Map Int (Word64, Word64)
window :: P -> Int -> [V] -> V -> [V] -> Bool
window p ip l x r = go m0 M.! sz == (0,0)
where
sz = A.rangeSize (A.bounds p)
m0 :: M
m0 = M.fromList $ [(i, (0,0)) | i <- [0..sz]] ++ [(ip, (k, complement k))]
k = foldl' (\n x -> n*2 + val x) 0 (reverse (take 31 l) ++ [x] ++ take 32 (r ++ repeat False))
val False = 0
val True = 1
(a,b) .||. (c,d) = (a .|. c, b .|. d)
propagate :: M -> M
propagate m = foldl' (flip (uncurry (M.insertWith (.||.)))) m $ do
(i, b) <- A.assocs p
let (t, f) = m M.! i
case p A.! i of
L -> [(i+1, (bit 63 .|. (t `shiftR` 1), bit 63 .|. (f `shiftR` 1)))]
R | (t, f) <- (clearBit t 32 .|. (bit 32 .&. f), clearBit f 32 .|. (bit 32 .&. t))
-> [(i+1, (bit 0 .|. (t `shiftL` 1), bit 0 .|. (f `shiftL` 1)))]
B d -> [(i+1, (t, clearBit f 32)) | testBit t 32]
++ [(i+d, (clearBit t 32, f)) | testBit f 32]
E d -> [(i-d, (t, clearBit f 32)) | testBit t 32]
++ [(i+1, (clearBit t 32, f)) | testBit f 32]
go m | m' <- propagate m = if m == m' then m else go m'
main = forM_ ref $ \(n, m) -> do
putStrLn $ unwords ["---", show n, "---"]
mapM_ print $ do
p <- prog n
let s = run0 p
[(A.elems p, s) | s >= m]
Output (convention 1)
Convention 1 treats ] as a single step that either exits the loop or jumps past the corresponding [.
Note that the size 15 champion can be padded to obtain a 253 step size 16 champion; the fact that the program misses it is by design.
--- 0 --- (,0) --- 1 --- (},1) --- 2 --- (}},2) --- 3 --- (}}},3) --- 4 --- (}}}},4) --- 5 --- (}}}}},5) (}<[}],5) (}<[<],5) --- 6 --- (}}<[<],8) --- 7 --- (}}}<[<],11) --- 8 --- (}}}}<[<],14) --- 9 --- (}}}}}<[<],17) (}}}<[}<<],17) --- 10 --- (}}}}<[}<<],22) (}}<[<<<}}],22) --- 11 --- (}}}}}<[}<<],27) (}}}<[[<]}}],27) --- 12 --- (}}}}<[[<]}}],36) --- 13 --- (}}}}}<[[<]}}],45) --- 14 --- (}}<[}<}}<[<]}],65536) (}<[}[<<]}}}<<],65536) (}<[}}<[<<]}}<],65536) (}<[}}<<<[<]}}],58) --- 15 --- (}}<[}[<<]}}}<<],65536) (}}<[}}<[<<]}}<],65536) (}<[[}}]<[<<]}}],65536) (}<[[<<]}}[}}]<],65536) (}<[[<<]}<[}}]<],65536) (}<[[}}<[<]<]}}],65536) (}<[[[<]}}<}}]<],65536) (}<[[[<<]}}}}]<],65536) (}<[}}<[<<<}]}}],252) (}<[}}<[[<]<]}}],65536) --- 16 --- (}}}}<[}<}}<[<]}],65536) (}}<<[}[<<]}}}<<],65536) (}}<<[}}<[<<]}}<],65536) (}}<[[}}]<[<<]}}],65536) (}}<[[}<]}}<[<]}],65536) (}}<[[<<]}}[}}]<],65536) (}}<[[<<]}<[}}]<],65536) (}}<[[}}<<]}[<]}],65536) (}}<[[<}<<]}[}]}],65536) (}}<[[[<<]}}}}]<],65536) (}}<[[}<}}<[<]]}],65536) (}}<[[}<}}<[<]}]],65536) (}}<[<[}[<<}]}]<],65536) (}}<[}<[]}}<[<]}],65536) (}}<[}}<<[]}[<]}],65536) (}}<[}<}}<[<][]}],65536) (}}<[}<}}<[[<]]}],65536) (}<[[<]}[}<}]}}<],65536) (}<[[<]}<[}<}]<<],65536) (}<[[<]}<[<}}]<<],65536) (}<[[}}]<[<<]}}<],65536) (}<[[}<}]}<[<<]}],65536) (}<[[}<}]}}<[<]}],65536) (}<[[<<}]}[}]}}<],65536) (}<[[[<]}}]<}}}<],65536) (}<[[}[<<]]}}}<<],65536) (}<[[<[<<]}}]<}<],65536) (}<[[}}<[<<]]}}<],65536) (}<[[}[<<]}}}]<<],65536) (}<[[<[<]}}<}}]<],65536) (}<[[<[<<]}}}}]<],101) (}<[[}[<<]}}}<<]],65536) (}<[[}}<[<<]}}<]],65536) (}<[}[<<][]}}}<<],65536) (}<[}[<<]}}}[]<<],65536) (}<[}[<<<]}}}}<<],65536) (}<[}[<<<<]}}}<<],65536) (}<[}[[<]<]}}}<<],65536) (}<[}[[<<]]}}}<<],65536) (}<[}[<[]<]}}}<<],65536) (}<[}}[]<[<<]}}<],65536) (}<[<<[<]}[}]}<}],65536) (}<[}}<[<<][]}}<],65536) (}<[}}<[<<]}[<]}],65536) (}<[}}<[<<<]}}}<],65536) (}<[}}<[<<<<]}}<],65536) (}<[}}<[[<]<]}}<],65536) (}<[}}<[[<<]]}}<],65536) (}<[}}<[<[]<]}}<],65536) (}<[}}<[<[<]<]}}],65536) (}<[<}<[[}<}]}]<],65536) (}<[}}}<[<<<]}}<],65536)
Output (convention 2, champions only)
Convention 2 treats ] as a single step that jumps to the corresponding [ (which then is counted as another step).
--- 0 --- (,0) --- 1 --- (},1) --- 2 --- (}},2) --- 3 --- (}}},3) --- 4 --- (}}}},4) --- 5 --- (}<[}],6) (}<[<],6) --- 6 --- (}}<[<],10) --- 7 --- (}}}<[<],14) --- 8 --- (}}}}<[<],18) --- 9 --- (}}}}}<[<],22) --- 10 --- (}}}}}}<[<],26) (}}}}<[}<<],26) --- 11 --- (}}}<[[<]}}],35) --- 12 --- (}}}}<[[<]}}],47) --- 13 --- (}}}}}<[[<]}}],59) --- 14 --- (}}}}}}<[[<]}}],71) --- 15 --- (}<[}}<[<<<}]}}],295) --- 16 --- (}<[[<[<<]}}}}]<],123) (not a bug, see previous section)
Σ(n)
to find Σ(n) i ran all bitchanger programs of size n, took the ones that halted in S'(n) steps and took the one that outputted the most bits on the tape.
Ψ(n)
The exact same thing as Σ(n) but i instead kept pointers for the left and right boundaries of the tape
BB(17-21)
When i reached out to the bbchallange discord server, Mxdys ran TM deciders for the bitchanger programs of size 17-23
however,
for size 22 there is one holdout: }<[[}}]}}<<<<<[<<]}}}],
with the champion }<[[[<<<<]}[}<}}]}}]<] with 544457668
for size 23, there are 3 holdouts:
}<[[}}]}}<<[<<[<]<]}}}] }<[[<<]<<}<[[}<}}]}]<<] <}<[[}}]}}<<<<<[<<]}}}]
the champion is }<[}}<[<<<]}}<}[<[}]]}] which halts after roughly 10^34 steps