BitChanger Busy beaver/Proof

From Esolang
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)

Size 15

NOTE: this section is a work in progress

Size 15 holdouts

these are the programs that the program could not prove halt/loop for. 

}<<}[}}<<}[<]}]
<}}<[}}<<}[<]}]
}<<}[}<}}<[<]}]
<}}<[}<}}<[<]}]
}}<[}}<<}[<]}]}
}}<[}}<<}[<]}]<
}}<[}<}}<[<]}]}
}}<[}<}}<[<]}]<
}}<[}}<[<<]}}<]
<}<[}}<[<<]}}<]
}}<[}[<<]}}}<<]
<}<[}[<<]}}}<<]
}}<[[}]<}<[<]}]
<}<[[}]<}<[<]}]
}}<[[<]}[}]<}<]
<}<[[<]}[}]<}<]
}}<[[<]}[}<}]<]
<}<[[<]}[}<}]<]
}}<[[}<}]<[<]}]
<}<[[}<}]<[<]}]
}}<[[[<]}}]<}<]
<}<[[[<]}}]<}<]
}<[}}<[<<]}}<]}
}<[}}<[<<]}}<]<
}<[}[<<]}}}<<]}
}<[}[<<]}}}<<]<
}<[[}]<}<[<]}]}
}<[[}]<}<[<]}]<
}<[[<]}[}]<}<]}     
}<[[<]}[}]<}<]<
}<[[<]}[}<}]<]}
}<[[<]}[}<}]<]<
}<[[}<}]<[<]}]}
}<[[}<}]<[<]}]<
}<[[[<]}}]<}<]}
}<[[[<]}}]<}<]<
}<[}}<[[<]<]}}]
}<[}[}]<}<[<]}]
}<[<[<]}[}]<}<]
}<[<[<]}[}<}]<]
}<[[}]<}<<[<]}]
}<[[<]}}[}]<}<]
}<[[<]}<[}<}]<]
}<[[<]}[}<}]<<]
}<[[}}]<[<<]}}]
}<[[<<]}}[}}]<]
}<[[<<]}<[}}]<]
}<[[}<}]}<[<]}]
}<[[}<}]<<[<]}]
}<[[[<]}}]<}<<]
}<[[<[<]}}]<}<]
}<[[}}<[<]<]}}]
}<[[[<]}}<}}]<]
}<[[[<<]}}}}]<]

Terminology and other useful stuff

Halting equivalence

Whenever we say programs are 'Halt equivalent', we mean that if one programs halts the other halts, and if one loops the other one loops too.

Dumps

Whenever we put a letter in our code, it will act as a dump. A dump outputs a section of the tape and dump letter like this: 

000000000000110 Y1Y 00000000000000

Proof that < Does nothing when starting on an empty tape

Lets say we treat < not as moving a pointer left, but as moving a tape right. we also acknowledge that the tape is all zeroes.

if we then execute < we shift all zeroes right, but that does nothing, each zero at position n becomes the zero from n-1 (with n increasing from left to right). this means as a first instruction < only adds 1 to the number of steps.

we will use this fact to prove Halting equivalence for several programs.

Proving

Section 1: reliant on previous results

First we will prove that }}<[}}<<}[<]}] is halt equivalent to 8 programs.

The program Loops, as it was proved previously.

It is Halt equivalent with }}<[}}<<}[<]}]} and }}<[}}<<}[<]}]<. Because it the first 14 characters halt, the last character is unimportant.

}}<[}}<<}[<]}]} is halt equivalent with }}<[}<}}<[<]}]} and }}<[}}<<}[<]}]< is halt equivalent with }}<[}<}}<[<]}]<.

this can be proven because <}}< is equivalent with }<<}, and thus can be substituted.

Now, we prove }}<[}}<<}[<]}] is Halt equivalent with <}}<[}}<<}[<]}]

This is because < does nothing as a first character. (proven previously)

Now we will prove }<<}[}}<<}[<]}]< is halt equivalent <}}<[}}<<}[<]}]<

This because <}}< can be substituded with }<<}

Now we will prove }<<}[}<}}<[<]}] is equivalent with }<<}[}}<<}[<]}]< and <}}<[}<}}<[<]}] is equivalent with <}}<[}}<<}[<]}]<.

This because <}}< can be substituded with }<<}

We now proved these programs 

}<<}[}}<<}[<]}]
<}}<[}}<<}[<]}]
}<<}[}<}}<[<]}]
<}}<[}<}}<[<]}]
}}<[}}<<}[<]}]}
}}<[}}<<}[<]}]<
}}<[}<}}<[<]}]}
}}<[}<}}<[<]}]<

are equivalent to }}<[}}<<}[<]}] and since }}<[}}<<}[<]}] loops, all these programs loop.

now onto something else; }<[[<]}[}<}]<] was proven to Loop previously, thus }<[[<]}[}<}]<]< and }<[[<]}[}<}]<]} are halt equivalent (trough appending)

this means these programs loop.

Doing something VERY similar now, }<[[<]}[}]<}<] was also proven to Loop previously, thus }<[[<]}[}]<}<]< and }<[[<]}[}]<}<]} are halt equivalent (trough appending)

this means these programs also loop.

We have to do this again; }<[[}]<}<[<]}] was also proven to Loop previously, thus }<[[}]<}<[<]}]< and }<[[}]<}<[<]}]} are halt equivalent (trough appending)

this means these programs also loop.

We have to do this ANOTHER time: }<[}}<[<<]}}<] was also proven to Loop previously, thus }<[}}<[<<]}}<]< and }<[}}<[<<]}}<]} are halt equivalent (trough appending)

this means these programs also loop.

I want to keep this unrepetitive, but its tough.

}<[}[<<]}}}<<] was also proven to Loop previously, thus }<[}[<<]}}}<<]< and }<[}[<<]}}}<<]} are halt equivalent (trough appending)

this means these programs will loop.

2 more paragraphs.

}<[[}<}]<[<]}] was also proven to Loop previously, thus }<[[}<}]<[<]}]< and }<[[}<}]<[<]}]} are halt equivalent (trough appending)

this means these programs will loop.

Last part! (Sort of)

}<[[[<]}}]<}<] was also proven to Loop previously, thus }<[[[<]}}]<}<]< and }<[[[<]}}]<}<]} are halt equivalent (trough appending)

this means these programs loop.


now, we will remove 7 programs purely based on the fact that < does nothing as a first instruction. (proven previously)

Equivalent Programs
Proving now Proven previously
<}<[}}<[<<]}}<] }<[}}<[<<]}}<]
<}<[}[<<]}}}<<] }<[}[<<]}}}<<]
<}<[[}]<}<[<]}] }<[[}]<}<[<]}]
<}<[[<]}[}]<}<] }<[[<]}[}]<}<]
<}<[[<]}[}<}]<] }<[[<]}[}<}]<]
<}<[[}<}]<[<]}] }<[[}<}]<[<]}]
<}<[[[<]}}]<}<] }<[[[<]}}]<}<]

These are all the programs that were untouched after Section 1: 

}}<[}}<[<<]}}<]
}}<[}[<<]}}}<<]
}}<[[}]<}<[<]}]
}}<[[<]}[}]<}<]
}}<[[<]}[}<}]<]
}}<[[}<}]<[<]}]
}}<[[[<]}}]<}<]
}<[}}<[[<]<]}}]
}<[}[}]<}<[<]}]
}<[<[<]}[}]<}<]
}<[<[<]}[}<}]<]
}<[[}]<}<<[<]}]
}<[[<]}}[}]<}<]
}<[[<]}<[}<}]<]
}<[[<]}[}<}]<<]
}<[[}}]<[<<]}}]
}<[[<<]}}[}}]<]
}<[[<<]}<[}}]<]
}<[[}<}]}<[<]}]
}<[[}<}]<<[<]}]
}<[[[<]}}]<}<<]
}<[[<[<]}}]<}<]
}<[[}}<[<]<]}}]
}<[[[<]}}<}}]<]
}<[[[<<]}}}}]<]

Section 2: New proofs

There are still 25 programs left, programs which are more complex and there are more of.

Program 1

The program is }}<[[<]}[}]<}<]

We will put dumps like this: }}<A[[<]}[}]<}<Y] this is how the program runs: 

000000000000001 A1A 00000000000000
000000000000010 Y1Y 00000000000000
000000000000011 Y1Y 00000000000000
000000000000100 Y1Y 00000000000000
000000000000101 Y1Y 00000000000000
000000000000110 Y1Y 00000000000000
000000000000111 Y1Y 00000000000000
000000000001000 Y1Y 00000000000000
000000000001001 Y1Y 00000000000000
000000000001010 Y1Y 00000000000000
000000000001011 Y1Y 00000000000000
000000000001100 Y1Y 00000000000000
000000000001101 Y1Y 00000000000000
000000000001110 Y1Y 00000000000000
000000000001111 Y1Y 00000000000000
000000000010000 Y1Y 00000000000000
              .......

We can see it is a binary counter. since there are an infinite amount of natural numbers the program does not halt.

Program 2

This is the program: }}<[}}<[<<]}}<]

We place dumps like this: }}<A[}}<[<<]}}<X]

the program runs like this: 

00000000000000000000001 A1A 0000000000000000000000
00000000000000000000001 X1X 1010000000000000000000
00000000000000000000101 X1X 1000000000000000000000
00000000000000000010101 X1X 0000000000000000000000
00000000000000000000001 X1X 1010101000000000000000
00000000000000000000101 X1X 1010100000000000000000
00000000000000000010101 X1X 1010000000000000000000
00000000000000001010101 X1X 1000000000000000000000
00000000000000101010101 X1X 0000000000000000000000
00000000000000000000001 X1X 1010101010100000000000
00000000000000000000101 X1X 1010101010000000000000
00000000000000000010101 X1X 1010101000000000000000
00000000000000001010101 X1X 1010100000000000000000
00000000000000101010101 X1X 1010000000000000000000
00000000000010101010101 X1X 1000000000000000000000
00000000001010101010101 X1X 0000000000000000000000
00000000000000000000001 X1X 1010101010101010000000
00000000000000000000101 X1X 1010101010101000000000
00000000000000000010101 X1X 1010101010100000000000
00000000000000001010101 X1X 1010101010000000000000
00000000000000101010101 X1X 1010101000000000000000
00000000000010101010101 X1X 1010100000000000000000
00000000001010101010101 X1X 1010000000000000000000
00000000101010101010101 X1X 1000000000000000000000
00000010101010101010101 X1X 0000000000000000000000
00000000000000000000001 X1X 1010101010101010101000
00000000000000000000101 X1X 1010101010101010100000
00000000000000000010101 X1X 1010101010101010000000
00000000000000001010101 X1X 1010101010101000000000
00000000000000101010101 X1X 1010101010100000000000
00000000000010101010101 X1X 1010101010000000000000
00000000001010101010101 X1X 1010101000000000000000
00000000101010101010101 X1X 1010100000000000000000
00000010101010101010101 X1X 1010000000000000000000
00001010101010101010101 X1X 1000000000000000000000
00101010101010101010101 X1X 0000000000000000000000
                      .......

The behavior is somewhat simple, it shifts the creates ever growing Rhombi of alternating ones and zeroes.


Program 3

This is the program: }}<[}[<<]}}}<<]

We place dumps like this: }}<[}[<<]}}}<<W]

the program runs like this: 

00000000000000000000101 W1W 1000000000000000000000
00000000000000000000001 W1W 0010100000000000000000
00000000000000000000101 W1W 0010000000000000000000
00000000000000000010101 W1W 0000000000000000000000
00000000000000001010101 W1W 1000000000000000000000
00000000000000000000001 W1W 0010101010000000000000
00000000000000000000101 W1W 0010101000000000000000
00000000000000000010101 W1W 0010100000000000000000
00000000000000001010101 W1W 0010000000000000000000
00000000000000101010101 W1W 0000000000000000000000
00000000000010101010101 W1W 1000000000000000000000
00000000000000000000001 W1W 0010101010101000000000
00000000000000000000101 W1W 0010101010100000000000
00000000000000000010101 W1W 0010101010000000000000
00000000000000001010101 W1W 0010101000000000000000
00000000000000101010101 W1W 0010100000000000000000
00000000000010101010101 W1W 0010000000000000000000
00000000001010101010101 W1W 0000000000000000000000
00000000101010101010101 W1W 1000000000000000000000
00000000000000000000001 W1W 0010101010101010100000
00000000000000000000101 W1W 0010101010101010000000
00000000000000000010101 W1W 0010101010101000000000
00000000000000001010101 W1W 0010101010100000000000
00000000000000101010101 W1W 0010101010000000000000
00000000000010101010101 W1W 0010101000000000000000
00000000001010101010101 W1W 0010100000000000000000
00000000101010101010101 W1W 0010000000000000000000
00000010101010101010101 W1W 0000000000000000000000
00001010101010101010101 W1W 1000000000000000000000
                      .......

The behavior is the same as program 2, except now the bit next to the head is inverted.

Untouched programs: 

}}<[[}]<}<[<]}]
}}<[[<]}[}<}]<]
}}<[[}<}]<[<]}]
}}<[[[<]}}]<}<]
}<[}}<[[<]<]}}]
}<[}[}]<}<[<]}]
}<[<[<]}[}]<}<]
}<[<[<]}[}<}]<]
}<[[}]<}<<[<]}]
}<[[<]}}[}]<}<]
}<[[<]}<[}<}]<]
}<[[<]}[}<}]<<]
}<[[}}]<[<<]}}]
}<[[<<]}}[}}]<]
}<[[<<]}<[}}]<]
}<[[}<}]}<[<]}]
}<[[}<}]<<[<]}]
}<[[[<]}}]<}<<]
}<[[<[<]}}]<}<]
}<[[}}<[<]<]}}]
}<[[[<]}}<}}]<]
}<[[[<<]}}}}]<]
Retrieved from "https://esolangs.org/w/index.php?title=BitChanger_Busy_beaver/Proof&oldid=153609"