bbchallenge / bbchallenge-proofs

Mathematical proofs of the bbchallenge project.
Creative Commons Attribution 4.0 International
16 stars 6 forks source link

Shawn's Comments #7

Closed sligocki closed 1 year ago

sligocki commented 1 year ago

Really interesting write-up! I added comments (as \todo{}s) and tried to fix a few things (but y'all should check that my "fixes" are actually correct or if I'm misunderstanding).

One notable change that I made that may be controversial is: I switched all references to tape symbols from \mathbb{2} to {0, 1} (maybe you want to use [2] instead? I'm happy with that). My reasoning here is that \mathbb{2} had been defined as the boolean semiring and previously only used roughly as a True/False to indicate if a given state was present in a row vector or if a transition matrix transitioned from one state to another or not. I think of tape symbols as a different type of thing, they are not booleans, you can't add them, they just happen to have the same number of elements labeled the same way. But, for example, this analysis could be expanded to multi-symbol TMs in which case the \mathbb{2} and [n] would not coincide any more.

Anyway, I leave it to y'all to decide if you want to accept my suggestion here, but I think at least some explanation is necessary. When I first saw \mathbb{2} used for the symbols I really didn't understand what you were talking about at first.

UncombedCoconut commented 1 year ago

I'm fine with preferring {0,1} for just the set/alphabet. Most of these changes look good! I'm inclined to just merge, though it may be better to see what cosmo thinks first. (Also I'll punt on any question about a "\mathcal{A}" -- I believe such phrasing would have been added by cosmo in pursuit of clarity.)

\todo{Shawn's Comment: Does this just mean for any $B_0 \preceq R_0$ and $B_1 \preceq R_1$?} -- Yes. \todo{Shawn: What is $Q_{cf}$? I guess it's $Q$ in canonical form -- yes -- ... but that's the same set as $Q$, right? This is just a permutation of $[n]$?} -- not necessarily, as this definition works on DFAs in general (which have $Q$ an arbitrary finite set). \todo{Shawn: What do you mean by not standard? Like there is a more common way to refer to canonical forms, but this one differs?} - I mean that "the canonical form of a DFA" is a definition I created for present purposes; if the reader uses this term in other context, probably no one will know what they're talking about. todo{Shawn: Shouldn't this be to $m_\ell$? As in there should be something that transitions to the highest defined state (State $\ell$)?} - I'm pretty sure you're right; this may have been fallout from me improving the index conventions after I started writing.

I think writing the one element set $s=\{\begin{bmatrix}0 & e_\bot\end{bmatrix}\}$ actually doesn't make sense -- it was already a vector (representing a set of classical NFA states).

UncombedCoconut commented 1 year ago

OK, yes, your correction to the DFA \corollary{} is good. That adds to my desire to merge this (before fixing that text independently and creating a merge conflict.) Ideally we'd have a plan to make the other \todo{}s go away satisfactorily. Adding $B_0\preceq R_0$ etc. is easy enough. It's not totally clear to me that the Q_cf phrasing needs to change, though I think the DFA section is due for an editing pass soon. Let me know whether it's friendly to revert the "one element set $s=...$" change or you think I've overlooked something. Thanks for the good feedback here!

sligocki commented 1 year ago

Yeah, feel free to revert the "one element set" thing, that doesn't make any sense, you are right :) I don't feel strongly about the Qcf thing ... I just think it's confusing that you white it out without explanation for what it is, but feel free to remove my todo. In fact, feel free to remove any todo. Basically, I just added them in order to make comments in a way that would be useful :)

On Sun, Mar 19, 2023 at 8:42 PM Justin Blanchard @.***> wrote:

OK, yes, your correction to the DFA \corollary{} is good. That adds to my desire to merge this (before fixing that text independently and creating a merge conflict.) Ideally we'd have a plan to make the other \todo{}s go away satisfactorily. Adding $B_0\preceq R_0$ etc. is easy enough. It's not totally clear to me that the Q_cf phrasing needs to change, though I think the DFA section is due for an editing pass soon. Let me know whether it's friendly to revert the "one element set $s=...$" change or you think I've overlooked something. Thanks for the good feedback here!

— Reply to this email directly, view it on GitHub https://github.com/bbchallenge/bbchallenge-proofs/pull/7#issuecomment-1475460431, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAVCKWH3CNGAAKNNXQE6BTDW46RVZANCNFSM6AAAAAAWANNT6E . You are receiving this because you authored the thread.Message ID: @.***>

sligocki commented 1 year ago

Also feel free to merge if you like.

On Sun, Mar 19, 2023 at 10:02 PM Shawn Ligocki @.***> wrote:

Yeah, feel free to revert the "one element set" thing, that doesn't make any sense, you are right :) I don't feel strongly about the Qcf thing ... I just think it's confusing that you white it out without explanation for what it is, but feel free to remove my todo. In fact, feel free to remove any todo. Basically, I just added them in order to make comments in a way that would be useful :)

On Sun, Mar 19, 2023 at 8:42 PM Justin Blanchard @.***> wrote:

OK, yes, your correction to the DFA \corollary{} is good. That adds to my desire to merge this (before fixing that text independently and creating a merge conflict.) Ideally we'd have a plan to make the other \todo{}s go away satisfactorily. Adding $B_0\preceq R_0$ etc. is easy enough. It's not totally clear to me that the Q_cf phrasing needs to change, though I think the DFA section is due for an editing pass soon. Let me know whether it's friendly to revert the "one element set $s=...$" change or you think I've overlooked something. Thanks for the good feedback here!

— Reply to this email directly, view it on GitHub https://github.com/bbchallenge/bbchallenge-proofs/pull/7#issuecomment-1475460431, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAVCKWH3CNGAAKNNXQE6BTDW46RVZANCNFSM6AAAAAAWANNT6E . You are receiving this because you authored the thread.Message ID: @.***>

UncombedCoconut commented 1 year ago

OK - this thread will be here if we need it for remaining questions. :) Thanks!

tcosmo commented 1 year ago

Thank you Shawn !