[Decider] Halting Segment

Deciders
#1

Halting Segment: principle

This decider is based on backwards reasoning and as such is not applicable to a specific family of machines.

This decider works similar to backwards reasoning. Starting from all configurations that halt the next step we look at all possible predecessors and continue doing so. If we find that no more predecessors are possible and haven’t found the starting configuration, then it is impossible for the machine to halt.

The difference to backwards reasoning is that we only allow the configuration descriptions to fix a limited tape segment around the eventual halting position.

If a predecessor comes from outside that segment we allow the machine to do anything it wants there. This is a set of configuration where any state is possible and any position in a given direction of the fixed segment is possible, in addition to the typical freedom of any symbol on the tape being possible outside of the fixed parts.

Assuming there is a 1 in the fixed segment we know that the machine has to have visited the fixed segment before and can pick up the search of predecessors at the point where it left the region around the halting position, leaving the fixed segment behind.

If we eventually find that there is no 1 on the fixed segment, then we have found a path from the starting position to the halting state that follows the machines rules whenever it is in the given region around the halting position. In that case we cannot say whether the machine halts or not.

If on the other hand we find no more possible predecessors, then no such path is possible, and the machine doesn’t halt.

The proof by Newcomb Greenleaf for Marxen & Buntrock’s chaotic machine relies on such an unreachable halting segment: To halt the machine needs an isolated 1, or the segment 010 on the right side of the tape (originally left, but the machine is mirrored in bbchallenge’s database.) But it is not possible to ever leave such a segment behind.

This decider finds the same result:

=== RUN   TestChaosMachine
-   0   1
- --- ---
A 1RB 1LB
B 1LC 0RE
C 0LD 0RA
D 1RA 0LD
E ??? 0RC

State: E ;  _ . .[0]. . _  ; Node: 1 ; Depth: 1
State: B ;  _ .[1]0 . . _  ; Node: 2 ; Depth: 2
State: A ;  _[0]1 0 . . _  ; Node: 3 ; Depth: 3
State: * ; [_]0 1 0 . . _  ; Node: 4 ; Depth: 4
State: D ;  _[1]1 0 . . _  ; Node: 5 ; Depth: 5
State: C ;  _[0]1 0 . . _  ; Node: 6 ; Depth: 5
State: B ;  _ 0[0]0 . . _  ; Node: 7 ; Depth: 6
Proved nonhalting with segment size 5 after expanding 7 nodes

Increasing the size of the segment can dramatically increase the depth needed to prove a given machine. So to scan the undecided machines I included a recursive mode, that tries again with a larger segment whenever a path to the starting position is found, until the total number of nodes expanded reaches some limit.

Decider examples and counterexamples

Decider code

https://github.com/Iijil1/Iijils-bb-challenge/blob/main/halting-segment/main.go

Decider tests

https://github.com/Iijil1/Iijils-bb-challenge/blob/main/halting-segment/main_test.go

Results
11/07/2022: 995554 machines were decided.

Database subset of application
11/07/2022: The decider was run in recursive mode expanding up to 10000 nodes on the 1538612 undecided machines at this time.

Decider correctness

I think the easiest way to proof correctness would use coCTL:

3 Likes
[Decider] Unilateral Bouncers
[July 16th 2022] Standard text format for TMs and 2 deciders in review
Currently applied deciders
[December 25th 2022] 1,002,823 new machines have been decided!
#2

This is really exciting, thank you for posting. This is both natural and powerful, what’s not to love?

Will review your code and share my comments, even though it seems really good from far.

To anyone reading this (@tomtom2357 I think this might appeal to you): alternative implementations of the idea would be welcome to confirm the results.

Thank you again!

#3

This is actually great - it fixes the biggest problem with backwards reasoning, that you’ll get stuck on some cycle relying on tape state that’s impossible to reach because the machine wouldn’t have written it.

What tape sizes did you use for your searches? What’s the maximum amount of times a machine has stepped off the fixed segment of the tape in a useful proof? What’s the largest depth you’ve encountered?

#4

What tape sizes did you use for your searches?

So far I have been recursively increasing the tape size for a machine whenever a path to the starting configuration was found. So if we can’t prove anything with tape size 3 we try again with type size 5, then 7 and so on. Until a total of 10000 configurations have been seen.
In one case that led to a successful proof with tape size 27 for #36902517. Though I think only the left half of that tape was ever used.
I’ve always used symmetric tapes, with the same max distance in both directions. But there are certainly some machines where that isn’t optimal.

What’s the maximum amount of times a machine has stepped off the fixed segment of the tape in a useful proof?

I have not kept track of that. But while writing/testing I have seen some machines that do this quite a lot. Especially when the tape size isn’t optimal.

What’s the largest depth you’ve encountered?

The longest path I’ve found had length 856 by #10575846. But the configurations aren’t arranged in a tree and I’ve used a depth-first approach to searching the graph, so that is not the minimal path length. Rerunning that machine breadth-first gives a minimal path length of 422 (with segment size 9)

#5

I have implemented my own HaltingSegments Decider in C++, available at bbchallenge/HaltingSegments at main · TonyGuil/bbchallenge · GitHub. It finds all of lijil’s 995,554 machines, plus another 25,080 machines due to its broader segment-matching criterion. I had to run it at depth 1,000 and a node limit of 60,000 to decide all of lijil’s machines; perhaps we are counting nodes differently? This took 160 minutes.

Here is the search tree for one of the newly decided machines (#30414):

(1)   . .[.]. .  HALT
(2)   .[1]. . .   A
(3)  [1]1 . . .    B
(4)   1 1 . . .     *
(5)  [1]1 . . .      C
(6)   1 1 . . .       * Duplicate of (4)
(7)   1[1]. . .       C
(8)   1 1[1]. .        C Duplicate of (7)
(9)  [0]1 . . .      D

Line (8) curtails the search because it matches line (7), shifted right by 1.

My code is not easy to follow, and I don’t think I’m capable of proving anything about it. So I need to come up with a Decider Verification File format that lets others verify these results. If anybody has any ideas, let me know!

1 Like
Bouncers
[Decider] Finite Automata Reduction
#6

That is excellent news, thank you!

Great to bring reproductions of this technique, would be interesting to dig into the differences that make you decide more machines.

What kind of dvf are you thinking about?

#7

If you go to the github link, you will see a brief description of my more general segment-matching criterion. I implemented it using a tree of trees to store the already-seen segments, which is what makes the code rather squeaky. I ran my own tests on this tree of trees before incorporating it into my search, but I can’t really expect you all to trust me on this!

So a more informative dvf file would be useful, but I haven’t had any workable ideas yet. I will add the segment width to the decider-specific info, and run the decider again (overnight this time, with a deeper search); but beyond this, I am open to suggestions.

#8

I have no good idea for verification data. Even if you provide the entire set of configurations that were found, a verifier would essentially need to redo all the work to check that it is correct. So just saying that the machine was decidable with a given segment size would be about as good.

One could also add on how long that took, so a verifier doesn’t have to look forever, or until it reaches its own step limit. But I think in all the implementations I know of the nodes/steps/configurations were counted in different ways, so there doesn’t seem to be a natural way to express that. The more permissive segment matching you do would also change the node count.

I don’t count configurations that were seen before again, so the (6) in your example would not be counted. going from under 10000 to up to 60000 with just that difference seems extreme, but might be possible.

#9

As promised, I added the segment width to the dvf format, and ran a deeper search. See bbchallenge/HaltingSegments at main · TonyGuil/bbchallenge · GitHub for details.

A few more machines were found, making a total of 1,022,541. This leaves 516,083 machines still undecided.

1 Like
#10

Update: change of heart.

I was unsettled about the approach I proposed in the earlier version of this post. Instead, we decided to modify slightly Iijil’s stopping criterion in a way that makes it independent of any ordering on the DFS’s node: we are going to exhaustively search the entire space up to tape size N, for odd tape lengths only, starting from center position, as in Iijil’s original strategy.

That way, the stopping criterion is much more reproducible.

Here are my results:

max segment size number of machines decided run time
7 855186 20s
9 943633 30s
11 983961 1m
13 1002808 4m
15 1012659 15m

Now, I am going to tweak @Iijil’s implem to use the same stopping criterion and compare results.

We’ll then need a proof of correctness and then, we’ll be done!!

Very excited to get this decider behind the finish line!

#11

Now that the reproduction is done (yay), it should be safe to peek back into the repo, where there is:
https://raw.githubusercontent.com/Iijil1/Iijils-bb-challenge/main/halting-segment/Sketch%20of%20Proof.txt

Lines 1-11 define a general* co-CTL; they’re solid.
* meaning not required to be a regular language

The next paragraph is legitimate background.

The next describes the algorithm: begin with the set of immediately halting configurations, and repeatedly augment the set with predecessor configurations (if they keep the head within the segment) or supersets either prefixed or suffixed with (0|1|predecessor_state)* as appropriate. The construction obviously produces a co-CTL, and so it can be matched against the start configuration.

I believe this is actually sufficient with minor tweaks.

  1. Fix typos “bout” (line 1) and “it’s” (line 20, should be “its”)
  2. For an implementation that starts with only halt-in-center configurations rather than all immediately halting configurations, we should point out that a “pointed” co-CTL is sufficient. That is, if condition 1 is replaced with 1'. all configurations where the TM immediately halts at position p are in C, C’s existence proves the TM can’t halt at position p; if we also require 3'. C does not contain any translation of the starting configuration, then the TM can’t get from any translated starting configuration to a halt at p. A further translation shows the TM therefore can’t halt anywhere from the starting configuration.

@Iijil, would you like a crack at it, or would you rather see a more thorough independent write-up?

#12

Yes, it’s great that we have solid elements to start the proof but the standard I have in mind is academic, i.e. full on proof with pseudocode and illustrations like done for Cyclers/Translated Cyclers/Backward Reasoning: bbchallenge-proofs/correctness-deciders.pdf at main · bbchallenge/bbchallenge-proofs · GitHub.

I think it is important not to defer this effort because currently the method is well incrusted in our brains and it will be way easier to do it now than in a few months.

#13

Thanks to @Iijil’s updated code, I was able to run the results for segment size 11 (3.8 MB) and they exactly match the 983961 machines found by my rust reproduction above.

Hence, we have perfect reproduction for segment size 11!

I will try to run segment size 13 and 15 with Iijil’s code too, so we can accept as many machines as possible.

We really just need a correctness proof now, working on that.

#14

Please note that my implementation of the forwards version of halting segment also reproduces the exact same result, 983961 machines with tape of size 11, only checking the center cell for halting.

I believe this gives more confidence, given that two very similar implementations of the same method and one implementation of a complementary method give the exact same results.

1 Like
#15

Excellent news! Thank you! Can you also reproduce size 13 as I expect that we will be able to get the go results soon?

#16

Yes, I did reproduce the N=13 results as well. Sadly I don’t have the free compute for now to do anything much larger.

1 Like
#17

I ran @Iijil 's code on size 13 and got exact same 1002808 machines as in my rust reproduction above (but run time was 2h20m).

Hence, we can move forward with officially deciding these 1002808 machines once we have the proof of correctness written up!

#18

The formal proof for HS has been written (GitHub - bbchallenge/bbchallenge-proofs: Mathematical proofs of the bbchallenge project.) hence, the decider validates all the criteria of [Debate & Vote] Deciders’ validation process, hence the size-13 results were officially applied today!!!

Many thanks to @Iijil for proposing the method and being… extremely patient with the reviewing process. Many thanks to all those that also participated to the discussions and reviewing process, including @mateon1, @Nathan-Fenner, @TonyG and @UncombedCoconut !

Here is the main figure of the proof which gives the full Halting Segment graph (from the initial nodes) for a 3-state machine:

halting-segment