In compliance with our validation process, we’re officially releasing the decider for bouncers today!
-
The formal presentation and proof of correctness of the decider is given in Section 7 of bbchallenge’s official write-up.
-
The method decided 29,799 machines (91%) over the 32,632 that were left undecided after the previous [Decider] Finite Automata Reduction release.
-
The official undecided index has been updated and certificates for the bouncers released: https://github.com/bbchallenge/bbchallenge-undecided-index/releases/tag/bouncers.
-
The implementations (and reproductions) for the decider are:
- Tony Guilfoyle’s C++ initial implementation (does not use the theory presented in the write-up)
- Iijil’s Go implementation (does not use the theory presented in this section)
- savask’s Haskell implementation (basis of the theory presented in the write-up)
- mei’s optimised Rust implementation, reproducing savask’s. This implementation outputs certificates that are verified using Coq, more details about this approach will be given in future versions of the write-up.
- Tristan Stérin’s (cosmo’s) Rust implementation, reproducing savask’s and mei’s. This implementation follows the write-up to the letter, reproducing each concept and algorithm as presented here. It is less efficient than mei’s.
Many thanks to @TonyG for initially presenting the method and to all the contributors that have participated in the release: @Iijil, @savask, @meithecatte, @UncombedCoconut, Pascal Michel, @cosmo.
Beaverly yours,
