Turing machine-to-Kondey(-to-Burro) Tests

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.

The Turmac compiler

This translation is implemented as a backend that reads a Turing machine description and emits the Kondey program that simulates it. (The Kondey program is then translated to Burro and executed.)

-> Tests for functionality "Run Turing Machine Program"

-> Functionality "Run Turing Machine Program" is implemented by
-> shell command "bin/burro run-turmac %(test-body-file)"

A machine is described in Turmac format. The first line is a header (its contents are ignored); each remaining line is a transition rule state, read, write, dir, newstate, where dir is L or R and a newstate of @H halts the machine. The machine starts in state S0 on a blank (all-_) tape.

The simplest machine writes a symbol, moves right, and halts. Reading the final Burro tape takes some care: the meaningful content is in the cell field of each CellStruct (the symbol written there, stored as an even number -- symbol 1 is stored as 2), while the scratch and carry cells are left holding harmless leftover "work values". Here, the single 2 (the second displayed value on the dumped tape) is the 1 we wrote:

state,read,write,dir,newstate
S0,_,1,R,@H
S0,1,_,R,@H
===> State{ tape=(... 1 2 0 1 0 [0] -1 ...), stack=(... [0] -2 ...), halt=True }

A more demanding check is a machine whose behaviour is known independently. The two-state busy beaver halts after six steps, having written four 1s onto the tape (visible below as four 2s, in the cell field of four adjacent CellStructs):

state,read,write,dir,newstate
S0,_,1,R,S1
S0,1,1,L,S1
S1,_,1,L,S0
S1,1,1,R,@H
===> State{ tape=(... 1 1 2 0 1 0 0 -1 3 2 0 3 3 [0] -1 1 2 0 3 1 0 -1 3 2 0 1 ...), stack=(... [1] -2 1 ...), halt=True }

Validating totality and determinism

The compiler above assumes that, at whatever (state, symbol) pair is actually being dispatched on, exactly one rule matches.

There are guards in the compiler to validate against such inputs.

-> Tests for functionality "Compile Turing Machine Program"

-> Functionality "Compile Turing Machine Program" is implemented by
-> shell command "bin/burro compile-turmac %(test-body-file)"

A duplicate rule for the same (state, symbol) pair is always rejected.

state,read,write,dir,newstate
S0,0,1,R,@H
S0,0,1,L,@H
???> Non-exhaustive patterns

A state that reads a symbol but not a lower-valued one (here S0 reads 1 and 2 but not the blank _) is rejected.

state,read,write,dir,newstate
S0,1,1,R,S0
S0,2,2,R,S0
???> Non-exhaustive patterns

An incomplete description is also rejected.

state,read,write,dir,newstate
S0,0,1,R,S1
S1,0,0,R,S1
???> Non-exhaustive patterns

Bisimulating Turing Machine programs, step by step

run-and-compare-turmac above can only ever check a machine that halts, since it runs both sides to completion and compares the final result. bisim-check-turmac instead compares the Turmac simulator and the compiled Burro program's decoded configuration after every step, up to a given bound, so it can also be used on a machine that never halts.

-> Tests for functionality "Bisimulate Turing Machine Program"

-> Functionality "Bisimulate Turing Machine Program" is implemented by
-> shell command "bin/burro bisim-check-turmac %(test-body-file) 50"

state,read,write,dir,newstate
S0,_,1,R,@H
S0,1,1,R,@H
===> MATCH
===> 1 steps, halted

state,read,write,dir,newstate
S0,_,1,R,S1
S0,1,1,L,S1
S1,_,1,L,S0
S1,1,1,R,@H
===> MATCH
===> 6 steps, halted

A machine that never halts can be checked too, out to the given bound:

state,read,write,dir,newstate
S0,_,_,R,S0
===> MATCH
===> 50 steps, still running

A more demanding non-halting machine: this one bounces its head back and forth over the same three tape cells forever, so the same CellStructs are dispatched from again and again, in alternating directions.

state,read,write,dir,newstate
S0,_,1,R,S1
S0,1,1,R,S1
S1,_,1,R,S2
S1,1,1,R,S2
S2,_,1,L,S3
S2,1,1,L,S3
S3,_,1,L,S0
S3,1,1,L,S0
===> MATCH
===> 50 steps, still running

(It's worth noting that the above test case did expose a genuine bug in an earlier version of the TM compiler that Claude generated. The carry cell was written with the move direction as a plain delta, on the assumption that it held 0; but the final, displacing Test that performs the move deposits into carry whatever is on the stack at that moment, and by the mechanics of the cascading conditional, this is the bumped state identifier from two visits prior. So on the third and subsequent dispatches of the same CellStruct, carry held a stale positive residue, and any transition that should have moved the head left moved it right instead. Running this program under the bisimulator revealed this problem and prompted Claude to find a fix for it, which was to launder carry before the direction is written into it, using the same swap mechanism that caused the problem in the first place.)

The most demanding machine of all is a binary counter, which counts 1, 10, 11, 100, ... upward forever over a three-symbol alphabet (blank, 0, 1). S0 sweeps right to the end of the number and turns around; S1 carries leftward, flipping 1s to 0s until it reaches a 0 or a blank, which it flips to 1. Unlike the bouncing machine above, this machine's working region grows without bound, and each cell is dispatched an unbounded number of times, in both directions, as carries ripple through it -- so it exercises the cascading conditional, the destination writes, and the carry laundering across arbitrarily many revisits of every CellStruct. This test shows that it agrees with the reference simulator at every one of the first fifty steps. I have also run it manually to 500,000 steps, and it still agrees.

state,read,write,dir,newstate
S0,_,_,L,S1
S0,0,0,R,S0
S0,1,1,R,S0
S1,_,1,R,S0
S1,0,1,R,S0
S1,1,0,L,S1
===> MATCH
===> 50 steps, still running

The cascading {...} dispatch fires the branch whose position equals the value being dispatched on, so the compiler must place each state's (and each symbol's) branch at the position matching its normalized value -- regardless of the order the rules happen to appear in the file (the Turmac format treats the rules as an unordered set). The next two machines exercise that: their rules are deliberately listed out of value order. The first lists state S0's symbol rules with 1 before the blank; reading a blank must still run the blank rule (write 2, move right), not the 1 rule:

state,read,write,dir,newstate
S0,2,2,L,@H
S0,1,1,L,S0
S0,_,2,R,S0
===> MATCH
===> 50 steps, still running

The second lists a non-start state's rules before S0's, so the start state is not the first to appear; the outer state dispatch must still select S0's block on the first step:

state,read,write,dir,newstate
S1,_,_,L,S0
S0,_,_,R,S1
===> MATCH
===> 50 steps, still running