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.
Thus, it deals in generic co-CTL arguments (“co-CTL” being the complement of a CTL, characterized by a time-reversed version of the latter’s closure criteria).
Any CTL or co-CTL solution to a TM is representable in this decider’s format. (There may be translation overhead.)
The README explains in more detail how the automata, CTL, and co-CTL perspectives are connected.
For complete TM proofs, I impose a specific state-machine architecture, such that the proof goes through as soon as the invariants are checked.
Fortunately, the decider includes an efficient way to reconstruct proofs from just a DFA describing how a language – either CTL or co-CTL – handles one side of the tape.
This is also the heart of the program’s first prover, which incrementally builds a DFA and checks whether it can work in a proof.
A second prover prescribes a more restrictive form of FA (also fully general with translation overhead), such that the search problem translates well to a boolean satisfiability (SAT) problem that we can delegate to an excellent incremental solver.
Because all proofs are checked, the algorithms can get complex without raising correctness concerns about the decider.
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 at low depth (abbreviating
--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
On a laptop and single-threaded, this takes about 10 seconds to solve 8/43 of them:
This command also outputs JSON-formatted proofs.
Skelet #34 in particular is conjectured to be immune to pure CTL solutions, due to the way it writes all bit patterns on both sides – and the lack of obvious other reasons it wouldn’t halt.
The unit tests are in-line, and the
src/core/ files responsible for proof-checking are extensively tested.
In progress – number of machines solved depends on one’s patience.
If you have only 17 minutes (and one thread on a laptop) to spare, the
direct solver with a depth limit of
5 will bring today’s undecided index (~1.5 million) down to just 81494 unsolved.
The deeper search’s status as of this edit is: 1529124 verifiably solved, 9500 unsolved.
When ready, provide the results of your decider under the form of a file containing the IDs of the machines it decided in the seed database.
Database subset of application
index revision 645dc9f with 1538624 machines.
Covered in the README file.