This is a automatic proof generator for a specific subset of shift-overflow counters, showing that they all halt. It does not state how many steps they take or the sigma value of the machines when they halt, but it does say how many resets they take (which can be used to find those values if needed).
Feel free to use or repurpose however you'd like (with proper credit)
The subset of shift overflow counters it decides have a binary counter and a unary counter. The binary counters have two components, active and inactive digits. As the active digits are incremented, so are the unary counter digits. Each binary counter increment corresponds to 2 unary counter digits.
Once the active digits have reached their maximum, 3 is subtracted from the unary counter and converted into an active digit, and then an inactive digit is converted to an active one.
Once all inactive digits become active, and the final binary counter is full, the machine resets. Then it halts according to the value of the unary counter mod 3. (Either it halts at 3k, or 3k+1 and 3k+2)
These machines are characterized by the following elements:
Critical stateDirectionAdder statesUnary EscapeToggle loop on 100Toggle loop exits on encountering 11 and 0Parity loop
The critical state is just the state that has the undefined transition. This is important for the parity loop later.
The direction is which side the unary counter is on (left or right). Mathematically it makes no difference but it's important for determining the rules programmatically. The direction can be determined by finding the adder states
The adder states (which are the 3 states that comprise the step that add 2 to the end of the unary counter) are uniquely identifiable because they happen between the only two self-referential states going in opposite directions.
Example: AAAAAAABFFFFFFFF... - AB will be the adder states They follow the pattern of read(0) -> Write 1 -> read(0) -> Write 1 -> Switch direction. We can determine that the direction of the machine is the direction that the first adder state is moving.
Once 2 has been added to the unary counter, the machine has to move out of the unary counter back to the binary counter. This is the unary escape loop. This is easily detectable as it's made of a single repeating state.
The "toggle loop" is one of the most important parts of the machine. It starts once the machine has exited the unary escape step. The loop restarts as it encounters a 1, a 0, and then a second 0 toggling every bit it encounters (hence the name).
It's detectable as it's entered by the unary escape step and has to follow the 100 pattern.
The machine can exit the toggle loop in 2 ways which have very different outcomes.
If instead of encountering 100, the machine encounters 11, the machine has encountered a 0 in binary. It converts this 0 to a 1, all previous 1s into 0s, and then enters a second less important loop that eventually goes back to the adder state.
If instead of 100 it instead encounters an extra 0, the machine enters the parity loop.
The parity loop is the most important part of the machine. It's made up of 3 states. One of which reads a 0, and the other two read 1's. One of the 1 states has to be the critical state and this determines with which parity the machine halts. If the first 1 state is the critical state, the machine halts at 3k+1 and 3k+2. If it's the other, it halts at 3k.
By going through and detecting all previous steps, we can detect the states the parity loop is made up of, and thus with which parity the machine halts.
All of these machines follow the A(a, 2^n - 1, c) -> A(a + 2^n (4(4^c - 1)/3) - 3c, 2^{n+2c} - 1, 0) rule, as it is the defining rule of this class of machines. The rules that can vary, and thus we need to detect, are the reset transitions A(3k + r, 2^n - 1, 0) -> ? and the starting configuration.
Both of these can be fairly trivially found by just running the machine until it hits these states.
The starting configuration is found by running the machine until it hits a clearly defined A(a, 2^n - 1, 0). This can be found by looking at the tape, and the state the machine is in (it should be in the state that makes up the unary escape but reading a 0)
The reset transition is found by setting up a tape with 50 binary digits (to get an accurate simulation for eventual larger tapes) and some amount of unary digits (based on whether the reset happens at 3k, 3k+1, or 3k+2)
Then the machine is just run until it reaches a clearly defined A(a, 2^n - 1, c) transition in pretty much the same way as the starting configuration detector, just with the added necessity to count the amount of c digits.
A reset configuration will look like A(a, 2^n - 1, n + 2k + x) where x is some constant value. The value of c comes from the observation that the original binary digits (all n of them) are preserved, and 2 c digits are added for every 3 unary digits. Then x comes from any unusuality that may come from the reset state. In our simulation, n + 2k is artificially set up to equal 50 so we can just find x by subtracting 50.
These rules can be directly evaluated in modular arithmetic with moduli that have a large enough power of 3. I found a modulus of 3^15 * 4 to be the smallest that works for all machines.
The power of 3 has to be large because each step requires 2 divisions by 3, meaning the modulus has to be reduced by a factor of 3 after each division to be mathematically sound.
These steps are just run until the halting configuration is output, and then the machine halts.
Put the machines you want analyzed into input_file.txt. This program outputs to stdout by default. My results from running the program are in output.txt
This program is compiled with gcc and was run on windows. It doesn't use any platform or compiler specific behavior though so it should work with others.
Thank you to Shawn Ligocki for evaluating the correctness of this program's output and offering critical insight without which this would've been impossible.