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 ; _ . .. . _ ; Node: 1 ; Depth: 1 State: B ; _ .0 . . _ ; Node: 2 ; Depth: 2 State: A ; _1 0 . . _ ; Node: 3 ; Depth: 3 State: * ; [_]0 1 0 . . _ ; Node: 4 ; Depth: 4 State: D ; _1 0 . . _ ; Node: 5 ; Depth: 5 State: C ; _1 0 . . _ ; Node: 6 ; Depth: 5 State: B ; _ 00 . . _ ; 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
– chaotic machine: 76708232
– complex counter: 10936909
– 108082, 109520, 108115
- Counterexamples: 7410754, 3810716
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.
I think the easiest way to proof correctness would use coCTL: