Finite Automata Reduction - Revision history

Polygon: Reference for Nondeterministic Finite Automata

2026-02-20T20:53:36Z

Reference for Nondeterministic Finite Automata

← Older revision		Revision as of 20:53, 20 February 2026
Line 1:		Line 1:
	{{Stub}}		{{Stub}}
	'''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 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.		'''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==		==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 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>

Polygon: expanded

2026-02-20T20:44:05Z

expanded

← Older revision		Revision as of 20:44, 20 February 2026
Line 1:		Line 1:
	{{Stub}}		{{Stub}}
	'''Finite Automata Reduction''' (short '''FAR''') is a co-[[CTL]] [[decider]]. It works by finding a regular language 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.		'''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 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==		==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 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>

Polygon: rewording

2026-02-20T20:40:58Z

rewording

← Older revision		Revision as of 20:40, 20 February 2026
Line 1:		Line 1:
	{{Stub}}		{{Stub}}
	'''Finite Automata Reduction''' (short '''FAR''') is a [[~~decider~~]] ~~related to~~ [[~~Closed Tape Language~~]]. It works by finding a regular language 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.		'''Finite Automata Reduction''' (short '''FAR''') is a co-[[CTL]] [[decider]]. It works by finding a regular language 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==		==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 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>

Polygon: Missing point

2026-02-20T20:26:59Z

Missing point

← Older revision		Revision as of 20:26, 20 February 2026
Line 1:		Line 1:
	{{Stub}}		{{Stub}}
	'''Finite Automata Reduction''' (short '''FAR''') is a [[decider]] related to [[Closed Tape Language]]. It works by finding a regular language 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		'''Finite Automata Reduction''' (short '''FAR''') is a [[decider]] related to [[Closed Tape Language]]. It works by finding a regular language 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==		==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 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>

Polygon: Attempted to expand this a bit

2026-02-20T20:26:39Z

Attempted to expand this a bit

← Older revision		Revision as of 20:26, 20 February 2026
Line 1:		Line 1:
	{{Stub}}		{{Stub}}
	'''Finite Automata Reduction''' (short '''FAR''') is a [[decider]].		'''Finite Automata Reduction''' (short '''FAR''') is a [[decider]] related to [[Closed Tape Language]]. It works by finding a regular language 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==		==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 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>

Polygon: Bolded names

2025-09-04T09:14:55Z

Bolded names

← Older revision		Revision as of 09:14, 4 September 2025
Line 1:		Line 1:
	{{Stub}}		{{Stub}}
	Finite Automata Reduction (short FAR) is a [[decider]].		'''Finite Automata Reduction''' (short '''FAR''') is a [[decider]].
	==History==		==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 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>

Polygon: /* History */ Mentioned application on BB(5) holdouts

2025-08-30T13:02:28Z

History: Mentioned application on BB(5) holdouts

← Older revision		Revision as of 13:02, 30 August 2025
Line 4:		Line 4:
	* 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 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 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>		* 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==		==See also==
	* [https://github.com/bbchallenge/bbchallenge-proofs/blob/build-latex-pdf/deciders/correctness-deciders.pdf Section 6] of bbchallenge's deciders write-up.		* [https://github.com/bbchallenge/bbchallenge-proofs/blob/build-latex-pdf/deciders/correctness-deciders.pdf Section 6] of bbchallenge's deciders write-up.

Polygon: /* See also */ Added MITMWFAR to see also

2025-08-30T12:51:12Z

Polygon: Expanded history section (migrated from Cosearch)

2025-08-30T12:45:40Z

Expanded history section (migrated from Cosearch)

← Older revision		Revision as of 12:45, 30 August 2025
Line 2:		Line 2:
	Finite Automata Reduction (short FAR) is a [[decider]].		Finite Automata Reduction (short FAR) is a [[decider]].
	==History==		==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 ~~developed~~ an SAT-based FAR implementation.<ref>https://github.com/colette-b/bbchallenge</ref>		* 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>
	==See also==		==See also==
	[https://github.com/bbchallenge/bbchallenge-proofs/blob/build-latex-pdf/deciders/correctness-deciders.pdf Section 6] of bbchallenge's deciders write-up.		[https://github.com/bbchallenge/bbchallenge-proofs/blob/build-latex-pdf/deciders/correctness-deciders.pdf Section 6] of bbchallenge's deciders write-up.
	==References==		==References==
	[[Category:Deciders]]		[[Category:Deciders]]

Polygon: Began adding a history section

2025-08-30T12:32:49Z

Began adding a history section

← Older revision		Revision as of 12:32, 30 August 2025
Line 1:		Line 1:
	{{Stub}}		{{Stub}}
	Finite Automata Reduction (short FAR) is a [[decider]].		Finite Automata Reduction (short FAR) is a [[decider]].
			==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 developed an SAT-based FAR implementation.<ref>https://github.com/colette-b/bbchallenge</ref>
	==See also==		==See also==
	[https://github.com/bbchallenge/bbchallenge-proofs/blob/build-latex-pdf/deciders/correctness-deciders.pdf Section 6] of bbchallenge's deciders write-up.		[https://github.com/bbchallenge/bbchallenge-proofs/blob/build-latex-pdf/deciders/correctness-deciders.pdf Section 6] of bbchallenge's deciders write-up.
			==References==
	[[Category:Deciders]]		[[Category:Deciders]]

← Older revision		Revision as of 12:51, 30 August 2025
Line 6:		Line 6:
	* 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>		* 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>
	==See also==		==See also==
	[https://github.com/bbchallenge/bbchallenge-proofs/blob/build-latex-pdf/deciders/correctness-deciders.pdf Section 6] of bbchallenge's deciders write-up.		* [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==		==References==
	[[Category:Deciders]]		[[Category:Deciders]]