Halting Segment - Revision history

Polygon: Separated lead and method

2026-04-01T10:56:19Z

Separated lead and method

← Older revision		Revision as of 10:56, 1 April 2026
Line 1:		Line 1:
	{{Stub}}		{{Stub}}
	'''Halting Segment''' is a [[decider]] which is based on [[Backward Reasoning]]. It starts from all configurations of a TM which will halt within the next step and looks for all possible predecessors by taking backward steps. However, only a limited tape segment with the halting position at its center is actually simulated, this segment is called the fixed segment. Outside of this segment all possible configurations of symbols, states and directions are allowed. All of these outside configurations have to be considered to determine predecessors which re-enter the fixed segment. If no more predecessors are found to be possible without the starting configuration having been found, the machine is shown to be non-halting.		'''Halting Segment''' is a [[decider]] which is based on [[Backward Reasoning]], with the difference being that instead of considering the entire tape, it only looks at a fixed segment around the halting positions.
	==History==
			== Method ==
			It starts from all configurations of a TM which will halt within the next step and looks for all possible predecessors by taking backward steps. However, only a limited tape segment with the halting position at its center is actually simulated, this segment is called the fixed segment. Outside of this segment all possible configurations of symbols, states and directions are allowed. All of these outside configurations have to be considered to determine predecessors which re-enter the fixed segment. If no more predecessors are found to be possible without the starting configuration having been found, the machine is shown to be non-halting.

			== History ==
	* In July 2022, the Halting Segment decider is first introduced by lijil<ref name=":0">https://discuss.bbchallenge.org/t/decider-halting-segment/75</ref>and on the eleventh of July the decider is applied to the remaining [[BB(5)]] holdouts.		* In July 2022, the Halting Segment decider is first introduced by lijil<ref name=":0">https://discuss.bbchallenge.org/t/decider-halting-segment/75</ref>and on the eleventh of July the decider is applied to the remaining [[BB(5)]] holdouts.
	* In August 2022, Halting Segment is reproduced by Mateon1.<ref>https://gist.github.com/mateon1/7f5e10169abbb50d1537165c6e71733b</ref>		* In August 2022, Halting Segment is reproduced by Mateon1.<ref>https://gist.github.com/mateon1/7f5e10169abbb50d1537165c6e71733b</ref>
Line 9:		Line 13:
	* In November 2023, int-y1 reproduced Halting Segment and wrote a forward implementation of it.<ref name=":0"/>		* In November 2023, int-y1 reproduced Halting Segment and wrote a forward implementation of it.<ref name=":0"/>

	==See also==		== See also ==
	[https://github.com/bbchallenge/bbchallenge-proofs/blob/build-latex-pdf/deciders/correctness-deciders.pdf Section 5] of the bbchallenge deciders write-up.		[https://github.com/bbchallenge/bbchallenge-proofs/blob/build-latex-pdf/deciders/correctness-deciders.pdf Section 5] of the bbchallenge deciders write-up.

	==References==		== References ==
	[[Category:Deciders]]		[[Category:Deciders]]

Polygon: Bolded name

2025-09-04T09:12:58Z

Bolded name

← Older revision		Revision as of 09:12, 4 September 2025
Line 1:		Line 1:
	{{Stub}}		{{Stub}}
	Halting Segment is a [[decider]] which is based on [[Backward Reasoning]]. It starts from all configurations of a TM which will halt within the next step and looks for all possible predecessors by taking backward steps. However, only a limited tape segment with the halting position at its center is actually simulated, this segment is called the fixed segment. Outside of this segment all possible configurations of symbols, states and directions are allowed. All of these outside configurations have to be considered to determine predecessors which re-enter the fixed segment. If no more predecessors are found to be possible without the starting configuration having been found, the machine is shown to be non-halting.		'''Halting Segment''' is a [[decider]] which is based on [[Backward Reasoning]]. It starts from all configurations of a TM which will halt within the next step and looks for all possible predecessors by taking backward steps. However, only a limited tape segment with the halting position at its center is actually simulated, this segment is called the fixed segment. Outside of this segment all possible configurations of symbols, states and directions are allowed. All of these outside configurations have to be considered to determine predecessors which re-enter the fixed segment. If no more predecessors are found to be possible without the starting configuration having been found, the machine is shown to be non-halting.
	==History==		==History==
	* In July 2022, the Halting Segment decider is first introduced by lijil<ref name=":0">https://discuss.bbchallenge.org/t/decider-halting-segment/75</ref>and on the eleventh of July the decider is applied to the remaining [[BB(5)]] holdouts.		* In July 2022, the Halting Segment decider is first introduced by lijil<ref name=":0">https://discuss.bbchallenge.org/t/decider-halting-segment/75</ref>and on the eleventh of July the decider is applied to the remaining [[BB(5)]] holdouts.

Polygon: /* History */ mentioned date of application on BB(5)

2025-08-29T21:54:33Z

History: mentioned date of application on BB(5)

← Older revision		Revision as of 21:54, 29 August 2025
Line 2:		Line 2:
	Halting Segment is a [[decider]] which is based on [[Backward Reasoning]]. It starts from all configurations of a TM which will halt within the next step and looks for all possible predecessors by taking backward steps. However, only a limited tape segment with the halting position at its center is actually simulated, this segment is called the fixed segment. Outside of this segment all possible configurations of symbols, states and directions are allowed. All of these outside configurations have to be considered to determine predecessors which re-enter the fixed segment. If no more predecessors are found to be possible without the starting configuration having been found, the machine is shown to be non-halting.		Halting Segment is a [[decider]] which is based on [[Backward Reasoning]]. It starts from all configurations of a TM which will halt within the next step and looks for all possible predecessors by taking backward steps. However, only a limited tape segment with the halting position at its center is actually simulated, this segment is called the fixed segment. Outside of this segment all possible configurations of symbols, states and directions are allowed. All of these outside configurations have to be considered to determine predecessors which re-enter the fixed segment. If no more predecessors are found to be possible without the starting configuration having been found, the machine is shown to be non-halting.
	==History==		==History==
	* In July 2022, the Halting Segment decider is first introduced by lijil.<ref name=":0">https://discuss.bbchallenge.org/t/decider-halting-segment/75</ref>		* In July 2022, the Halting Segment decider is first introduced by lijil<ref name=":0">https://discuss.bbchallenge.org/t/decider-halting-segment/75</ref>and on the eleventh of July the decider is applied to the remaining [[BB(5)]] holdouts.
	* In August 2022, Halting Segment is reproduced by Mateon1.<ref>https://gist.github.com/mateon1/7f5e10169abbb50d1537165c6e71733b</ref>		* In August 2022, Halting Segment is reproduced by Mateon1.<ref>https://gist.github.com/mateon1/7f5e10169abbb50d1537165c6e71733b</ref>
	* In September 2022, Nathan Fenner verifies Halting Segment in [https://en.wikipedia.org/wiki/Dafny Dafny].<ref>https://github.com/Nathan-Fenner/bbchallenge-dafny-deciders/blob/main/halting-segment.dfy</ref>		* In September 2022, Nathan Fenner verifies Halting Segment in [https://en.wikipedia.org/wiki/Dafny Dafny].<ref>https://github.com/Nathan-Fenner/bbchallenge-dafny-deciders/blob/main/halting-segment.dfy</ref>

Polygon: Reworded parts of the introduction

2025-08-29T21:28:27Z

Reworded parts of the introduction

← Older revision		Revision as of 21:28, 29 August 2025
Line 1:		Line 1:
	{{Stub}}		{{Stub}}
	Halting Segment is a [[decider]] which is based on [[Backward Reasoning]]. It starts from all configurations of a TM which will halt within the next step and looks for all possible predecessors. However, only a limited tape segment ~~around~~ the halting position ~~(usually on the middle of the segment)~~ is actually simulated, this segment is called the fixed segment. Outside of this segment all possible configurations of symbols, states and directions are allowed. All of these outside configurations have to be considered to determine predecessors which re-enter the fixed segment. If no more predecessors are found to be possible without the starting configuration having been found, the machine is shown to be non-halting.		Halting Segment is a [[decider]] which is based on [[Backward Reasoning]]. It starts from all configurations of a TM which will halt within the next step and looks for all possible predecessors by taking backward steps. However, only a limited tape segment with the halting position at its center is actually simulated, this segment is called the fixed segment. Outside of this segment all possible configurations of symbols, states and directions are allowed. All of these outside configurations have to be considered to determine predecessors which re-enter the fixed segment. If no more predecessors are found to be possible without the starting configuration having been found, the machine is shown to be non-halting.
	==History==		==History==
	* In July 2022, the Halting Segment decider is first introduced by lijil.<ref name=":0">https://discuss.bbchallenge.org/t/decider-halting-segment/75</ref>		* In July 2022, the Halting Segment decider is first introduced by lijil.<ref name=":0">https://discuss.bbchallenge.org/t/decider-halting-segment/75</ref>

Polygon: Added information about how the decider works

2025-08-29T21:21:35Z

Added information about how the decider works

← Older revision		Revision as of 21:21, 29 August 2025
Line 1:		Line 1:
	{{Stub}}		{{Stub}}
	Halting Segment is a [[decider]] which is based on [[Backward Reasoning]].		Halting Segment is a [[decider]] which is based on [[Backward Reasoning]]. It starts from all configurations of a TM which will halt within the next step and looks for all possible predecessors. However, only a limited tape segment around the halting position (usually on the middle of the segment) is actually simulated, this segment is called the fixed segment. Outside of this segment all possible configurations of symbols, states and directions are allowed. All of these outside configurations have to be considered to determine predecessors which re-enter the fixed segment. If no more predecessors are found to be possible without the starting configuration having been found, the machine is shown to be non-halting.
	==History==		==History==
	* In July 2022, the Halting Segment decider is first introduced by lijil.<ref name=":0">https://discuss.bbchallenge.org/t/decider-halting-segment/75</ref>		* In July 2022, the Halting Segment decider is first introduced by lijil.<ref name=":0">https://discuss.bbchallenge.org/t/decider-halting-segment/75</ref>

Polygon: Added a short description

2025-08-29T20:59:54Z

Added a short description

← Older revision		Revision as of 20:59, 29 August 2025
Line 1:		Line 1:
	{{Stub}}		{{Stub}}
			Halting Segment is a [[decider]] which is based on [[Backward Reasoning]].
	==History==		==History==
	* In July 2022, the Halting Segment decider is first introduced by lijil.<ref name=":0">https://discuss.bbchallenge.org/t/decider-halting-segment/75</ref>		* In July 2022, the Halting Segment decider is first introduced by lijil.<ref name=":0">https://discuss.bbchallenge.org/t/decider-halting-segment/75</ref>

Polygon: /* History */ Expanded history section (migration from Cosearch)

2025-08-29T20:34:44Z

History: Expanded history section (migration from Cosearch)

← Older revision		Revision as of 20:34, 29 August 2025
Line 1:		Line 1:
	{{Stub}}		{{Stub}}
	==History==		==History==
	* In July 2022, the Halting Segment decider is first introduced by lijil.<ref>https://discuss.bbchallenge.org/t/decider-halting-segment/75</ref>		* In July 2022, the Halting Segment decider is first introduced by lijil.<ref name=":0">https://discuss.bbchallenge.org/t/decider-halting-segment/75</ref>
	* In August 2022, Halting Segment is reproduced by Mateon1.<ref>https://gist.github.com/mateon1/7f5e10169abbb50d1537165c6e71733b</ref>		* In August 2022, Halting Segment is reproduced by Mateon1.<ref>https://gist.github.com/mateon1/7f5e10169abbb50d1537165c6e71733b</ref>
	* In September 2022, Nathan Fenner verifies Halting Segment in [https://en.wikipedia.org/wiki/Dafny Dafny].<ref>https://github.com/Nathan-Fenner/bbchallenge-dafny-deciders/blob/main/halting-segment.dfy</ref>		* In September 2022, Nathan Fenner verifies Halting Segment in [https://en.wikipedia.org/wiki/Dafny Dafny].<ref>https://github.com/Nathan-Fenner/bbchallenge-dafny-deciders/blob/main/halting-segment.dfy</ref>
			* In October 2022, the decider is reproduced by Tony Guilfoyle<ref name=":0"/> and in November 2022 again by Tristan Stérin.<ref>https://github.com/bbchallenge/bbchallenge-deciders/tree/main/decider-halting-segment-reproduction</ref>
			* In December 2022, Halting Segment is added to the deciders write-up, becoming section 5.
			* In November 2023, int-y1 reproduced Halting Segment and wrote a forward implementation of it.<ref name=":0"/>

	==See also==		==See also==
	[https://github.com/bbchallenge/bbchallenge-proofs/blob/build-latex-pdf/deciders/correctness-deciders.pdf Section 5] of the bbchallenge deciders write-up.		[https://github.com/bbchallenge/bbchallenge-proofs/blob/build-latex-pdf/deciders/correctness-deciders.pdf Section 5] of the bbchallenge deciders write-up.

Polygon: Added more information about history (migrated from Cosearch)

2025-08-29T20:06:00Z

Added more information about history (migrated from Cosearch)

← Older revision		Revision as of 20:06, 29 August 2025
Line 2:		Line 2:
	==History==		==History==
	* In July 2022, the Halting Segment decider is first introduced by lijil.<ref>https://discuss.bbchallenge.org/t/decider-halting-segment/75</ref>		* In July 2022, the Halting Segment decider is first introduced by lijil.<ref>https://discuss.bbchallenge.org/t/decider-halting-segment/75</ref>
			* In August 2022, Halting Segment is reproduced by Mateon1.<ref>https://gist.github.com/mateon1/7f5e10169abbb50d1537165c6e71733b</ref>
			* In September 2022, Nathan Fenner verifies Halting Segment in [https://en.wikipedia.org/wiki/Dafny Dafny].<ref>https://github.com/Nathan-Fenner/bbchallenge-dafny-deciders/blob/main/halting-segment.dfy</ref>
	==See also==		==See also==
	[https://github.com/bbchallenge/bbchallenge-proofs/blob/build-latex-pdf/deciders/correctness-deciders.pdf Section 5] of the bbchallenge deciders' write-up.		[https://github.com/bbchallenge/bbchallenge-proofs/blob/build-latex-pdf/deciders/correctness-deciders.pdf Section 5] of the bbchallenge deciders write-up.

	==References==		==References==
	[[Category:Deciders]]		[[Category:Deciders]]

Polygon: /* See also */ grammar fix

2025-08-29T19:50:44Z

Polygon: Fixed reference

2025-08-29T19:48:56Z

Fixed reference

← Older revision		Revision as of 19:48, 29 August 2025
Line 1:		Line 1:
	{{Stub}}		{{Stub}}
	==History==		==History==
	* In July 2022, the Halting Segment decider is first introduced by lijil.<ref>https://discuss.~~bbchallange~~.org/t/decider-halting-segment/75</ref>		* In July 2022, the Halting Segment decider is first introduced by lijil.<ref>https://discuss.bbchallenge.org/t/decider-halting-segment/75</ref>
	==See also==		==See also==
	[https://github.com/bbchallenge/bbchallenge-proofs/blob/build-latex-pdf/deciders/correctness-deciders.pdf Section 5] of bbchallenge deciders' write-up.		[https://github.com/bbchallenge/bbchallenge-proofs/blob/build-latex-pdf/deciders/correctness-deciders.pdf Section 5] of bbchallenge deciders' write-up.
	==References==		==References==
	[[Category:Deciders]]		[[Category:Deciders]]

← Older revision		Revision as of 19:50, 29 August 2025
Line 3:		Line 3:
	* In July 2022, the Halting Segment decider is first introduced by lijil.<ref>https://discuss.bbchallenge.org/t/decider-halting-segment/75</ref>		* In July 2022, the Halting Segment decider is first introduced by lijil.<ref>https://discuss.bbchallenge.org/t/decider-halting-segment/75</ref>
	==See also==		==See also==
	[https://github.com/bbchallenge/bbchallenge-proofs/blob/build-latex-pdf/deciders/correctness-deciders.pdf Section 5] of bbchallenge deciders' write-up.		[https://github.com/bbchallenge/bbchallenge-proofs/blob/build-latex-pdf/deciders/correctness-deciders.pdf Section 5] of the bbchallenge deciders' write-up.

	==References==		==References==
	[[Category:Deciders]]		[[Category:Deciders]]