Sync bouncer counter: Difference between revisions
Jump to navigation
Jump to search
No edit summary |
m (coq -> rocq) |
||
| (One intermediate revision by one other user not shown) | |||
| Line 1: | Line 1: | ||
{{Stub}} | |||
A '''sync bouncer counter''' is an informal class of Turing machines. A typical Turing machine in this class has the following behavior: | A '''sync bouncer counter''' is an informal class of Turing machines. A typical Turing machine in this class has the following behavior: | ||
| Line 4: | Line 5: | ||
* Increment: the counter is increased by one, and the bouncer finishes a period. | * Increment: the counter is increased by one, and the bouncer finishes a period. | ||
* Overflow: when the counter overflows, the bouncer changes its structure (and change back before next overflow). | * Overflow: when the counter overflows, the bouncer changes its structure (and change back before next overflow). | ||
[https://github.com/ccz181078/busycoq/blob/BB6/verify/SBCv1.v A | [https://github.com/ccz181078/busycoq/blob/BB6/verify/SBCv1.v A Rocq proof of a kind of typical behavior doesn't halt.] | ||
== Examples == | == Examples == | ||
| Line 11: | Line 12: | ||
{{TM|1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA}} (complex) | {{TM|1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA}} (complex) | ||
[[Category:Zoology]] | [[Category:Zoology]] | ||
Latest revision as of 09:05, 25 August 2025
A sync bouncer counter is an informal class of Turing machines. A typical Turing machine in this class has the following behavior:
- It has both a bouncer and a counter on the tape, and the lowest digit of the counter is adjacent to the bouncer.
- Increment: the counter is increased by one, and the bouncer finishes a period.
- Overflow: when the counter overflows, the bouncer changes its structure (and change back before next overflow).
A Rocq proof of a kind of typical behavior doesn't halt.
Examples
1RB0LF_0RC---_1RD1LE_0RE0LA_1LF0RF_0LC0LB (bbch) (most common)
1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA (bbch) (complex)