Backward Reasoning: Difference between revisions
Jump to navigation
Jump to search
(Expanded beginning) |
(Added history section) |
||
| Line 2: | Line 2: | ||
Backward Reasoning 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 <math>D</math> reach a contradiction, it is known that, if the machine halts, it must do so in less than <math>D</math> steps. If the machine runs for <math>D</math> 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. | Backward Reasoning 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 <math>D</math> reach a contradiction, it is known that, if the machine halts, it must do so in less than <math>D</math> steps. If the machine runs for <math>D</math> 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== | |||
* The idea of Backward Reasoning was already used in 1989 by Heiner Marxen in "Attacking the Busy Beaver 5".<ref name=":0">https://discuss.bbchallenge.org/t/decider-backward-reasoning/35</ref> | |||
* In March 2022, the decider is introduced to Busy Beaver Challenge.<ref name=":0"/> | |||
* 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.<ref name=":0"/> | |||
* In June 2022, a bug in the decider is found and fixed, leading to some less machines being marked as decided.<ref name=":0"/> | |||
* In October 2022, another bug is found and fixed, leading to the decider briefly being unapplied.<ref name=":0"/> | |||
* In August 2023, Backward Reasoning is verified in Coq (now Rocq) by meithecatte.<ref>https://github.com/meithecatte/busycoq</ref> | |||
==See also== | ==See also== | ||
* [https://github.com/bbchallenge/bbchallenge-proofs/blob/build-latex-pdf/deciders/correctness-deciders.pdf Section 4] of bbchallenge's deciders write-up. | * [https://github.com/bbchallenge/bbchallenge-proofs/blob/build-latex-pdf/deciders/correctness-deciders.pdf Section 4] of bbchallenge's deciders write-up. | ||
==References== | |||
[[Category:Deciders]] | [[Category:Deciders]] | ||
Revision as of 11:46, 29 August 2025
Backward Reasoning 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
- The idea of Backward Reasoning was already used in 1989 by Heiner Marxen in "Attacking the Busy Beaver 5".[1]
- In March 2022, the decider is introduced to Busy Beaver Challenge.[1]
- 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.[1]
- In June 2022, a bug in the decider is found and fixed, leading to some less machines being marked as decided.[1]
- In October 2022, another bug is found and fixed, leading to the decider briefly being unapplied.[1]
- In August 2023, Backward Reasoning is verified in Coq (now Rocq) by meithecatte.[2]
See also
- Section 4 of bbchallenge's deciders write-up.