Finite Automata Reduction: principle
This program finds and verifies proofs of the form:
The following finite-state 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 co-CTL decider, where the “co-” means complement.
(The complement of a CTL is characterized by closure under time-reversed TM steps. Regardless, the goal is to tell the start config apart from halting ones.)
The basis of its proof format is a specific state-machine 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 state-of-the-art SAT solver (powered by cats), is automatically sound if its DFAs check out.
This second prover actually looks for for meet-in-the-middle DFA solutions—which translate into the above framework but are best understood on their own terms.
(Update: This method is not part of the 2023-04-09 decider acceptance.)
Historically, that one was developed earlier. The first public SAT-based 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, direct-n
covers mitm_dfa-n
in scope.)
Decider examples and counterexamples
From a zoology perspective, this decider’s coverage is cross-cutting.
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 single-threaded at low depth (abbreviating --limit
and --ad-hoc
on the command line):
$ target/release/decider-finite-automata-reduction -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 JSON-formatted 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 halting-problem obstacles, proving any specific 5-state 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 Bruteforce-CTL solved 7046428, whereas direct-10
and mitm_dfa-16
(~1 thread-hour 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: bbchallenge-deciders/decider-finite-automata-reduction at finite-automata-reduction · UncombedCoconut/bbchallenge-deciders · GitHub
Pull request: Finite automata reduction by UncombedCoconut · Pull Request #11 · bbchallenge/bbchallenge-deciders · GitHub
Decider tests
The unit tests are in-line, and the src/core/
files responsible for proof-checking are extensively tested.
Results
April 9th 2023: 503,169 machines decided using up to direct-6
(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 25-state DFAs for 5-state 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 MitM-DFA 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 FAR-direct 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.