Kondey Tests =========== Here are some test cases that can serve as a check that an implementation of Kondey is not grossly broken. These tests are written in [Falderal][] format. Each indented code block (generally preceded by a description) represents a test. All the lines of the code block up until the `===>` line give the input to be tested; the text after `===>` gives the expected output. `???>` gives an expected error message, which is permitted to be a partial (substring) match. [Falderal]: https://catseye.tc/node/Falderal Kondey ------ As mentioned in the [Burro tests](Burro-Tests.md), there is an extensional idiom for conditionals in Burro, however, obtaining and maintaining inverses for them by hand would be tiresome and error-prone. So it would be beneficial to have them be machine-generated. To that end, a facility to generate these conditional structures has been implemented. In fact, a mini-language for describing these structures, **Kondey**, has been defined, and we have implemented a compiler from Kondey to Burro. -> Tests for functionality "Compile Kondey Program" -> Functionality "Compile Kondey Program" is implemented by -> shell command "bin/burro compile-kondey %(test-body-file)" Kondey is a proper superset of Burro. Every Burro program is a Kondey program, but not vice versa. Kondey adds a conditional structure to Burro, which looks like this: {.../.../...} where each `...` is a Kondey subprogram, i.e. it is a `/`-delimited list of Kodey subprograms written inside curly braces. This conditional form maps to a Burro conditional structure following this pattern: * if the current cell is greater than 0, then execute the 1st fragment * if the current cell is greater than 2, then undo the 1st fragment and execute the 2nd fragment * if the current cell is greater than 4, then undo the 2nd fragment and execute the 3rd fragment So, we can rewrite the conditional structure shown in the "Notes" section above in a more concise and readable (such as it is) fashion: +++++ { +++++++++ / +++++++++++++ / +++++++ } -----<<< ===> +++++(+++++++++>/>)(/)--(<---------+++++++++++++>>/>)--(/)----(<<-------------+++++++>>>/>)----(/)-----<<< Once the Kondey program has been compiled to Burro, we can run the Burro, to further confirm the behaviour is what we expect. -> Tests for functionality "Compile and Run Kondey Program" -> Functionality "Compile and Run Kondey Program" is implemented by -> shell command "bin/burro run-kondey %(test-body-file)" +++++ { +++++++++ / +++++++++++++ / +++++++ } -----<<< ===> State{ tape=(... [7] ...), stack=(... [0] ...), halt=True } -> Tests for functionality "Compile Kondey Program" Kondey adds `{.../...}`, but still supports the Burro-style conditional `(.../...)`. Code that follows `(.../...)` is included in the compiled program and must not be silently dropped. -> Tests for functionality "Compile Kondey Program" + ( + / - ) + ===> +(+/-)+ -> Tests for functionality "Compile and Run Kondey Program" + ( + / - ) + ===> State{ tape=(... [0] ...), stack=(... [1] ...), halt=True } -> Tests for functionality "Compile Kondey Program" Kondey conditional forms can be nested. That was, kind of, the whole point of defining Kondey; without some syntax and some automatic translation, we would need to write these things by hand in Burro, and that's horrible and we wanted to avoid that. { +++++++++ / >>>>> { + / ++ } <<<<< / +++++++ } ===> (+++++++++>/>)(/)--(<--------->>>>>(+>/>)(/)--(<-++>>/>)--(/)<<<<<>>/>)--(/)----(<<>>>>>(/)++()++(/)(>>/>)----(/) Exiting a Conditional with the Tape Head at a Different Spot ------------------------------------------------------------ It will be useful if we can have the tape head move conditionally, that is, different branches of a conditional leave the tape head at different spots. The conditional idiom was not designed with this in mind, so there is some doubt that it supports it. What happens if we try, with the basic conditional? -> Tests for functionality "Run Burro Program" Try it with 1: + --( ++>>>>++++++++ >/ ++++ >)--(/)< ===> State{ tape=(... [4] 1 ...), stack=(... [0] ...), halt=True } Try it with 3: +++ --( ++>>>>++++++++ >/ ++++ >)< ===> State{ tape=(... 2 0 0 0 [8] -1 ...), stack=(... [0] ...), halt=True } So this seems harmless enough on its own. But will it combine well with the cascading-and-successively-undoing nature of the extensible conditional idiom? There's one way to find out... -> Tests for functionality "Compile and Run Kondey Program" Try it with 1: + { +++++++++ / +++++++++++++>>>>+++ / +++++++ } -----<<< ===> State{ tape=(... [9] 0 0 -4 ...), stack=(... [0] ...), halt=True } Try it with 3: +++ { +++++++++ / +++++++++++++>>>>+++ / +++++++ } -----<<< ===> State{ tape=(... 13 0 0 0 [3] 0 0 -2 ...), stack=(... [0] ...), halt=True } Try it with 5: +++++ { +++++++++ / +++++++++++++>>>>+++ / +++++++ } -----<<< ===> State{ tape=(... [7] ...), stack=(... [0] ...), halt=True } So... this works? It leaves different junk in the temporary cells, but since we don't care about the contents of those cells (pretty sure we don't), this... might be sufficient? Translating Turing machines to Kondey ------------------------------------- The next step is to show how we can translate an arbitrary Turing machine to a Kondey program. Our Kondey program will consist of one big loop (as befitting Burro's approach to control flow), and each iteration of that loop will simulate processing one step of the Turing machine. As mentioned (obliquely) above, each cell on the Turing machine's tape is represented by a sequence of adjacent cells on the Burro tape. We treat this sequence like a data record, and call it a _CellStruct_. A CellStruct must consist of at least: - `state`, the TM state stored locally, represented as an even integer - `tmps_1`..`tmps_n`, _n_ scratch cells for executing the conditional - `cell`, the symbol written at position on the TM tape, also represented as an even integer - `tmpc_1`..`tmpc_m`, another _m_ scratch cells for executing the inner conditional _n_ in the above is the number of states of the TM, while _m_ is the number of possible symbols in a tape cell. _k_ = _n_ + _m_ + 2 Burro tape cells are needed to store each CellStruct, and the TM instruction "Move Right" is a sequence of _k_ `>` instructions, while the TM instruction "Move Left" is a sequence of _k_ `<` instructions. Within the same CellStruct, moving from the `state` cell to the `cell` cell uses _n_ + 1 `>` instructions - and suchlike for other internal moves. For convenience we will also refer to the `start` of a CellStruct, which is the Burro cell containing the first field, which also happens to be `state`. The set of TM states is finite, as is the set of symbols that can appear on cells of the TM tape. This will allow us to work with these values with finite program structures which do not contain loops. At any point there is a current CellStruct. This is indicated by where the current Burro tape cell is. Whichever CellStruct it is inside, is the current CellStruct. The TM state exists locally in the current CellStruct, so that we may execute a conditional branch on it. But when we move to a new CellStruct, we need to copy the current state to that new cell, as it will not have the correct value. In fact, we can be more accurate and, noting that when we move to a new cell we also move to a new TM state, we need only write the new TM state into the new current CellStruct. Because the initial Burro tape consists entirely of zero-valued cells, it behooves us to represent a blank CellStruct as a sequence of four zero-valued Burro cells, so that we do not need to detect and initialize blank cells when we first encounter them. And this would in turn imply that the Turing machine must start in state 0 in our representation, and that blank Turing machine cells are represented by 0 cells in our representation. However, this runs up against a problem in the simulation, namely, that our conditional idiom works on odd values only. We can address this by storing the Turing machine cells as even numbers on the Burro tape, but bumping up the contents of the Burro tape by one (`+`) whenever we move to a new CellStruct, to ensure that they are odd when we perform tests on them, and bumping them back down (`-`) when leaving the CellStruct. This gives us a tape that is (virtually) filled with 1's initially. We need to do this even-to-odd-and-back adjustment for both the tape contents and the state kept locally in the CellStruct. Another problem this runs up against is that we do want to be able to, in a conditional, leave the tape in a different place than we started; we want to move left or right on the simulated tape. The extensible conditional idiom was not designed to handle that. The tests above suggest that it does, though, so we should move forward with it, and see. ### Pseudocode while (not halted) { (assertion: the head is at the "state" part of the current CellStruct) bump up the state id by 1, to make it odd if state == 1 { move to "cell" part of current CellStruct bump up the cell value by 1, to make it odd if cell == 1 { write new (even) value of cell (adjust 0 using +'s) move to "state" part of the CellStruct write 0 into "state" value (using -'s) move left or right to adjacent CellStruct as appropriate (assertion: the head is at the "state" part of the new CellStruct) write the new (even) state id in the "state" cell. toggle the halt flag if the new state is "halt" } elseif cell == 3 { write new (even) value of cell (adjust 0 using +'s) move to "state" part of the CellStruct write 0 into "state" value (using -'s) move left or right to adjacent CellStruct as appropriate (assertion: the head is at the "state" part of the new CellStruct) write the new (even) state id in the "state" cell toggle the halt flag if the new state is "halt" } elseif cell == 5 { .... } } elseif state == 3 { ... } elseif state == 5 { ... } } In conclusion, this is the method by which we propose that arbitrary Turing machines could be translated to Kondey, and thence to Burro, thus establishing that Burro is Turing-complete. However, we defer presenting this as an actual Turing-completeness proof until such time as the method can be vetted in a more formal and/or mechanical manner.