BitChanger Busy beaver/Proof

From Esolang
Jump to navigation Jump to search

Proof sketch (mostly computational)

  • 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

Four holdouts evolve into repeating patterns: 

}}<[}}<<}[<]}] and }}<[}<}}<[<]}] (noting that }}<<} and }<}}< are equivalent)

  }}<: 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.

The remaining ones can be analysed with small contexts: 

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

  }<: *1
  [[}]<}<: ?*1?
  [<]}]:   ?1*1?
  ETC.

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

  }<: *1
  [[<]}:   ?1*1?
  [}]<}<]: ?*10?
  ETC.

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

  }<: *1
  [[<]}:   ?1*1?
  [}<}]<]: ?*10?
  ETC.

}<[[}<}]<[<]}]
  }<: *1
  [}<}]<: ?*10?
  [<]}]:  ?1*1?
  ETC.

  }<: *1
  [[<]: ?*01?
  }}]:  ?0*0?
  <}<]: ?*10?
  ETC.

Haskell Code

-- Find small BitChanger busy beavers

import Control.Monad

-- Bitchanger programs.
type P = [I]
data I = R | L | Loop P
    deriving Eq

instance Show I where
    showsPrec _ R = ('}':)
    showsPrec _ L = ('<':)
    showsPrec _ (Loop i) = ('[':) . shows i . (']':)
    showList = foldr (.) id . map shows

-- generate programs of given length
prog :: Int -> [P]
prog 0 = [[]]
prog n = simple ++ loop
  where
    simple = do
        p <- prog (n-1)
        i <- [R,L]
        [i:p]
    loop = do
        i <- [0..n-2]
        l <- prog i
        guard $ i == 0 || useful l
        r <- prog (n-2-i)
        [Loop l : r]

-- Basic static analysis to find whether a loop is useful: If we can
-- prove that loop body, ends on a 1 bit, then we could use an empty
-- loop instead. We know that initially, the bit at the pointer is 1.
-- We also know that inner loops exit with a 0 at the current pointer
-- (if they exit).
useful xs = lr True 0 xs
  where
    lr b n []          = n /= 0 || not b
    lr b n (L:xs)      = lr b (n-1) xs
    lr b n (R:xs)      = lr (if n == 0 then not b else b) (n+1) xs
    lr _ _ (Loop _:xs) = lr False 0 xs

-- cell values (False = 0, True = 1)
type V = Bool
-- program stack for loops, position, tape
type S = ([P], Int, [V], V, [V])

-- initial state
s0 :: P -> S
s0 p = ([p], 0, [], False, [])

-- single step
step :: S -> Maybe S
step ([[]],  _, _, _, _) = Nothing
step ([]:ps, o, l, x, r) = step (ps, o, l, x, r) -- convention 1: ] jumps into or after loop
-- step ([]:ps,o,l,x,r) = Just (ps, o, l, x, r) -- convention 2: ] jumps to [
step ((i:p):ps, o, l, x, r) = Just $ case (i, l, x, r) of
    (L, [],  x, r) | !o <- o-1 -> (p:ps, o, [], False, cons x r)
    (L, y:l, x, r) | !o <- o-1 -> (p:ps, o, l, y, cons x r)
    (R, l, x,  []) | !o <- o+1, !x <- not x -> (p:ps, o, cons x l, False, [])
    (R, l, x, y:r) | !o <- o+1, !x <- not x -> (p:ps, o, cons x l, y, r)
    (Loop q, l, True, r) -> (q : (i:p) : ps, o, l, x, r)
    (Loop q, l, False, r) -> (p : ps, 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 0 (s0 p)
  where
    go i s
        | i >= 32          = run1 (2*i) i s
        | ((Loop []:_):_,_,_,True,_) <- s = -1
        | Just s <- step s = go (i+1) 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 i (ps0, _, l0, x0, r0)
    | l > 2^16
    = i
    | otherwise
    = go i 0 0 (ps0, 0, l0, x0, r0)        -- reset position to 0
  where
    go i ol oh s
        | i >= l = run1 (2*l) i s
        | ((Loop []:_):_,_,_,True,_) <- s = -1
        | Just s@(_, o, _, _, _) <- step s
        , !ol <- min o ol
        , !oh <- max o oh
        = go' (i+1) ol oh s
        | otherwise
        = i
    go' i ol oh s@(ps, o, l, x, r)
        | ps0 /= ps ||                     -- 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 i ol oh s
        | o == 0                           -- position unchanged
        = -1
        | o < 0, l == l0                   -- moved left
        = -1
        | o > 0, r == r0                   -- moved right
        = -1
        | otherwise
        = go i ol oh s

main = forM_ [0..14] $ \s -> do
    putStrLn $ unwords ["---", show s, "---"]
    -- values to validate, convention 1 (] checks loop):
    let (n,m) = zip [0..] [0,1,2,3,4,5, 8,11,14,17,22,27,36,45,58] !! s
    -- values to validate, convention 2 (] jumps to [):
    -- let (n,m) = zip [0..] [0,1,2,3,4,6,10,14,18,22,26,35,47,59,71] !! s
    mapM_ print $ do
        p <- prog n
        let s = run0 p
        [(p, s) | s >= m]

Output (convention 1, abridged)

Convention 1 treats ] as a single step that either exits the loop or jumps past the corresponding [. 

--- 0 ---
(,0)
--- 1 ---
(},1)
(<,1)
--- 2 ---
(}},2)
(<},2)
(}<,2)
(<<,2)
--- 3 ---
(}}},3)
...
(<<<,3)
--- 4 ---
(}}}},4)
...
(<<<<,4)
--- 5 ---
(}}}}},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)
(}<[}}<<<[<]}}],58)
(}<[}}<[<<]}}<],65536)
(}<[}[<<]}}}<<],65536)
(}<[[}]<}<[<]}],65536)
(}<[[<]}[}]<}<],65536)
(}<[[<]}[}<}]<],65536)
(}<[[}<}]<[<]}],65536)
(}<[[[<]}}]<}<],65536)

Output (convention 2, abridged)

Convention 2 treats ] as a single step that jumps to the corresponding [ (which then is counted as another step). 

--- 0 ---
(,0)
--- 1 ---
(},1)
(<,1)
--- 2 ---
(}},2)
(<},2)
(}<,2)
(<<,2)
--- 3 ---
(}}},3)
...
(<<<,3)
--- 4 ---
(}}}},4)
...
(<<<<,4)
--- 5 ---
(}<[}],6)
(}<[<],6)
--- 6 ---
(}}<[<],10)
--- 7 ---
(}}}<[<],14)
--- 8 ---
(}}}}<[<],18)
--- 9 ---
(}}}}}<[<],22)
--- 10 ---
(}}}}}}<[<],26)
(}}}}<[}<<],26)
--- 11 ---
(}}}<[[<]}}],35)
--- 12 ---
(}}}}<[[<]}}],47)
--- 13 ---
(}}}}}<[[<]}}],59)
--- 14 ---
(}}}}}}<[[<]}}],71)
(}}<[}}<<}[<]}],65536)
(}}<[}<}}<[<]}],65536)
(}<[}}<[<<]}}<],65536)
(}<[}[<<]}}}<<],65536)
(}<[[}]<}<[<]}],65536)
(}<[[<]}[}]<}<],65536)
(}<[[<]}[}<}]<],65536)
(}<[[}<}]<[<]}],65536)
(}<[[[<]}}]<}<],65536)

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=153102"