search

bbchallenge / bbchallenge-proofs

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

Proof for finite-automata-reduction. #2

Closed UncombedCoconut closed 1 year ago

UncombedCoconut commented 1 year ago

Some notes about the current status...

  1. I know the halting-segment section is under construction. To avoid merge conflicts, I have left out the \input{decider-finite-automata-reduction.tex} that must be added to correctness-deciders.tex.
  2. I am planning to finish \subsection{Search algorithm: meet-in-the-middle DFA} today, but opening for feedback already.
  3. There are explicit todos where I decided not even to guess whether/how to cite certain background material (which is roughly at CS undergrad level, I think).
UncombedCoconut commented 1 year ago

(Today's force-push was just a rebase.)

UncombedCoconut commented 1 year ago

Merging to branch finite-automata-reduction so work can continue there.