Bell eats counter: Difference between revisions
Jump to navigation
Jump to search
m coq -> rocq |
Added TM template |
||
| (One intermediate revision by the same user not shown) | |||
| Line 8: | Line 8: | ||
== Examples == | == Examples == | ||
{{TM|1RB1RE_0RC1RD_1LA1RC_1LC---_1LF0RE_0LF0LA}} | |||
{{TM|1RB---_1RC0RA_1LD1RA_1LE0LD_0RE1RF_0RB0LF}} | |||
{{TM|1RB0LE_0RC---_1LC0RD_0RB1RA_1LF1LE_0LA1LF}} (more complex than typical ones) | |||
{{TM|1RB3LB---3RA0LA_2LA3LB4RB1RB2RA}} | |||
{{TM|1RB0RB_0RC1RB_1LD1RC_0LE0LD_1RA1LE}} | |||
[[Category:Zoology]] | [[Category:Zoology]] | ||
Latest revision as of 16:37, 26 August 2026
Bell eats counter is an informal class of Turing machines. A typical Turing machine in this class has the following behavior:
- It has both a bell and a counter on the tape.
- Increment: when the bouncer in the bell finishes a period, the counter is increased by one.
- Overflow: when the bouncer in the bell overflows, the bell eats the lowest digit of the counter (the counter is halved), and the bouncer in the bell is reset.
A Rocq proof of a kind of typical behavior doesn't halt.
Examples
1RB1RE_0RC1RD_1LA1RC_1LC---_1LF0RE_0LF0LA (bbch)
1RB---_1RC0RA_1LD1RA_1LE0LD_0RE1RF_0RB0LF (bbch)
1RB0LE_0RC---_1LC0RD_0RB1RA_1LF1LE_0LA1LF (bbch) (more complex than typical ones)
1RB3LB---3RA0LA_2LA3LB4RB1RB2RA (bbch)
1RB0RB_0RC1RB_1LD1RC_0LE0LD_1RA1LE (bbch)