This is to announce a Decider and Verifier for all types of Bouncers. A Bouncer is a machine that moves back and forth between (and sometimes through!) walls that drift ever further apart.
As well as being categorised as Unilateral, Bilateral, or Translated, a Bouncer can also be categorised by how many times it bounces back and forth before completing its cycle; and by how many internal walls it has. The DecideBouncers program recognises all types of Bouncer, and outputs a Decider Verification File for checking by the VerifyBouncers program.
If fed the 1,538,624 machines left undecided by the Backward Reasoning decider, it decides 1,405,856 (91%) of them, taking about three and a half minutes. As a spin-off, It also categorises 18,643 of the undecided machines as Probable Bells (see ProbableBells.txt); no doubt some of these are Bouncers rather than Bells (see e.g. Bouncer #3653511, which pretends to be a Bell but can’t quite keep it up), and some of them are neither.
For the moment, please see bbchallenge/Bouncers at main · TonyGuil/bbchallenge · GitHub for more details, including source code, executables, and a full description of the (rather complicated) Verification Data format. I have started on a description of the verification process, but I ran out of steam before I finished it. I will come back to it in a few days, when I have finished some real-world work that is waiting for me.
(taken within the universe of the 1.5 million TM undecided index, with halting_segment etc. being decided subsets and ~halting_segment, etc. being undecided subsets - and with ctl_veryslow representing my decider through direct-9 and mitm_dfa-12 - I don’t have indexes for CPS with very high parameters available)
Also, just anecdotally, a huge fraction of the machines that are hard for the FA/CTL solvers are funny-looking bouncers (sometimes glued to counters). Inductive solvers that take care of the bouncer zoology would complement the other methods very well.
That’s actually quite a good result, because this list includes results reported by @univerz from an inductive prover.
It’s sort of true (if overly simplistic) that some deciders naturally complement each other whereas others naturally compete. My fallible understanding is that: (a) this bouncer decider’s most natural competitors are such an inductive prover and GitHub - Iijil1/Bruteforce-CTL: An attempt to proof that a turing machine doesn't halt by finding a closed tape language using bruteforce (ironically not very brutish, also explicitly tunable for bouncers), (b) the inductive prover hasn’t had the same level of publication/documentation work done, (c) Bruteforce-CTL needs a whole lot more than 3.5 minutes to make much progress.
Update based on Discord conversations and better searching:
@univerz’s prover matters only as a benchmark. (“its under continuous construction for breaking BB6 record; but i do not think we can get that code to bbchallenge replicability standards, its too complicated”)
“Rule-proving simulation acceleration” by @sligocki (thread: Shawn's Holdouts) has the potential to generalize/subsume the “bouncers” decider, based on reported results. I haven’t yet checked its performance, ease of reproduction, and ease of proof. Your decider looks good on those fronts…
The relevance issue is subjective, speculative, and fluid.
Discord is good for such conversations and has been more active.
To summarize my impressions:
The active community right now is small; many are busy with non-BB things.
The most active topic right now is Halting Segment; we want to finish it off while it’s fresh.
I love finite automata! I just hit a milestone ~yesterday that lets me pause work on the subject. It’s not something everyone’s working on. There’s ample space for you to compete or help. It doesn’t cover/obsolete a Bouncers decider.
CPS may or may not be the next thing after that to draw community attention – depends on when key proponents free up the time to do the reproduction/verification work. It doesn’t cover/obsolete a Bouncers decider either.
The most likely thing to cover/obsolete a Bouncers decider is general accelerated simulation / inductive proof. There’s one hedged opinion that it should - but the job of building such a decider to the reproducibility and verifiability standards is tough and not in progress. Undone work can’t obsolete done work. (@sligocki does have real, working code with potential to be reproduced and proven.)
I’ll be taking a look at your new work.
I’m pretty confident guessing that either your direction or Shawn’s (et. al.) must be pursued in order to finish off BB(5).
The process that you refer to is unnecessarily restrictive! Clearly, it is enough to validate the Verifier rather than the Decider. How the Decider arrives at its conclusions is irrelevant – as long as its output can be verified, that should be enough.
For Translated Cyclers, the verification process is trivial. So any machine that has a verifiable certificate should be accepted.
For Bouncers, the verification process (as documented on GitHub) is more complicated. But it is still simpler than the Decider. Validating my Decider is unnecessary.
I have an idea for useful verification data for HaltingSegments. I have modified my Halting Segments Decider so that it visits the search nodes in exactly the same order as @Iijil’s go implementation. Now when I arrive at a node that has already been seen according to my broader criterion (see [Decider] Halting Segment - #5 by TonyG) I can output the IndexString of the original matched node into the dvf, along with the index of the search node where it is required. So it is a simple matter to verify that the current position satisfies the IndexString according to my criteria. (Never mind if this explanation is a little incomplete; when I have the code ready I will post a fuller account on Deciders:Halting Segments. My point is that we don’t have to restrict ourselves artificially to validating Deciders, when there are other ways of achieving the confidence level required.)
The process has been discussed at length on the forum and on discord and is currently the one in place.
I 100% agree that there is merit in the verifier approach, while raising the point that it is probably not universal (some techniques may not have any suitable verifier).
My opinion is to move to this more agile governance model (i.e. validating machines on the fly based on verifier data) once we reach a small set of undecided machines, which, given the projected results of current methods that are discussed on discord should be around 10,000 machines.
Finally, note that the restrictiveness and constraints in the current process are thought to ensure maximal trust in validated techniques and do the ground work necessary for publication (reproductions, formal proofs, etc…).
You are more than welcome to express your opinion in the thread and/or discord.
I have discovered a small problem, which means that six of my claimed Bouncers are of uncertain status. The problem is that Bouncer::CheckTapesEquivalent checks that two tape descriptors are equivalent, but only for the specific values of their RepeaterCount array. For the inductive proof to hang together, it should check that the tapes are equivalent for any RepeaterCount values greater than or equal to the current ones; I have amended the code to check for this, and six machines fail the amended test. I am pondering the best way to fix this. I suspect that most of these six are in fact Bouncers, but not all of them.
The problem is solved. All the uncertain cases turned out to be Bouncers afer all. I have posted the fix to github, and updated the Readme file to better explain the verification process.
Note: The format of the Decider Verification File has changed slightly: nRuns is now ushort, and RepeaterCount has been removed from RunDescriptor. If anybody out there is verifying, I apologise for the inconvenience.
Re: validating Decider vs. Verifier. I think this could be a bit of a terminology issue. I completely agree with you @TonyG that only the Verifier needs to be validated. Effectively, I would call your Verifier the “True Decider” in your system while the thing you’re calling a decider is sort of a heuristic detail that helps you search for a proof certificate. I’ve been really interested in this type of split for a long time, I’m excited to see that you’ve implemented it. I’m reading up now.
FWIW, here’s a rebased index showing what of today’s undecided index is unsolved by “Bouncers” with the 1M limit. undecided_index_filtered_by_Bouncers_1M.umf (342.7 KB)
Sadly, the larger search now outdoes the fast 100K search by only 9 beavers. Still worthwhile, and reordering the decider runs could slash the cost a great deal.
On Discord, it was noted that for a few bouncers where Tony’s approach has a huge advantage over Shawn’s otherwise more general approach: Shawn’s code uses fixed-size blocks, so a bouncer with (real example) 4-, 5-, and 7-periodic runs will escape detection.
Funny zoological point: The class solved by this decider could be called the “quadratic” bouncers (in analogy with the “exponential” counters). This is by far the main and largest group of “bouncing” machines. However, there are others which are surely bouncing, but are keeping themselves busy to a higher degree along the way. (Sorry, didn’t have a simple 5-state example handy.) Perhaps the zoology should distinguish these cases.
@savask (Discord) announced a new Bouncers implementation.
This one is written in Haskell, a high-level functional programming language, and able to express the method and comments/examples in under 500 lines.
(This doesn’t include the seed DB and index file integration. It uses the TM text format.)
The linear/quadratic rule for detecting Cycle boundaries is the same, as is the high-level matching strategy. Some finer implementation details differ, and it doesn’t try to be DVF-compatible with Tony’s program. Savask reports that it solves the same machine population, though, so it would corroborate the results by the same standards as most bbchallenge deciders.