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.