Halting Segment
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
- 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