I/D machine Turing-completeness proof

This page contains a proof by User:ais523 that the I/D machine is Turing-complete. It does this by introducing an intermediate language, "ErrorBucket", then gives a compiler from cyclic tag to ErrorBucket and ErrorBucket to the I/D machine.
== ErrorBucket ==
ErrorBucket is a (very special-purpose, and probably not usable outside this page) esoteric programming language. It uses the following data model:
* There are five queue elements (each of which is an atom / enum value, i.e. the only thing you can do with queue elements is compare them to see if they're equal): inactive data (or d), active data (or D), inactive bucket (or b), active bucket (or B), and inactive error (or e). There's no such thing as an active error; attempting to activate an inactive error is undefined behaviour (i.e. an erroneous thing to do). There's an infinite supply of each of these queue elements (i.e. a queue can contain multiple copies of the same element, if necessary).
* There are two queues: the data queue and the bit bucket. The data queue is read/write, supporting the queue operations "push" (i.e. adding an element to the back of the queue), "peek" (i.e. looking at the element at the front of the queue, without changing the queue), "activate" (which replaces the first element of the queue with an active version, and thus requires it to not be an inactive error; this is undefined behaviour if the element is active or an inactive error), and "shift" (i.e. removing the front element of the queue without inspecting it). The bit bucket is write-only; it only supports pushes, not peeks or shifts. Both queues can contain queue elements, but nothing else.
* At any given time, there may or may not be a selected queue. It's possible either for one of the queues to be selected, or for neither queue to be selected; it is never possible for both queues to be selected at once. (This is a small amount of additional state beyond that stored in the queues.)
The initial state upon running any program is as follows:
* The active queue contains two elements: active data at the front, inactive data at the back (i.e. Dd).
* The bit bucket is initially empty (although its initial state is not really observable anyway).
* Neither queue is selected.
An ErrorBucket program consists of a sequence of commands, which are run in a loop forever. No command takes an argument, i.e. each command makes a small discrete modification to the program's state. Here are the commands:
; Activate (a)
: This command is undefined behaviour if a queue is selected. It activates the first element of the data queue; this will also be undefined behaviour, unless the element in question is inactive data or inactive bucket. An activate command must always be followed by a select command; a program is syntactically incorrect if this rule is not followed.
; Push Bucket (b)
: This command is undefined behaviour unless a queue is selected. It pushes an inactive bucket element to the end of the selected queue, then deselects the queue.
; Continue (c)
: This command is undefined behaviour if a queue is selected. It shifts and discards the first element of the data queue. This is undefined behaviour unless the data queue contains at least two elements at the time (the data queue is never supposed to become completely empty).
; Push Data (d)
: This command is undefined behaviour unless a queue is selected. It pushes an inactive data element to the end of the selected queue, then deselects the queue.
; Push Error (e)
: This command is undefined behaviour unless a queue is selected. It pushes an inactive error element to the end of the selected queue. Unlike the other "push" commands, it does not deselect the queue.
; Select (f)
: This command is undefined behaviour if a queue is selected. It peeks at the first element of the data queue; if this is inactive, it causes undefined behaviour; if it's active, it selects the corresponding queue (i.e. if the element is active data, the data queue is selected, if the element is active bucket, the bit bucket is selected).
As a special restriction (beyond the fact that each a must be followed by an f), the last few commands of the program (before it loops) must be cafdfed. (A program that does not end with this sequence of seven commands is syntactically invalid.) Of course, the programmer will need to write the program in such a way that this mandatory sequence of commands fits into the flow of their program, not causing any undefined behaviour or other unwanted effects on the program state.
== Compiling cyclic tag to ErrorBucket ==
We use the following definition of cyclic tag programs: we have a command list that is a sequence of strings of Booleans, and a storage, a queue of Booleans. (The program itself simply defines the initial states of the command list and of the storage.) Execution proceeds by performing the following steps in a loop:
# Shift the storage (i.e. remove its head element).
# If "true" was shifted this way, append a copy of the first string in the program to the tail of the storage. (If "false" was shifted, no append is done.)
# Move the first string in the program to the end.
This is well-known to be a Turing-complete construction (and is equivalent to that in Bitwise Cyclic Tag, although Bitwise Cyclic Tag has a lower-level concept of how the appending happens). We'll also add the (without-loss-of-generality) restrictions that the storage never becomes shorter than 2 elements, and that the initial value of the storage starts with "true" (you can easily cause this situation to come about by simply running the program until a state in which the storage starts with "true"; there has to be one somewhere in the initial storage or the program has no way to append to it, causing the storage to empty).
First, giving the translation without explanation (a proof that this is correct will be given subsequently):
* The very first part of the ErrorBucket program is a fixed fb.
* The next part of the ErrorBucket program represents the initial storage (minus its leading 1), encoded as follows:
** "true" becomes fdfb
** "false" becomes fbfb
* Next comes another fixed part, a single c.
* This is followed by the representation of the command list. Each string within the command list is written in order, represented as follows:
** An empty string becomes c. If the string is nonempty, its translation instead consists of a, followed by the Booleans that make up the string, followed by c. (Note that the translation of a Boolean always starts with f, fulfilling the requirement that a is always followed by f.)
** Each Boolean in the string is then encoded the same way as above:
*** "true" becomes fdfb
*** "false" becomes fbfb
** Immediately after each command comes an additional c, unless it's the last command in the program, in which case afdfed is used instead (to fulfil the requirement that the program must end with cafdfed; the leading c will be present because the encoding of every command ends in c).
So how does this work? First, we consider program initialisation. At the very start of the program, the data queue is Dd. So fx (where x is d or b) will select the data queue, push d or b accordingly onto it, and then deselect the queue, leaving everything in the same state apart from the newly pushed element. Finally, the c at the end of the initialisation removes the leading D. In other words, the eventual state of the data queue will be equal to the initial storage of the cyclic tag system, expressed as db for true or bb for false. The bit bucket's state is of course irrelevant, and no queue is selected.
We can then specify our invariant for mapping between a cyclic tag state and an ErrorBucket state; just before each cyclic tag command runs, the ErrorBucket state consists of no selected queue, with the data queue containing the cyclic tag's storage encoded using db/bb. This is clearly true post-initialisation. Meanwhile, just after the command runs, the encoding is slightly different; it consists of a leading b, followed by the same encoding as before. (This makes the purpose of the linking c that comes after each command other than the last clear; it deletes the leading b, putting the data queue back into the expected format.)
Next, we check that the compiled version of each cyclic tag command retains this invariant:
* If the command is empty, it doesn't matter what the head of the storage is; we're either appending the empty string to it or not appending the empty string to it, and both of these choices have the same result. So the only effect of the cyclic tag command is to remove the head of the storage. We do this using c; the first element of the storage corresponds to db or bb in the data queue, and c removes half of this element, leaving it as just b. So we've gone from the encoding of the storage using the no-b encoding to the encoding of the shifted version of the storage with a leading b, just as required.
* If the command is not empty, we start with a, activating the first element of the data queue (it's now D or B; note that this activation is defined because we know that the queue was nonempty and thus must have started with d or b). If the element happens to be D, then just like at the start of the program, fdfb will push db onto the data queue (the equivalent of pushing true onto the storage), and likewise fbfb will push bb and thus emulate pushing false. So in that case – where the first element of the storage was true – a copy of the command will get appended to the storage, just as required. Meanwhile, if the first element of the storage was false, meaning that we have a B at the start of the data queue, in order to emulate cyclic tag semantics we need to not append the command to the storage. The ErrorBucket program handles that by pushing all the bbs and dbs onto the bit bucket instead, which clearly has no useful effect (this is because the f will now select the bitbucket, with the subsequent b or d uselessly pushing onto it and then deselecting the bit bucket). Once we're done, the final c of the command will remove the activated D or B, leaving us with the encoding of the shifted storage preceded by b, as required.
Finally, what happens at the end of the ErrorBucket program, when it loops back round? Due to our invariant, the queue at this stage is encoded as b followed by the encoding of the storage. We then run a mandatory afdfed; the a converts the leading b to B; then fdfed will push ded onto the bit bucket (which of course has no effect). Then the preamble at the start of the program will run; there's still a B at the start of the data queue, so all the fd and fb will push d or b respectively onto the bit bucket, again doing nothing. The only remaining character before the encoding of the first command of the cyclic tag program is a c; that will remove the initial B, restoring our invariant. So the cyclic tag commands will run in sequence forever (with all the characters that aren't part of an encoding of a command doing nothing but shifting off stray b or B characters or pushing onto the bit bucket), meaning that the ErrorBucket program emulates the cyclic tag program.
== Compiling ErrorBucket to the I/D machine ==
The mechanical translation from ErrorBucket to I/D machine is first given without explanation, and then proved correct. The translation is mostly given in RLE format for readability, although the occasional translated command ends with I and thus needs to be spelled out. (It's trivial to convert the translated program into either format via run-length encoding or decoding.)
Here's the translation:
* af → 0 2
* b → 3 1 0
* c → III
* d → 3 5 0
* e → III
* f → 0 0
Before performing the translation, the program is rotated to put the cafdfed sequence that was at the end of the program to the start of the program instead. (That is, the program will always start III 0 2 3 5 0 0 0 III 3 5 0, i.e. 3 2 3 5 0 0 0 6 5 0.)
And now for the proof. First, we look at the 3 2 3 5 0 0 0 6 5 0 with which the program starts, and simply observe the effect it has at the start of the program (i.e. starting with empty RAM and the pointer at 0) by executing it:
 Address 0 1 2 3 4 5 6 7 8 9
 Command ------------------------------
 [0] 0 0 0 0 0 0 0 0 0
 3 3 0 0 [0] 0 0 0 0 0 0
 2 3 0 [0] 2 0 0 0 0 0 0
 3 3 0 3 [2] 0 0 0 0 0 0
 5 3 0 3 7 0 0 0 [0] 0 0
 0 [3] 0 3 7 0 0 0 0 0 0
 0 3 0 3 [7] 0 0 0 0 0 0
 0 3 0 3 7 0 0 0 [0] 0 0
 6 3 0 3 7 0 0 [0] 6 0 0
 5 3 0 3 7 0 [0] 5 6 0 0
 0 [3] 0 3 7 0 0 5 6 0 0
Next, we state how an I/D machine state corresponds to the ErrorBucket state:
* The I/D machine pointer corresponds to the selected ErrorBucket queue: it points to 0 if neither queue is selected, 3 if the bit bucket is selected, 7 if the data queue is selected.
* Each ErrorBucket queue element has a corresponding number in the I/D machine state:
** Inactive data (d) in ErrorBucket corresponds to a value of 5 in the I/D machine's RAM;
** Active data (D) in ErrorBucket corresponds to a value of 7 in the I/D machine's RAM;
** Inactive bucket (b) in ErrorBucket corresponds to a value of 1 in the I/D machine's RAM;
** Active bucket (B) in ErrorBucket corresponds to a value of 3 in the I/D machine's RAM;
** Inactive error (e) in ErrorBucket corresponds to a value of 0 in the I/D machine's RAM.
* The elements of the bit bucket are stored at RAM elements 10, 13, 16, 19, etc. (going up by 3 each time). RAM address 3 tracks the size of the bit bucket, always pointing to 3 cells before the first unused cell (i.e. once the bit bucket becomes nonempty, it'll point to the most recently pushed bit bucket cell). Cells which exist in this arithmetic sequence, but are "beyond the end" of the bit bucket, contain 0. The bit bucket is ordered in memory so that lower-numbered cells are towards the front of the queue.
* The elements of the data queue are stored in cells whose addresses are divisible by 3. The first cell being used for the data queue (i.e. the cell containing its head) is pointed to by RAM cell 0. The last cell being used for the data queue (i.e. the cell containing its tail) is pointed to by RAM cell 7. Cells in the sequence 6, 9, 12, 15, etc. that are to the left of the data queue can contain any value. Cells in this sequence that are to the right of the data queue always contain 0. The data queue is ordered in memory so that lower-numbered cells are towards the front of the queue.
* The remaining RAM elements are 1, 2, 4, 5, and the sequence 8, 11, 14, 17, etc.. These each have fixed values; RAM cell 2 always contains 3, the rest always contain 0.
We can see that the RAM array that exists after startup, [3] 0 3 7 0 0 5 6 0 0…, corresponds to a valid ErrorBucket state: no queue is selected (the pointer is at 0), the bit bucket is empty (because RAM element 3 points to 7), and the data queue (which goes from 3 to 6, as indicated by RAM elements 0 and 7 respectively) contains 75, i.e. active data, inactive data (or Dd). This is in fact the same state in which ErrorBucket programs need to start. As such, by the time we reach the start of the ErrorBucket program (the cafdfed is at the end, so after running its translation 3 2 3 5 0 0 0 6 5 0, the two programs will be in the same place), the two programs have the same state.
Confirming the translation is now a simple matter of confirming that the translation of each command maintains the correspondence between the states of the two languages:
;af → 0 2
:In ErrorBucket, af is defined only if the data queue starts with an inactive element (other than an error) and no queue is selected; it makes the element active, then selects the corresponding queue. So in the I/D machine program, we'll always start with the pointer at 0, and a 5 or 1 in the cell it points to. Running 0 will point the pointer at the start of the data queue; then 2 will add 2 to that (changing 5=d to 7=D, or 1=b to 3=B) and move the pointer to 7 or 3 accordingly, thus maintaining the state correspondence.
;b → 3 1 0
:In ErrorBucket, b requires a queue to be selected. So the I/D machine program has the pointer pointing to the tail of that queue. The first 3 command will point the tail three squares further right (to a 0, due to our invariant that cells beyond the right end of a queue are always zero), and then point the I/D machine pointer at the newly added element. Then the 1 will change that element to a 1 (i.e. we just pushed a b to the end of the queue in question, as required), and point the I/D machine at cell 1. Finally, 0 will dereference cell 1; it always contains 0 due to our invariant, so the I/D machine pointer moves back to cell 0, corresponding to a deselection of the queue (as required).
;c → III
:The way our correspondence is defined means that increasing cell 0 by 3 is performs the operation of shifting the data queue entirely by itself. c is only defined behaviour in ErrorBucket if no queue is selected (i.e. the I/D machine data pointer is at 0), so we know the pointer is at cell 0, and III will increase it by 3 with no other effects.
;d → 3 5 0
:This is entirely analogous for the case for b; the only difference is that we're using 5 (i.e. d), not 1 (i.e. b). Cell 5 is always maintained at 0, just like cell 1 is, so we get the pointer back to cell 0 without any trouble.
;e → III
:The e command in ErrorBucket pushes e onto the selected queue, without deselecting it. e corresponds to 0, and cells to the right of the tail of a queue are always 0. Because e is only defined on a selected queue, this means that the I/D machine pointer will be pointing to a "tail of the queue" storage element; moving the tail three cells to the right (and doing nothing else) will cause a 0 that was just beyond the right-hand end of the queue to now be considered part of the queue, effectively pushing a 0 onto the queue. We can do that with III.
;f → 0 0
:f is very similar to af, except that it leaves the first element of the queue alone rather than activating it. So the construction is the same as for af, except that we don't do the two increments on the head of the queue while we're there; we just dereference it immediately without altering it. f is only defined in ErrorBucket if the queue starts with an active element (i.e. 7 or 3 after being translated), so the pointer will end up pointing to 7 or 3 accordingly, thus selecting the appropriate queue.
Category:Proofs