bbchallenge-proofs's Introduction

bbchallenge's proofs

For The Busy Beaver Challenge to be successful we want to formally prove as many of the challenge's results as possible.

This includes:

Proving the correctness of deciders (https://github.com/bbchallenge/bbchallenge-deciders)
Proving the non-halting/halting of specific individual machines that are not covered by deciders

Please see our reproducibility and verifiability statement for more.

We elaborate and store these proofs here.

Future work: using theorem provers

At the moment we focus on writing standard plain-English proofs but future work includes a translation to formal proof systems such as Lean or Coq.

License

This work is licensed under a Creative Commons Attribution 4.0 International License.

You should have received a copy of the license along with this work. If not, see http://creativecommons.org/licenses/by/4.0/.

bbchallenge-proofs's People

Contributors

Stargazers

Watchers

bbchallenge-proofs's Issues

[Bouncers] Lemma 7.16, proof case 2, help the reader understand why the HP of Lemma 7.15 applies

Compiled Discord feedback on decider-finite-automata-reduction (and a few overall)

(savask) 6.1: 1) " ... at least all ... ", I suggest just "all".
(savask) 6.1: 2) "... eventually-halting configurations ... ", one should remind briefly what a configuration is. I know it's in the preliminaries, but it's a chance to clarify the term "eventually-halting" and remind a crucial definition at the same time.
(savask) 6.1: 3) Shawn Ligocki -> S. Ligocki, since other people are cited with initials.
(savask) 6.1: 4) "... it is a simple task ...", I suggest to remove bold font and say "computationally simple".
(savask) 6.2: 5) "Let M_{m,n} be the set of matrices ... Boolean domain 2 ...". I suggest to split this into two sentences. First, "Let 2 denote the Boolean semiring, where + and * are ,,,", and then "Let M ... be the matrix semiring over ...". I think the word "semiring" stresses that associativity holds, and it is used later on.
(savask) 6.2: 6) "... i-th entry of q0 is set to 1 ...", maybe worth adding "... and all other are set to 0"
(savask) 6.2: 7) "... one of its execution traces ... " maybe better to write "... if there is a path from the initial state to the accepting state", since the notion of an "execution trace" isn't used anywhere else.
(savask) 6.2: 8) " ... which algebraically translates to q0 Tu a = 1". The definition of Tu = T1 ... Tl is missing.
(savask) 6.2: 9) I suggest to move the definition of <= relation for matrices to the paragraph where the set of conditions is simplified, as that is the first time this relation is used. I think it is also helpful to note that if qTa = 1 and T < K then qKa = 1.
(savask) 6.2: 10) "Hence, if we call L the regular ..." -> "If L is the regular ..."
(savask) 6.2: 11) "We translate these into ..." maybe something like "These conditions are implied by the following, generally stronger, conditions on the transition matrix ..."
(savask) 6.2: 12) "Then, we want our ..". I think one should avoid "wanting" something in the text, so something like "... the language L must include ..." seems better. ;; (bt) or "a desirable property of L is to include..." might be better if that property is not guaranteed ;; (savask) If it does not hold then the argument won't work, so it's not simply desirable, but required in my opinion
(savask) 6.2: 13) Notation of c1, c2, c3 and "hats" should be explained before the displayed formula. I had to waste some time looking in the preliminaries, thinking that it was defined there.
(savask) 6.2: 14) I think "just a bit b" needn't be mentioned before the displayed formulae, since it is written there that b \in 2
(savask) 6.2: 15) Maybe it's worth explaining that ufrz is the concatenation of u, f, r, z.
(savask) 6.2: 16) Remove "These conditions are unwieldy" and say something more neutral like "For simplicity, we replace this set of conditions by a simpler one ..."
(savask) 6.2: 17) "q0 Tu Tf Tr is a vector q' satisfying q' Tz a = 1" simplify that into "q0 Tu Tf Tr Tz a = 1 for all z \in 2*". In general, try to avoid using quantifiers \forall \exists where possible.
(savask) 6.2: 18) "accepted steady state s" maybe add "s \in M_{1,n}"
(savask) 6.2: 19) "transitions are total up to the head", it's not clear what that means, but in any case bold font should be removed.
(savask) 6.2: 20) "that a subset of (1) - (8)", I think it should be (1) - (9)
(savask) A more general remark, applying everywhere: one should expand "let's", "doesn't", "isn't" etc to "let us", "does not", "is not" etc
(savask) 6.2: First, I think one should explicitly explain how a TM configuration is translated into a word in the alphabet {0, 1, A, ..., E} (right now it's a bit vague and relies on an example).
(savask) 6.2: Second, I think the section would benefit tremendously if one put all the arguments about simplifying conditions etc into the proof of Theorem 18. I suggest to state the theorem right after closure conditions for the language L are introduced (so before "the above conditions turn into"), and then prove that the language L corresponding to the NFA from the statement satisfies all the closure properties. The current argument "we want that", "we simplify this" shows the rationale behind conditions (1) - (9), but I think it would be better if it was hidden inside the proof and made a bit more rigorous.
(savask) Looks like you used a darker shade of red lol
(bt) is spelling "for ever" intentional? I'd write it as "forever", but I'm not a native English speaker.
(bt) positioning of floats could be better. The worst offender here is Figure 2 that appears at page 7 while being discussed in detail at the page 4. That's a lot of scrolling.
(bt) the definition of Distance L is defined as being the maximum distance to record position 1 that was visited between the configuration of record 1 and record 2. was really hard for me to grok.
AFAIU, this is reminiscent of Scott Aaronsons's "cosmological horizon" argument, which is very easy to visualise, so maybe a descriptive name would help? "Bounding radius", "storage space used", "max-retreat-distance"?
(bt) Awkward phrase: These can get significantly more complex, bbchallenge’s machine #59,090,563 is an example see Figure 3 and https://bbchallenge.org/59090563
(bt) Auxiliary routine compute-distance-L (Algorithm 3, l.1) uses the “pebbles” that were left on the tape to give the last time a memory cell was seen I think the best place for describing the "pebbles" is a first explanation of L, several pages earlier