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

[x] (savask) 6.1: 1) " ... at least all ... ", I suggest just "all".
[x] (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.
[x] (savask) 6.1: 3) Shawn Ligocki -> S. Ligocki, since other people are cited with initials.
[x] (savask) 6.1: 4) "... it is a simple task ...", I suggest to remove bold font and say "computationally simple".
[x] (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.
[x] (savask) 6.2: 6) "... i-th entry of q0 is set to 1 ...", maybe worth adding "... and all other are set to 0"
[x] (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.
[x] (savask) 6.2: 8) " ... which algebraically translates to q0 Tu a = 1". The definition of Tu = T1 ... Tl is missing.
[x] (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.
[x] (savask) 6.2: 10) "Hence, if we call L the regular ..." -> "If L is the regular ..."
[x] (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
[x] (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.
[x] (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}"
[x] (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.
- [x] (savask) Looks like you used a darker shade of red lol
- [x] (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

bbchallenge / bbchallenge-proofs

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