Bouncers: principle

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.


Taking posted results at face value, here’s a quick Venn diagram:

 halting_segment &  ctl_veryslow &  bouncers &  cps_8_16        957803   
 halting_segment &  ctl_veryslow & ~bouncers &  cps_8_16        44969    
 halting_segment & ~ctl_veryslow &  bouncers &  cps_8_16        20      
 halting_segment & ~ctl_veryslow & ~bouncers &  cps_8_16        16     
~halting_segment &  ctl_veryslow &  bouncers &  cps_8_16        239259   
~halting_segment &  ctl_veryslow & ~bouncers & ~cps_8_16        12827   
~halting_segment & ~ctl_veryslow &  bouncers & ~cps_8_16        1434   
~halting_segment & ~ctl_veryslow & ~bouncers &  cps_8_16        304     
~halting_segment &  ctl_veryslow &  bouncers & ~cps_8_16        205253   
~halting_segment &  ctl_veryslow & ~bouncers &  cps_8_16        74245    
~halting_segment & ~ctl_veryslow &  bouncers &  cps_8_16        2087    
~halting_segment & ~ctl_veryslow & ~bouncers & ~cps_8_16        407   

(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.

Do you have a provisional list of such intransigent machines? I could run my Bouncer Decider on it with souped-up parameters, to see how many I can settle.

At a later time, I plan to upload more detailed info.
For now, a recent list of the most stubborn machines to solve is available here:

I am afraid to report that a search with a time limit of 10,000,000 decides only one of the machines in your list (#13458880) as a bouncer. (But that’s progress, right?)

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”)
  • Bruteforce-CTL probably isn’t needed (still interesting though)
  • “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…

Ha! I found another bouncer in there: #347505. You have to increase Steps to 30,000 in the SImulation Parameters to see the cyclic behaviour. It has three partitions, and 104 runs (see bbchallenge/Bouncers at main · TonyGuil/bbchallenge · GitHub for terminology).