Sync bi-counter: Difference between revisions
Jump to navigation
Jump to search
m (bold name) |
(add description of decider) |
||
| Line 9: | Line 9: | ||
* [https://bbchallenge.org/1RB1LA_1LA0RC_1RB0RD_1LE1RD_0LC0LF_---0LA 1RB1LA_1LA0RC_1RB0RD_1LE1RD_0LC0LF_---0LA] | * [https://bbchallenge.org/1RB1LA_1LA0RC_1RB0RD_1LE1RD_0LC0LF_---0LA 1RB1LA_1LA0RC_1RB0RD_1LE1RD_0LC0LF_---0LA] | ||
* [https://bbchallenge.org/1RB0LE_0LC---_1LA0RD_1RC0RC_1LF1LE_0LA1RF 1RB0LE_0LC---_1LA0RD_1RC0RC_1LF1LE_0LA1RF] | * [https://bbchallenge.org/1RB0LE_0LC---_1LA0RD_1RC0RC_1LF1LE_0LA1RF 1RB0LE_0LC---_1LA0RD_1RC0RC_1LF1LE_0LA1RF] | ||
== Decider == | |||
For typical cases, we can fold the tape so that two counters overlap as one counter, and then it's usually decidable by CTL. | |||
Inductive decider can deal with some more complex situations. | |||
Revision as of 02:03, 4 August 2024
Sync bi-counter is an informal class of Turing machines. A typical Turing machine in this class has the following behavior:
- It has two counters on the tape, and the lowest digit of both counters are adjacent.
- In each round, both of the two counters are increased by one, and they count in the same base. Both counters count to the same number after each round (i.e. they are synchronized).
Examples
- Skelet #10 (Proof of non-halt)
- 1RB1LA_1LA0RC_1RB0RD_1LE1RD_0LC0LF_---0LA
- 1RB0LE_0LC---_1LA0RD_1RC0RC_1LF1LE_0LA1RF
Decider
For typical cases, we can fold the tape so that two counters overlap as one counter, and then it's usually decidable by CTL.
Inductive decider can deal with some more complex situations.