[Decider] Unilateral Bouncers

Deciders
1

Unilateral Bouncers: principle

This attempts to decide [Family] Unilateral bouncers.

The principle is inspired by the former description of unilateral bouncers as “[…] each successive bounce can be inductively described from the previous ones.”

To decide a machine we have an observer follow along with a run of it and try to extract the tape segments and states that we need to inductively proof that the machine never halts.

E.g. If s, i, h are tape segments and X, Y states and we find the rules:
(i) Xh turns into iYh
(ii) iYh turns into Yi
(iii) sY turns into sX
(iv) Xi turns into iX
then starting from sXh we get sXh → siYh → sYih → sXih → siXh → … → siiXh → … → siiiXh → … and can proof by induction that we get all s(i^n)Xh and thus never halt.

To show that the rules always work the machine isn’t allowed to leave the segment that it is currently transforming, i.e. Xi has to be converted into iX without leaving the i part of the tape.

To detect crablike traversing of the increment segment we allow for a buffer b in the detection:
sbXh → siYbh → sYbih → sbXih → sibXh → … → siibXh → … → siiibXh → …
now the rules work as long as e.g. bXi is converted into ibX without leaving the i or b part or the tape.

And the buffer and increment can be different for the left and right movement:
sbXh → siYph → sYpjh → sbXjh → sibXh → … → siibXh → … → siiibXh → …

Once s,h,i,j,b,p,X,Y are defined and the conversions observed (without leaving the relevant tape segment) the decider has found a unilateral bouncer. If an attempt to define the tape segments and states doesn’t lead to the correct conversions we continue the run and try again with new definitions.

Growth direction

The observer only looks for unilateral bouncers that grow to the right. A second observer could be written to find those that grow to the left, but that means any changes have to be made in two places. Mashing them together seems unwise as it would complicate the proof and be prone to errors.

We can find the left-growers by inverting the machines from the seed database before simulating them, i.e. switch all L transitions to R transitions and vice versa. For left-growers that gives us a symmetric machine that grows to the right and can be detected.

Decider examples and counterexamples

Decider code

https://github.com/Iijil1/stuff/blob/main/main.go

Decider tests

https://github.com/Iijil1/stuff/blob/main/main_test.go

Results

110570 Unilateral Bouncers that grow to the left
110781 Unilateral Bouncers that grow to the right
Total: 221351 decided

Database subset of application

11/06/22: I have run the decider on all undecided machines remaining in the seed database, that means 1538612 machines were tested. This was done in two runs, one looking for unilateral bouncers that grow to the right, the other looking for those growing to the left.

Decider correctness

It should be relatively straightforward to proof this decider correct. See this outline for the form the proof could take.

1 Like
2

Thank you for your work, it is very interesting! I find your idea very elegant and nice to reason about. I have not dived into the code yet as I want to be sure I understand the idea fully first.

I made a slight modification in your representation that helps me:

sX.iiih -> siiX.ih -> siiiX.h -> siii.Y(i^k)h -> si.Yii(i^k)h -> s.Yiii(i^k)h -> s(i^p)X.iii(i^k)h

  • I put a ‘.’ to indicate if the machine is looking at the first symbol of the block to the right of the state or to the left, sX.iiih means that the machine is in state X currently looking at the left most symbol of the first i

  • I generalised a bit saying that X.h can turn into .Y(i^k)h with k a constant of the machine (you have k=1). Same in the other direction with p where you have p = 0 in your case.

I would believe that this generalisation, with p >= 1 gives some bilateral bouncers.

My points are:

  1. I believe that a limitation of your technique is that it assumes that the increment is the same going left and going right? For instance, this bilateral bouncer uses different increments in both directions: https://bbchallenge.org/9821166 but I don’t know if unilateral bouncers can do the same.

  2. In the general case wouldn’t you need a buffer b' for what comes after X as well as what comes before X?

  3. It seems to me that implementing the above with p>=0 and k>=1 should give us many unilateral and bilateral bouncers. I expect that the machines that we will miss are those that:

    • Do not use the same increment in both directions (with a potential offset in how both directions parse the increment)
    • Are of “higher order” in the sence that s,i,h,X,Y are not unique but alternate once over two for instance (I believe it is the case of https://bbchallenge.org/2188111)

(Here’s a funny machine which seems to need a buffer for s: https://bbchallenge.org/8163699, look in explore mode)

What do you think?

3

Yeah, the X always reads to the right and the Y always reads to the left. I omitted the direction in the short notation because it reminded me of formal grammar rules.

That X.h turns into .Y(i^k)h seems to me like the result we want to proof? So the rule we need to detect is the base case and that each bounce adds 1 additional iteration. Stuff with k>1 is then handled by the proof later using the segments and rules the decider chose and verified.
(If you think k should be >1 for a single bounce, then i should be longer instead)

Explicitly describing the growth rule in the program would be useful if we want to accelerate the simulation. But it seems unnecessary for classifying and deciding the infinite.

To your points:

  1. In the first simplified description the increment is the same in both direction, just to not throw all the different letters at the reader at once. In the 3rd example sequence there is i for the increment in one direction and j in the other. That is what the decider actually looks for.

  2. On the non-buffer side of the state there is the segment we are currently converting into something else. Once whatever segment after that is entered we count that as entering the phase where we convert that new segment. Note that even if we haven’t really finished converting the old segment into its final form, it will now be part of the new buffer and we really only need to be finished with the conversion once the buffer of whatever segment conversion is going on doesn’t cover it any more.
    In practice we can choose very long buffers and turn around segments to give enough space for full conversions. Those will then be mostly just repetitions of i/j, but while that would be inconvenient for a manual proof the program handles that sort of thing just fine.

  3. The proof technique can be adapted to find bilateral bouncers, I have a version that does that. Some care needs to be taken with the borders of the segments and phase transitions, and how the growth of the tape goes into that. I find it safer to keep them separate for now.

  • As mentioned above, different increment in the two directions is not a problem.
  • The “higher order” bouncers are indeed not detected. One could write a version to detect those by going through everything twice, detecting and verifying two versions of each segment. But that gets messy and I don’t know if that is worth it with something like CTL on the horizon.

(buffer for s would not really be necessary, just choose a longer s. Though when going through the detection we still need to attach the same buffer to the state, in case it is needed to finish transforming any of the increment segments)

1 Like
4

Congrats on your work, reading your code was a pleasure as it is really clear.

I am now convinced that your decider does indeed recognise unilateral bouncers and am also confident that a formal of correctness is within reach.

I propose that we vote on whether your decider should officially be applied on bbchallenge now. Let’s give this vote 2 full weeks, starting now.

Here are my pros and cons:

Pros:

  1. The technique is elegant and yields a compact and concise code, amenable to being formally proved correct (@Iijil gave a draft of the proof).
  2. The technique seems to allow to decide all unilateral bouncers. (I still personally need to do a bit of work on my side to get 100% convinced but I trust @Iijil confidence on the matter).

Cons:

  1. A decider for bilateral bouncers will probably also recognise unilateral bouncers.
  2. Unilateral bouncers seem to “only” correspond to ~15% of the currently 1.5M undecided machines. This poses the question of whether even simpler techniques that this one could end up deciding more machines (such as your [Decider] Halting Segment).

My personal vote is in favor of applying the decider: deciding 15% of the currently undecided machines is still a significant contribution and the technique can be proved correct without too many efforts (it seems). I also like the fact that the decider seems to exactly recognise the class of unilateral bouncers. Finally, I would like to acknowledge the significant effort realised by @Iijil to put this decider outhere while achieving all the standards that we care for the code of deciders. Thank you!

5

I vote we use it. I still need to reconstruct it at some point, haven’t exactly had the most energy to do that recently, but lijil has given quite a lot of evidence that it works, and I’m keen for this project to move along.

1 Like