Finite Automata Reduction: Difference between revisions
Jump to navigation
Jump to search
m Int-y1 moved page Finite Automata Reduction (FAR) to Finite Automata Reduction: remove acronym |
Reference for Nondeterministic Finite Automata |
||
| (10 intermediate revisions by the same user not shown) | |||
| Line 1: | Line 1: | ||
{{Stub}} | {{Stub}} | ||
See [https://github.com/bbchallenge/bbchallenge-proofs/blob/build-latex-pdf/deciders/correctness-deciders.pdf Section 6] of bbchallenge's deciders write-up. | '''Finite Automata Reduction''' (short '''FAR''') is a co-[[CTL]] [[decider]]. It works by finding a regular language restricted to a class of Nondeterministic Finite Automata<ref>https://arxiv.org/pdf/2509.12337 Determination of the fifth Busy Beaver value</ref> containing all eventually halting configurations of a TM. If the empty tape is not in the regular language, the TM has been shown to be non-halting. | ||
==History== | |||
* In October 2022, Finite Automata Reduction is first introduced by Justin Blanchard,<ref>https://github.com/UncombedCoconut/bbchallenge-deciders/tree/finite-automata-reduction/decider-finite-automata-reduction</ref> later in October, Konrad Deka developes an SAT-based FAR implementation.<ref>https://github.com/colette-b/bbchallenge</ref> | |||
* In January 2023, Finite Automata Reduction is reproduced by Tony Guilfoyle.<ref>https://github.com/TonyGuil/bbchallenge/tree/main/FAR</ref> | |||
* In April 2023, the decider is added to the deciders write-up, becoming section 6. Later in April, it is also reproduced by Tristan Stérin.<ref>https://github.com/bbchallenge/bbchallenge-deciders/tree/main/decider-finite-automata-reduction-reproduction</ref> On the 9th of April, Finite Automata Reduction is applied on the remaining [[BB(5)]] holdouts.<ref>https://discuss.bbchallenge.org/t/decider-finite-automata-reduction/123</ref> | |||
==See also== | |||
* [https://github.com/bbchallenge/bbchallenge-proofs/blob/build-latex-pdf/deciders/correctness-deciders.pdf Section 6] of bbchallenge's deciders write-up. | |||
* [[Meet-in-the-Middle Weighted Finite Automata Reduction (MITMWFAR)]] | |||
==References== | |||
[[Category:Deciders]] | [[Category:Deciders]] | ||
Latest revision as of 20:53, 20 February 2026
Finite Automata Reduction (short FAR) is a co-CTL decider. It works by finding a regular language restricted to a class of Nondeterministic Finite Automata[1] containing all eventually halting configurations of a TM. If the empty tape is not in the regular language, the TM has been shown to be non-halting.
History
- In October 2022, Finite Automata Reduction is first introduced by Justin Blanchard,[2] later in October, Konrad Deka developes an SAT-based FAR implementation.[3]
- In January 2023, Finite Automata Reduction is reproduced by Tony Guilfoyle.[4]
- In April 2023, the decider is added to the deciders write-up, becoming section 6. Later in April, it is also reproduced by Tristan Stérin.[5] On the 9th of April, Finite Automata Reduction is applied on the remaining BB(5) holdouts.[6]
See also
- Section 6 of bbchallenge's deciders write-up.
- Meet-in-the-Middle Weighted Finite Automata Reduction (MITMWFAR)
References
- ↑ https://arxiv.org/pdf/2509.12337 Determination of the fifth Busy Beaver value
- ↑ https://github.com/UncombedCoconut/bbchallenge-deciders/tree/finite-automata-reduction/decider-finite-automata-reduction
- ↑ https://github.com/colette-b/bbchallenge
- ↑ https://github.com/TonyGuil/bbchallenge/tree/main/FAR
- ↑ https://github.com/bbchallenge/bbchallenge-deciders/tree/main/decider-finite-automata-reduction-reproduction
- ↑ https://discuss.bbchallenge.org/t/decider-finite-automata-reduction/123