Finite Automata Reduction: principle
This program finds and verifies proofs of the form:
The following finitestate machine, by construction, recognizes all halting tape configurations for this TM.
It doesn’t recognize the initial configuration. Therefore, the TM doesn’t halt from its initial configuration.
The decider correctness paper, available here, derives its algorithms from this requirement.
It’s also fair to call it a general coCTL decider, where the “co” means complement.
(The complement of a CTL is characterized by closure under timereversed TM steps. Regardless, the goal is to tell the start config apart from halting ones.)
The basis of its proof format is a specific statemachine architecture.
If the required conditions hold, the state machine works as a proof.
It’s known that all possible (co)CTL solutions are expressible in this way, though there may be translation overhead.
Moreover, the full automaton is efficiently constructible from the DFA it uses to scan one side of the tape.
This has three good consequences:
 The DFA serves as verification data, in a compact and easily parsed format. @TonyG has helpfully implemented a verifier in an independent code base.
 We get a powerful decider by searching the space of DFAs for one that works. That’s implemented in my code (
prover=direct
) and also Tony’s.  A second decider, built on a stateoftheart SAT solver (powered by cats), is automatically sound if its DFAs check out.
This second prover actually looks for for meetinthemiddle DFA solutions—which translate into the above framework but are best understood on their own terms.
(Update: This method is not part of the 20230409 decider acceptance.)
Historically, that one was developed earlier. The first public SATbased implementation is this one by @djmati1111
on Discord.
@Mateon1 also shared many insights, discoveries, results, and a public but not freestanding implementation.
Huge thanks and credit to the above authors!
The methods coexist because direct
is far superior at lower search depths, whereas mitm_dfa
scales far better at high search depths.
(When feasible, directn
covers mitm_dfan
in scope.)
Decider examples and counterexamples
From a zoology perspective, this decider’s coverage is crosscutting.
It doesn’t particularly care what the machines do, just what they won’t do (set themselves up to halt).
For grins, we can ask it to search the entire Skelet list singlethreaded at low depth (abbreviating limit
and adhoc
on the command line):
$ target/release/deciderfiniteautomatareduction l 6 l 0 a 68329601 a 55767995 a 5950405 a 6897876 a 60581745 a 58211439 a 7196989 a 7728246 a 12554268 a 3810716 a 3810169 a 4982511 a 7566785 a 31357173 a 2204428 a 20569060 a 1365166 a 15439451 a 14536286 a 347505 a 9980689 a 45615747 a 6237150 a 60658955 a 47260245 a 13134219 a 7163434 a 5657318 a 6626162 a 4986661 a 56967673 a 6957734 a 11896833 a 11896832 a 11896831 a 13609549 a 7512832 a 35771936 a 9914965 a 3841616 a 5915217 a 57874080 a 5878998
this takes about 10 seconds to solve 8/43 of them and output JSONformatted proofs:

Examples:
Skelet #4
Skelet #23
Skelet #25
Skelet #29
Skelet #32
Skelet #36
Skelet #37
Skelet #40
(Deeper searches add Skelet machines 2, 5, 6, 8, 9, 11, 12, 13, 16, 19, 24, 27, 38, and 42. See “Results”.) 
Counterexamples:
Despite the haltingproblem obstacles, proving any specific 5state TM immune to CTL proofs was an open question for quite some time. This has been settled decisively by Iijil, and there are strong heuristic arguments that a total of 30 TMs in the seed DB are completely immune to CTL.
Basically, a heuristic argument gives a reason that a TM’s halting configurations can only be told apart from reachable ones by counting, and such arguments become proofs if we can invoke the pumping lemma.
Sometimes, CTL proofs exist but are only visible to my program at absurd search depths.
@Iijil reports that BruteforceCTL solved 7046428, whereas direct10
and mitm_dfa16
(~1 threadhour each) can’t.
Similarly, the entire Halting Segment and CPS methods are covered in theory, but my program couldn’t replace them practice. (In CPS’s case, the idea is laughable.)
Decider code
Original home: bbchallengedeciders/deciderfiniteautomatareduction at finiteautomatareduction · UncombedCoconut/bbchallengedeciders · GitHub
Pull request: Finite automata reduction by UncombedCoconut · Pull Request #11 · bbchallenge/bbchallengedeciders · GitHub
Decider tests
The unit tests are inline, and the src/core/
files responsible for proofchecking are extensively tested.
Results
April 9th 2023: 503,169 machines decided using up to direct6
(6 DFA states). This takes a bit less than 30 minutes on a regular laptop.
The maximum potential is FAR greater, and has a dedicated thread.
The Decider Verification File there solves all but 38 TMs, and descending.
However, results this good are not even theoretically achievable with this version of the program (where proof search is limited to 25state DFAs for 5state TMs for efficiency reasons).
(Note: to verify this DVF with Tony’s program now requires raising MaxDFA_States
in FAR.h
.)
More practically, it should be quite easy to adopt MitMDFA in order to solve thousands more TMs. Halving the undecided index to 15543 could be done almost immediately.
For a walkthrough of operating this decider in both modes, and reproducting its results exactly, see this Results Reproduction thread.
In addition, when the undecided population shrinks further, it becomes highly practical to run the FARdirect decider again to higher depths, up to 9, without any tricks.
Database subset of application
index revision 758324e with 535801 machines.
Decider correctness
Formal presentation of the method here.