Backward Reasoning
Backward Reasoning or backtracking is a decider which simulates Turing machines backwards from all possible halting configurations, creating a tree of possible previous configurations, until a contradiction (or an impossible step) is reached. If, for all possible halting configurations, all leaves of a Backward Reasoning tree of depth reach a contradiction, it is known that, if the machine halts, it must do so in less than steps. If the machine runs for steps from an empty tape, it cannot reach any halting configurations and thus cannot halt. The amount of backward steps which are simulated can also be called the depth with which Backward Reasoning was applied.
History
- A version of Backward Reasoning is described by Shen Lin in his 1963 proof of BB(3), where he calls it back-tracking.[1]
- The idea of Backward Reasoning is again used in 1989 by Heiner Marxen in "Attacking the Busy Beaver 5".[2]
- In March 2022, the decider is introduced to Busy Beaver Challenge.[2]
- In May 2022, Backward Reasoning is added to the deciders write-up, becoming section 4. The decider is also applied to the remaining BB(5) holdouts.[2]
- In June 2022, a bug in the decider is found and fixed, leading to some less machines being marked as decided.[2]
- In October 2022, another bug is found and fixed, leading to the decider briefly being unapplied.[2]
- In August 2023, Backward Reasoning is verified in Coq (now Rocq) by meithecatte.[3]
- In November 2023, the decider is reproduced by int-y1.[2]
See also
- Section 4 of bbchallenge's deciders write-up.
- Halting Segment
References
- ↑ Shen Lin. 1963. Computer studies of Turing machine problems. PhD dissertation. Ohio State University. https://etd.ohiolink.edu/acprod/odb_etd/etd/r/1501/10?clear=10&p10_accession_num=osu1486554418657614
- ↑ 2.0 2.1 2.2 2.3 2.4 2.5 https://discuss.bbchallenge.org/t/decider-backward-reasoning/35
- ↑ https://github.com/meithecatte/busycoq