In a nutshell, the method gives a very efficient algorithm for finding a regular language that describes the eventually-halting configurations of a TM. That way, the TM can be proven to be non-halting if the initial, all-0 configuration is not part of the language. This approach is closely related to @heiner and @sligocki CTL method.
Following the requirements of [Debate & Vote] Deciders’ validation process, the method is close to the finish line because:
- The decider follows the principles of our reproducibility and verifiability statement.
- It decides 99% of the currently undecided machines (it only leaves a few hundreds undecided machine out of the current 535,801).
- The decider has been reproduced independently by @TonyG (here) and by @cosmo (here).
- The method has been formally presented and proven correct here (still WIP but currently in a good readable state).
One notable feature of the method is that, it is very well suited to verification: for a given machine decided by Finite Automata Reduction, it is easy to provide a certificate with the necessary and sufficient data (mainly consisting in a specific finite automaton) which allow to conclude that the machine doesn’t halt. Moreover, the task of verifying that such certificates are valid is computationally simple.
This brings us to the point of this topic: re-finding from scratch all FAR proofs that have been found by @UncombedCoconut (and combined in this ~15Mb DVF file (DVF stands for Decider Validation File)) requires months of compute power and quite an expertise to accelerate the search algorithm in certain cases. However:
All those proofs, combined in the ~15Mb DVF file, are easy to verify: it takes roughly 5 minutes on a 8-core laptop to verify all ~500k proofs using the slow (but hopefully easy to follow) Python implementation of the verifier.
Hence, here is what I propose, and please feel free to express your opinion on this post:
- We officially accept all machines that have a FAR certificate present in the DVF file, regardless of how hard was the proof to produce.
- We require that ~70% of the proofs of the DVF file to be re-found independently. The Python independent implementation of the decider, available here, could achieve this goal using a few hours of compute time.
So, maybe put a heart reaction if you are OK with that plan and/or express your opinion in this thread