Halting Segment: Difference between revisions
Jump to navigation
Jump to search
Added information about how the decider works |
Separated lead and method |
||
| (3 intermediate revisions by the same user not shown) | |||
| 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 | '''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== | |||
* In July 2022, the Halting Segment decider is first introduced by lijil | == 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 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> | ||
| 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]] | ||
Latest revision as of 10:56, 1 April 2026
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.
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[1]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.[2]
- In September 2022, Nathan Fenner verifies Halting Segment in Dafny.[3]
- In October 2022, the decider is reproduced by Tony Guilfoyle[1] and in November 2022 again by Tristan Stérin.[4]
- 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.[1]
See also
Section 5 of the bbchallenge deciders write-up.
References
- ↑ 1.0 1.1 1.2 https://discuss.bbchallenge.org/t/decider-halting-segment/75
- ↑ https://gist.github.com/mateon1/7f5e10169abbb50d1537165c6e71733b
- ↑ https://github.com/Nathan-Fenner/bbchallenge-dafny-deciders/blob/main/halting-segment.dfy
- ↑ https://github.com/bbchallenge/bbchallenge-deciders/tree/main/decider-halting-segment-reproduction