[Decider] Halting Segment

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:

2 Likes

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!

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?

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)