Tree @master (Download .tar.gz)
How-the-Turmac-to-Kondey-Backend-Works.md @master — view markup · raw · history · blame
How the Turmac-to-Kondey backend works
This document was generated by Claude Opus 4.8, and it shows.
This is a walkthrough of src/Language/Turmac/Backend/Kondey.hs, the module
that turns a Turing machine into a Kondey program. It is a companion to
doc/Turing-completeness-of-Burro.md, but the two have different jobs:
- that document proves the translation is correct (it is a dense bisimulation proof);
- this document just explains how the code works, one piece at a time, so you can read the module without holding the whole proof in your head.
I assume you're comfortable with brainfuck, with Burro (especially its
(a/b) conditional and its group/inverse property), with Turing machines,
and with what Turing-completeness means. I do not assume you can juggle
six moving parts at once — so every section ends where it began, and the
diagrams are the part you should actually read.
There is only one hard rule in this whole design, and almost every decision in the module is a consequence of it. I'll state the representation first, then that rule, then watch the rest fall out.
The pipeline, in one picture
The compiler is one stage in a small pipeline:
Turmac text ──normalize──▶ IR tree ──▶ Kondey text ──▶ Burro
(a TM, as a ▲
rule table) │
THIS MODULE
(Kondey.hs: IR ──▶ Kondey)
We only care about the one boxed stage. Everything to its left (parsing the
.turmac rule table, renumbering states/symbols so they're 0,1,2,…) is
already done; the module receives a clean IR tree shaped exactly like the
machine:
Program
└─ CondState -- "dispatch on the current state"
0 → CondSymbol -- "in state 0, dispatch on the symbol"
0 → WriteMoveGoto … -- write a symbol, move, go to a state
1 → WriteMoveGoto …
1 → CondSymbol
0 → WriteMoveGoto …
…
The module's whole task is to emit Kondey text that, when run once, performs
one step of that machine. It does not write the loop. Burro supplies the
loop for free: its run construct re-executes the program body, over and
over, until a halt flag says stop.
┌──────────────────────────────────────────┐
│ Burro's run loop │
│ │
│ ┌─────────────────────────────┐ │
│ │ the compiled program body │ ◀──┐ │
│ │ = exactly one TM step │ │ │
│ └─────────────────────────────┘ │ │
│ │ │ │
│ halt flag set? ── no ────────────┘ │
│ │ yes │
│ ▼ │
│ stop │
└──────────────────────────────────────────┘
So: read this module as "how do I do one TM step in Burro?" The looping, the halting, the not-halting — those are Burro's problem, and the module only has to nudge the halt flag correctly.
The representation: one TM cell = one "CellStruct"
Here is the central idea. Each cell of the TM's tape is represented by a fixed-size run of consecutive Burro cells, called a CellStruct:
┌───────┬──────────────────┬──────┬──────────────────┬───────┐
│ state │ tmps_1 .. tmps_n │ cell │ tmpc_1 .. tmpc_m │ carry │
└───────┴──────────────────┴──────┴──────────────────┴───────┘
0 1 .. n n+1 n+2 .. n+m+1 n+m+2
where n = number of TM states and m = number of TM symbols. The whole
struct is K = n + m + 3 Burro cells wide. Only two of those fields hold
"real" data:
state— the TM state (only meaningful in the CellStruct the head is currently inside);cell— the TM symbol written on this tape square.
The rest are workspace:
tmps_*— scratch cells the state-dispatch cascade walks through;tmpc_*— scratch cells the symbol-dispatch cascade walks through;carry— a one-cell relay used to carry the move direction out of the dispatch (more on this later).
Now the insight that makes the whole scheme cheap:
There is no "head position" stored anywhere. The TM's head is simply whichever CellStruct the Burro tape head is currently sitting inside.
Picture the Burro tape as a row of CellStructs, with the Burro head parked in one of them:
… ┌───────────┐ ┌───────────┐ ┌───────────┐ ┌───────────┐ …
│ CellStruct│ │ CellStruct│ │ CellStruct│ │ CellStruct│
│ (cell-1) │ │ (cell 0) │ │ (cell+1) │ │ (cell+2) │
└───────────┘ └───────────┘ └───────────┘ └───────────┘
▲
Burro head here
= TM head is on tape cell 0
Moving the TM head one square left or right just means moving the Burro head
one whole CellStruct (K cells) left or right.
And there's a lovely bonus: a blank Burro tape (all zeros) is already a
valid starting configuration. Every CellStruct reads state = 0,
cell = 0, all scratch = 0 — i.e. "the TM is in state 0, this square is
blank." That's exactly the TM's initial configuration, so the compiler emits
no initialization code at all.
Numbers are stored doubled (the even/odd trick)
One small convention, needed before we go further. State and symbol values
are stored doubled: TM state q is stored as 2q, symbol s as 2s.
So at rest, state and cell always hold even numbers (0, 2, 4, …).
Why? Because to dispatch on a value we run it through Burro's Test, and
Test can only tell "positive vs. non-positive" — it needs a nonzero value,
and the cascade that follows counts down by 2s. So right before dispatching,
the code bumps the value up by one with a single +, turning 2q into the
odd number 2q+1. After dispatch it's restored to even.
at rest: state = 2q (even)
bump +: state = 2q+1 (odd) ── now dispatchable
dispatch runs, then it's put back to even
Keep this in the back of your mind: even = data lying at rest, odd = a value mid-flight through a conditional.
The one hard rule
Everything above is representation. Here is the single constraint that dictates the shape of the emitted code:
Inside a
{a/b/c/…}dispatch, no branch may move the tape head (on net). Every branch must return the head to where it started.
Why? Recall how Kondey's extensible conditional is built (see
Language.Kondey.Compiler): it's a cascade of Burro Tests that walks
rightward, one scratch cell at a time. Each Test leaves a "work value" in
the next cell for the following Test to read:
{branch0 / branch1 / branch2} compiles to, roughly:
Test──▶ work ──▶ Test──▶ work ──▶ Test──▶ …
(reads in (reads in (reads
cell C) cell C+1 cell C+1) C+2 cell C+2)
The cascade only stays in sync if, after each branch's payload runs, the head
is back on the cell the next Test expects. If some branch displaced the
head — even by one cell — every following Test would read the wrong cell,
and later branches would fire (or not) at random.
So: a dispatch branch may compute and write all it likes, but it must leave the head exactly where it found it. Hold onto this. The next three sections are all just "…and here's how we obey that rule."
What one TM step has to do
A single TM transition — "in state q reading symbol s, write s′, move
direction d, go to state q′" — breaks into five jobs:
1. read the current state (q) ┐ figure out *which*
2. read the current symbol (s) ┘ transition applies
3. write the new symbol s′ into this cell
4. write the new state q′ into the *destination* cell
5. move the head one square in direction d
(plus: keep Burro's loop going, unless we're halting)
Now line these up against the one hard rule. Jobs 1–4, and the halt-flag nudge, are all things we can do without a net head move: read a value, write a delta here, reach over to a neighbor and reach back. But job 5, the move, is inherently a net head displacement — it is the one thing the rule forbids inside a dispatch.
That tension is the entire architecture. The module splits the step into two phases:
┌─ PHASE 1 ──────────────────────────────────┐ ┌─ PHASE 2 ─────────┐
│ Identify (state, symbol) via nested │ │ Do the one move, │
│ dispatch, and do jobs 3, 4, and the halt │ │ as a single 2-way │
│ nudge — all net-zero head movement. │ │ Test. (job 5) │
│ Also: stash the move direction in `carry`. │──▶│ │
└─────────────────────────────────────────────┘ └───────────────────┘
Phase 1 lives entirely inside the dispatch and obeys the rule. Phase 2 is the last thing the body does — nothing is chained after it — so it's finally safe to move the head. Let's take them in turn.
Phase 1: find the leaf, do the writing
Phase 1 is a nested dispatch: an outer {…} on the state, and inside each
state's branch, an inner {…} on the symbol. Reaching the inner-inner leaf
means we've identified the exact (state, symbol) pair — i.e. exactly which
transition applies.
Three functions build it. Read them as an outline:
compileToKondey— the outermost frame: bump the state, emit the outer state-dispatch, then hand off to phase 2.compilePhase1State— one branch of the state-dispatch: walk over tocell, bump it, emit the inner symbol-dispatch, walk back.compilePhase1Symbol— one leaf: the actual transition work.
Head movement in phase 1
The thing to watch is the head, so here's its whole journey through phase 1,
drawn inside one CellStruct (using n=2 states, m=2 symbols, so
K = 7):
┌───────┬────────┬────────┬──────┬────────┬────────┬───────┐
│ state │ tmps_1 │ tmps_2 │ cell │ tmpc_1 │ tmpc_2 │ carry │
└───────┴────────┴────────┴──────┴────────┴────────┴───────┘
start: head on `state`
│
│ compileToKondey: `+` bump state to odd
│ emit outer {…} dispatch on state ───────────────┐
│ │
▼ (inside the matching state branch — │
compilePhase1State:) │
`>>>` move to `cell` (n+1 = 3 cells right) │
`+` bump cell to odd │
emit inner {…} dispatch on symbol ──────┐ │
▼ │
(inside the matching symbol branch — │
compilePhase1Symbol: the leaf. see below) │
│ │
`<<` recenter over inner branches ◀──────┘
`<<<` move back to `state` │
◀───────────────────────────────────────────────────┘
│ `<<` recenter over outer branches
▼
head back on `state` — net zero. ✔
Every step out is matched by a step back. The two "recenter" moves (<< each)
undo the rightward drift the cascades leave behind (recall: each cascade walks
one cell right per branch). The upshot: phase 1 as a whole returns the head
to state, obeying the rule.
What the leaf actually does (compilePhase1Symbol)
Now zoom into the leaf, where we know the transition is "write s′, move d,
go to q′." The head is parked on cell. Four actions happen, each carefully
net-zero:
-
Write the new symbol. Emit
s′(doubled) as a plain+/-delta intocell. This is safe because Burro'sTesthas just freshly resetcellto 0 before the leaf runs, so a delta writes an absolute value. -
Write the new state at the destination (
writeNewStateAtDest). Reach out to the neighbor CellStruct we're about to move into — one whole CellStruct left or right, per directiond— writeq′(doubled) as a delta into itsstate, and reach back. Safe because an unvisited CellStruct always hasstate = 0. Skipped entirely if the transition halts — there's no next state to store, and Burro stops before that neighbor would ever be read.this CellStruct destination CellStruct ┌──────┬─────┐ ┌───────┬─────┐… │ cell │ … │ ────▶ │ state │ … │ … write q′ here, reach back └──────┴─────┘ └───────┴─────┘
-
Stash the move direction in
carry. Reach over to this CellStruct'scarryand write+1(move right) or-1(move left). Phase 2 will read it. (There's a subtlety here — the++(</)"launder" gadget you'll see in the code — which we defer to its own section below; ignore it for now.) -
Nudge the halt flag. Emit
!to keep Burro's loop going — unless this transition enters the halt stateH, in which case emit nothing, so the flag stays set and Burro stops after this body execution.
All four reach-and-return, so the leaf is net-zero, so the inner dispatch is net-zero. Good.
Why the writes don't get scrambled by all the other branches
Here's the part that feels like magic but is just Burro's group property. In a
cascade, it's not only the matching branch that runs — every branch up to the
matching one runs its payload, and each one first undoes its predecessor
using Burro's exact inverse. So all the spurious writes to cell, to
destinations, to carry, and all the spurious ! toggles from non-matching
branches, cancel out in inverse/redo pairs. What survives is exactly the one
leaf that logically fired. You get to write each branch as if it were the
only one; the cascade's undo machinery collapses them to the real one.
Phase 2: the one real move
After phase 1, the head is back on state, and carry holds +1 or -1.
compileToKondey now walks right to carry and emits the move
(phase2Move):
( >>…> / <<…< )
^^^^ ^^^^
then else
carry > 0 carry < 0
move RIGHT move LEFT
one struct one struct
This is a plain 2-way Burro Test on carry. Two things make it legal to
move the head here, where it was forbidden before:
- It's a 2-way
Test, not a cascade. A 2-wayTestnever re-reads its pivot, so there's no following comparison to knock out of sync. - It's the very last thing in the body. Nothing is chained after it, so its head displacement can't corrupt anything downstream.
So this is the single sanctioned head move — exactly job 5 — and it moves the head one whole CellStruct in the transition's direction.
The overshoot-by-one trick
One detail. Burro's Test has a quirk: after the chosen branch runs, it swaps
a value back onto the tape at wherever the head ended up. If a branch of
phase2Move landed precisely on the destination's state cell, that swap
would clobber the q′ we so carefully wrote there in phase 1.
The fix: each branch deliberately overshoots the target state cell by one,
landing on a harmless scratch cell of the destination. The Test's swap-back
then splats onto that scratch cell instead of onto state. Then
compileToKondey emits one uniform < to step back onto state:
phase2Move lands here (one past state) ─┐
▼
destination CellStruct: ┌───────┬────────┬─ …
│ state │ tmps_1 │
└───────┴────────┘
▲ swap-back clobbers this
final `<` steps │ (a scratch cell — harmless)
back onto state ──┘
As a bonus, because this displacing Test's swap-back lands at the
destination rather than back on carry, it leaves carry reset to 0, ready
for next time. (Mostly. See the next section for the "mostly.")
The carry wrinkle: why ++(</) is in the code
You can skip this on a first read. It's a correctness patch for a subtle bug, not part of the main idea — but it's staring at you in the emitted code, so here's what it's for.
The problem: carry is not reliably 0 when phase 1 goes to write the
direction into it. On the third-and-later visit to the same CellStruct, the
displacing Test of phase 2 (via that swap-back quirk again) has deposited
stale junk into carry — specifically an old, always-positive value left over
from a previous visit. If phase 1 then just wrote the direction as a delta
onto that junk, -1 could come out ≥ 0, turning every intended left move
into a right move (or no move). This actually happened; it was caught by
bisim-check-turmac on eg/bouncing-infinite.turmac at step 8. Two earlier
test machines never visited any cell three times, so it stayed hidden.
The fix is the gadget ++(</), emitted in the leaf just before the direction
is written. It uses the same swap-back quirk deliberately, to launder
carry back to exactly 0:
++makescarryreliably positive (the junk is provably≥ -1, so+2makes it≥ 1);(</)is a displacing 2-wayTestwhosethenbranch steps one cell left. Because the head displaces, theTest's swap-back deposits the stack value — which is provably 0 at this depth — intocarry.
Net effect: carry := 0, the garbage is dumped into a scratch cell that
provably never matters, and the following delta writes a clean ±1. (The full
argument for why the stack cell is 0 here, and why the discarded garbage is
inert, is in Turing-completeness-of-Burro.md — that's the proof's job.)
End to end: write-one compiled
To make it concrete, here's the smallest real machine.
eg/write-one.turmac is a single rule:
state,read,write,dir,newstate
S0,_,1,R,H -- in state 0 reading blank: write 1, move right, halt
It has n = 1 state and m = 2 symbols (_ and 1), so K = 6:
┌───────┬────────┬──────┬────────┬────────┬───────┐
│ state │ tmps_1 │ cell │ tmpc_1 │ tmpc_2 │ carry │
└───────┴────────┴──────┴────────┴────────┴───────┘
0 1 2 3 4 5
Running burro compile-turmac eg/write-one.turmac gives (annotated):
+ phase 1: bump `state` odd, then dispatch on state…
{>> outer {…}, branch for state 0:
`>>` move to `cell` (offset 2)
+ bump `cell` odd, then dispatch on symbol…
{++ inner {…}, branch for symbol 0 (blank):
`++` write new symbol 1 (doubled = 2) into cell
(new state is H, so writeNewStateAtDest emits nothing)
>>> move to `carry` (3 cells right of cell)
++(</) launder `carry` to 0
> step back to `carry`
+ write direction +1 (move right) into carry
<<< move back to `cell`
(halting, so no `!` — Burro will stop)
} end inner dispatch
< recenter over inner branch
<< `<<` move back to `state`
} end outer dispatch
< recenter over outer branch
>>>>> phase 2: walk to `carry` (offset 5)
(>>/<<<<<<<<<<) the move: carry>0 → right; here overshoot by `>>`
< step back onto the destination's `state`
Run this once and Burro is left with cell = 2 (symbol 1) in the original
CellStruct and the head sitting one CellStruct to the right — and because we
never emitted !, the halt flag stays set and run stops. One step, one
halt, done. Exactly the machine.
Cheat sheet
Keep this next to the code:
The CellStruct (K = n + m + 3 Burro cells; n states, m symbols):
┌───────┬──────────────────┬──────┬──────────────────┬───────┐
│ state │ tmps_1 .. tmps_n │ cell │ tmpc_1 .. tmpc_m │ carry │
└───────┴──────────────────┴──────┴──────────────────┴───────┘
state,cell— real data, stored doubled (even at rest, bumped odd to dispatch).tmps_*,tmpc_*— scratch for the state / symbol dispatch cascades.carry— relay holding the move direction (+1/-1) between phases.- TM head position = which CellStruct the Burro head is in. Blank tape = valid start state, no init needed.
Offsets (cellOffset, carryOffset, cellStructSize in the module):
state = 0 cell = n+1 carry = n+m+2 width K = n+m+3
The one rule: inside a {…} dispatch, no branch may move the head on net.
The two phases (per TM step = per body execution):
Phase 1 compileToKondey / compilePhase1State / compilePhase1Symbol
nested {state}{symbol} dispatch, all net-zero:
• write new symbol into `cell`
• write new state into the destination CellStruct
• launder + set `carry` to the move direction
• toggle `!` (unless halting)
Phase 2 phase2Move
one 2-way Test on `carry`: move the head one CellStruct,
overshoot by one, then a uniform `<` back onto `state`.
Whom to blame for what: this document explains the mechanism;
Turing-completeness-of-Burro.md proves it's correct; bisim-check-turmac
checks it step-by-step on real machines.