Strelnokoff Turing-completeness proof

We show that Strelnokoff is Turing-complete by showing how to convert
any Alternating 1-based Minsky machine to an equivalent Strelnokoff
program.
==Assumptions==
We assume that Strelnokoff variables may contain integers of unbounded
extent, including negative integers. We also adopt the interpretation
that, if the program state is such that no assignment of the program
would change it, we may consider the program to have halted.
==Approach==
We first establish some conditions and invariants under which the converted
program works.
Each counter in the A1MM is stored in one variable in the Strelnokoff
program. The value of the counter is the absolute value of the variable,
i.e. the variable may be multiplied by -1 and it still represents the
same counter value.
We will use the Strelnokoff variables A and B to store the counter
variables. (The construction may be extended to handle any finite
number of counters, but 2 is the minimum required for the A1MM to be
Turing-complete.)
During a step, the number of the step will be stored in the
Strelnokoff variable called S.
Each step consists of a counter update and a step update.
At the beginning of an odd-numbered step, all counter variables are
positive. At the beginning of an even-numbered step, all counter
variables are negative.
The counter update assignments for the step are guarded on this fact.
All counters are updated during the step, to have signs that are
opposite to what they started as.
There are also one or more step update assignments as part of the
step. They are guarded on the fact the counters all have the
opposite sign than they started with, and they update the step index.
==Construction==
Now, we give a procedure for translating each of the possible
A1MM steps to a set of Strelnokoff assignments.
For step n, there are always two cases: n is even, or n is odd.
We will only display the case where n is odd (and the counters
are initially positive). The case where
n is even can be derived by swapping the relational tests on the
guard expressions on the counters, i.e. (0 > A) instead of (A > 0).
===1. NOP===
In pseudocode the NOP semantics are:
 Sn: GOTO Sm
No change is made to the counters, but in the counter update
phase we still must update all counter variables to have the opposite sign.
 REM IF S = n AND COUNTER > 0 THEN COUNTER := -COUNTER
 A = (S = n) * (A > 0) * (0 - A) + (1 - (S = n) * (A > 0)) * A
 B = (S = n) * (B > 0) * (0 - B) + (1 - (S = n) * (B > 0)) * B
And the step update is unconditional.
 S = (S = n) * (0 > A) * (0 > B) * m + (1 - (S = n) * (0 > A) * (0 > B)) * S
===2. INCR===
In pseudocode the INCR semantics are:
 Sn: A := A + 1 ; GOTO Sm
For illustration we'll update A, and leave B unchanged, but you could of course
just as easily update B while leaving A unchanged, just swap the letters.
 REM IF S = n AND COUNTER > 0 THEN COUNTER := -(COUNTER + 1)
 A = (S = n) * (A > 0) * (0 - (A + 1)) + (1 - (S = n) * (A > 0)) * A
 B = (S = n) * (B > 0) * (0 - B) + (1 - (S = n) * (B > 0)) * B
Again, the step update is unconditional.
 S = (S = n) * (0 > A) * (0 > B) * m + (1 - (S = n) * (0 > A) * (0 > B)) * S
===3. DECR===
In pseudocode the DECR semantics are:
 Sn: IF A = 1 THEN GOTO Sm0 ELSE A := A - 1 ; GOTO Sm1
Again, we could do this with either A or B, but we'll only show it with A.
The only extra consideration on the counter update part is that we shan't
decrement the counter if it is already 1. But! We still need to negate
it if it is already 1.
 REM IF S = n AND COUNTER > 1 THEN COUNTER := -(COUNTER - 1)
 A = (S = n) * (A > 1) * (0 - (A - 1)) + (1 - (S = n) * (A > 1)) * A
 REM BUT IF S = n AND COUNTER = 1 THEN COUNTER := -(COUNTER)
 A = (S = n) * (A = 1) * (0 - A) + (1 - (S = n) * (A = 1)) * A
 B = (S = n) * (B > 0) * (0 - B) + (1 - (S = n) * (B > 0)) * B
The step update this time however is not unconditional. We update to Sm0
if the counter is 1 and Sm1 if it's not.
 S = (S = n) * (A = (0 - 1)) * (0 > B) * m0 +
 (S = n) * ((0 - 1) > A) * (0 > B) * m1 +
 (1 - (S = n) * (0 > A) * (0 > B)) * S
===Startup and Halting===
We need all counters to initially be 1 and we need to know when we've halted.
For this purpose, we will reserve step 0 to be a special initialization step.
The startup assignments will look something like this:
 A = (S = 0) * 1 + (1 - (S = 0)) * A
 B = (S = 0) * 1 + (1 - (S = 0)) * B
 S = (S = 0) * (A = 1) * (B = 1) * 1 + (1 - (S = 0) * (A = 1) * (B = 1)) * S
For halting, assigning S to a step number which isn't handled in the
program is sufficient.
Category:Proofs