The Turing-completeness of Burro

This document was generated by Claude Opus 4.8, and it shows.

This document argues that Burro is Turing-complete, by showing that the translation from Turing machines to Kondey (and thence, via the Kondey compiler, to Burro) implemented in src/Language/Turmac/Backend/Kondey.hs is a step-for-step simulation: after k executions of the generated program's body, the Burro state encodes exactly the configuration the simulated Turing machine is in after k steps — for every k. In particular this covers the case that a weaker argument (comparing only final configurations of halting machines) cannot: a Turing machine that never halts translates to a Burro program that never halts. Without that direction, a "Turing-completeness proof" would be unsound — nothing would rule out the compiler mapping some non-terminating machine to a Burro program that merrily terminates.

The argument is a hand-written bisimulation proof in the same spirit as the group-property proof in src/Language/Burro/Definition.lhs: rigorous case analysis over the constructions involved, referring directly to the executable Haskell that implements them, but not mechanized. Its executable companion is the bisim-check-turmac command, which runs the Turmac simulator and the compiled Burro program in lockstep and compares their (decoded) configurations after every step, up to a bound — see the final section, and Tests.md.

Preliminaries

We fix a Turing machine M given as Turmac rules (see doc/Definition-of-Turmac.md), total and deterministic: for every (state, symbol) pair over M's alphabets, exactly one rule matches. (This is a genuine precondition, enforced by Language.Turmac.Validator; the Dispatch Lemma below fails without it.) The rules are normalized (Language.Turmac.Normalizer) so that states are 0..n−1 with start state 0, and symbols are 0..m−1 with blank 0. Because the cascading dispatch below selects the branch whose position equals the value being dispatched on, compileToKondey sorts each {...}'s branches into ascending value order before emitting them (the Turmac format leaves rule order unspecified, so this cannot be left to the input); the Dispatch Lemma's identification of "branch q" with state q (and symbol s with leaf s) depends on that sort. On the Burro tape these are stored doubled — state q as 2_q_, symbol s as 2_s_ — so that values at rest are even, and a transient + bump makes them odd (hence nonzero, as Burro's Test requires) during dispatch.

Each simulated tape cell of M occupies a block of K = n + m + 3 consecutive Burro cells, a CellStruct:

state | tmps_1 .. tmps_n | cell | tmpc_1 .. tmpc_m | carry

A blank Burro tape is a valid encoding of M's initial configuration: every CellStruct reads state 0 (= start state), symbol 0 (= blank), all scratch cells 0. One execution of the generated program body simulates one step of M; Burro's own repetition construct (run in Definition.lhs: re-execute the body, with the stack tape cleared and the halt flag reset to 1, for as long as ! was executed an odd number of times) provides the loop.

Two facts about exec (Test thn els) (Definition.lhs) are used throughout. Writing x for the value of the pivot (current data) cell and S for the current stack cell:

• (T1) The construct swaps x onto the stack (negating it) and swaps the old stack value into the pivot; the chosen branch then runs with the stack head one cell deeper. Afterwards the value −x is swapped back into whatever data cell the head then occupies, and the stack cell receives that data cell's old contents.
• (T2) Consequently: if the branch is position-preserving (net zero head movement), the pivot ends up holding −x and the stack cell ends up back at its old value; but if the branch displaces the head, the pivot permanently keeps the old stack value, −x lands at the displaced position, and the stack cell receives the displaced cell's old contents.

(T2) is a double-edged sword, and both edges matter below: a displacing Test contaminates its pivot with whatever was on the stack — and, used deliberately at a moment when the stack cell is known to be 0, it launders its pivot to exactly 0.

Behavior of the cascading conditional

Kondey's {a_0/a_1/.../a_{B-1}} construct is compiled by Language.Kondey.Compiler (genCond, genCondRest, makeBranch) into a chain of Tests. With the pivot cell T holding an odd value w ≥ 1, conditional j (0 ≤ j < B) is, schematically,

-^{2j} ( <^j  undo_{j-1} a_j  >^{j+1} / > )  -^{2j} ( / )

where undo_{j-1} is the Burro inverse of branch j−1's payload (empty for j = 0), and the trailing (/) is a coda that repairs the work value. Branch j's payload runs if and only if w > 2_j_; since w = 2_q_+1 is odd, the payloads that run are exactly those for j ≤ q, each undoing its predecessor, so the net payload effect is that of branch q alone. This much is the design documented in Tests.md's "Idiom for conditional execution". What we need here is an exact account of what the chain does to the cells and the stack around it. Write C_j = T+j for the j-th work cell, and S for the stack cell at the chain's own depth. Assume S = 0 when the chain starts (justified case-by-case later). By (T1)/(T2) and direct calculation:

• (C1) Dispatch is residue-independent. Conditional j tests the value w − 2_j_, where w is the value the coda of conditional j−1 re-established in C_j. Tracing one conditional-plus-coda pair: conditional j deposits −(w−2_j_) into C{j+1}, its coda subtracts 2_j more (yielding −w, reliably negative, so the coda's own Test takes its no-op branch) and swap-restores C{j+1} := _w. So the tested values are w, w−2, w−4, ... regardless of what the work cells held beforehand.
• (C2) Interior work cells keep their old contents. The old value of C{j+1} (call it ρ) is swapped onto the stack by conditional _j, held there across the coda, and swapped back into_ C{j+1} by conditional _j+1's own pivot swap, where it then stays. So after the whole chain, C_1 .. C{B-1}_ hold exactly what they held before. (In particular, junk parked in an interior work cell is preserved but never influences dispatch* — by (C1).)
• (C3) The pivot is zeroed; the last work cell receives w; the old last-work-cell value is left on the stack. Conditional 0's pivot swap puts S = 0 into T, and nothing writes T again (payloads that touch T do so from this 0 base, and undo/redo pairing leaves only the fired payload's effect). The final coda leaves C_B := w and S := (old contents of C_B). This last clause — the chain exports the previous residue of its last work cell onto the stack — is easy to overlook, and overlooking it caused a real bug, described below.

Note what (C3) does not say: it does not say S ends at 0. A chain whose last work cell held junk ρ leaves ρ sitting in the stack cell at its own depth. Within the same body execution, anything that later displaces a Test at that depth will, by (T2), absorb ρ into its pivot.

The generated program body

compileToKondey emits, per body execution (= per TM step), with the data head starting at the current CellStruct's state cell:

1. + — bump state odd (2_q_ → 2_q_+1).
2. An outer chain {p_0/.../p_{n-1}} dispatching on state; payload p_q (compilePhase1State) moves to cell, bumps it odd, runs an inner chain {l_{q,0}/.../l_{q,m-1}} dispatching on cell, and moves back — position-preserving.
3. Leaf l{q,s}_ (compilePhase1Symbol), with the head on cell, all position-preserving:
   • writes the new symbol 2_s_′ into cell as a delta;
   • reaches to the destination CellStruct's state cell and writes the new state 2_q_′ there as a delta (writeNewStateAtDest), omitted when the transition halts;
   • launders carry (see below) and writes the move direction ±1 into it as a delta;
   • executes ! — except when the transition enters the halt state, in which case the halt flag is left alone and Burro's run loop stops after this body execution.
4. Recenter; move to carry; one final displacing Test (phase2Move): pivot carry = +1 moves the head one CellStruct right, −1 one CellStruct left, overshooting the destination state cell by one on purpose so that (T2)'s −x deposit lands in a scratch cell (tmps_1 of the destination) rather than on the state; a uniform < then lands the head on the destination's state cell.

The Encoding Relation

Let B be a Burro data tape with head position aligned to a CellStruct boundary (position hK for some integer h), and let C be a configuration of M (tape contents, head position, state, halted flag). Say B encodes C when:

• (E1) C's head position is h.
• (E2) For every tape index i, CellStruct i's cell field holds 2·(symbol at i in C) — with never-visited Burro cells reading 0 = blank, matching M's blank tape.
• (E3) If C is not halted, CellStruct h's state field holds 2·(state of C).
• (E4) The state field of every CellStruct that the encoded computation may later arrive at holds either its correct pending value (the destination just written by writeNewStateAtDest) or 0 (never dispatched, or zeroed on departure per (C3)).
• (E5) carry of any CellStruct holds a value ≥ −1. (This is the launder gadget's precondition; see below.)

The initial Burro state (blank tape, position 0) encodes M's initial configuration: (E1)–(E4) read all zeros; (E5) holds trivially.

The Dispatch Lemma

If the body executes from a state encoding a non-halted C, the outer chain's net payload effect is that of p_q, and within it the inner chain's net payload effect is that of leaf l{q,s}, where (_q, s) are exactly C's current state and scanned symbol.

By (E3) and the bump, the outer pivot holds w = 2_q_+1; by (C1) the chain's dispatch depends only on w; totality and determinism of M guarantee the chain has exactly one branch per state, so branch q is the last whose payload fires, and undo/redo pairing cancels the others. (Totality earns its keep here: a missing branch would make the whole chain a silent no-op — the halt flag would never be toggled and the Burro program would quietly stop, with no error, one step early. A duplicate branch would be unreachable dead code, since dispatch is by cumulative thresholds. Neither failure announces itself at run time, which is why the validator checks the precondition statically.) The stack cell at the outer chain's depth is 0 because the body has just begun and run cleared the stack. The same argument applies one level down: the inner pivot holds 2_s_+1 by (E2) and the bump; the stack cell at the inner chain's depth is 0 because the only deeper stack activity so far was inside earlier outer payloads, all of which were exactly undone by their successors' undo prefixes (Burro's group property, proven in Definition.lhs, guarantees the undo restores the stack as well as the data tape). ∎

The carry contamination, and the launder gadget

Before stating the step lemma, we must deal with the one place where the constructions above interact badly — found not by inspection but by running bisim-check-turmac on eg/bouncing-infinite.turmac, and worth recording precisely because it is exactly the kind of error this document exists to rule out.

By (C3), the outer chain ends with the stack cell at depth 0 holding the old contents of its last work cell tmps_n — which, from the second visit to a CellStruct onward, is the bumped state identifier 2_q_″+1 left there by the previous visit's chain. The final move (phase2Move) is a displacing Test at that same depth, so by (T2) its pivot — carry — permanently absorbs that stale positive value. An earlier version of the compiler then wrote the next visit's direction into carry as a plain delta, assuming it held 0. First and second dispatches of a CellStruct: fine (the residue chain hasn't cycled yet). Third and later dispatches: carry = 2_q_″+1 ± 1, which is ≥ 0 whatever the direction — so every left-move became a right-move (or, when it summed to exactly 0, no move at all). The two halting machines the compiler had been tested on never dispatch any CellStruct three times, so final-state comparison passed; the per-step check on a bouncing machine caught it at step 8.

The fix uses (T2)'s good edge. In the leaf, before the direction is written, the head is moved to carry and the gadget

++ ( < / )

is executed. The leaf runs at stack depth 2 (inside the outer Test's frame and the inner Test's frame), and the stack cell there is 0: the stack was cleared when the body began, and the only depth-2 activity in a body execution is the leaves themselves, whose effects between branches are exactly undone by the cascade's own undo prefixes. The ++ makes the pivot 2 + (residue) ≥ 1 > 0 — by (E5) the residue is never below −1 (it is 0 initially, a bumped state ≥ 1 thereafter, or −1 from phase2Move's overshoot deposit in the one-scratch-cell case n = 1) — so the < branch always fires, the head lands one cell left on tmpc_m, and by (T2): carry := (stack cell) = 0, and the garbage 2 + residue is parked (negated) in tmpc_m. The subsequent delta then sets carry := ±1 exactly.

Parking garbage in tmpc_m is sound: tmpc_m is the inner chain's last work cell, so by (C3) its contents never influence dispatch — they are merely exported to the stack cell at the inner chain's depth, which nothing displaces at, and which the next body execution clears. (This is also why the launder gadget cannot be hoisted out of the leaf to the top of the body, where the stack cell is also 0: a displacing Test at depth 0 there would launder carry but export tmpc_m's garbage into the depth-0 stack cell, which the outer chain is just about to swap into state — precisely the kind of contamination we are eliminating. At depth 2 the exported garbage lands somewhere provably inert.)

The Step Simulation Lemma

Let B encode a non-halted configuration C, and let C′ be the configuration after one step of M (per Language.Turmac.Simulator's step). Then executing the body once from B (with fresh stack and halt flag, as run provides) yields B′ encoding C′, and the halt flag afterwards is 1 (stop) iff C′ is halted.

Proof sketch, by the Dispatch Lemma reducing everything to the single leaf l{q,s} for _C's actual (state, symbol):

• (E2′) The inner chain's pivot swap zeroes cell (C3, with the depth-1 stack cell 0), and the leaf's delta writes 2_s_′ onto that 0. Other CellStructs' cell fields: untouched. Matches step's writeSymbol.
• (E3′/E4′) The outer chain zeroes this CellStruct's state (C3, depth-0 stack cell 0) — establishing the departure half of (E4) — and the leaf's writeNewStateAtDest writes 2_q_′ as a delta onto the destination's state, which is 0 by (E4). Matches step's state update. (On a halting transition nothing is written and (E3) is vacuous for C′.)
• (E1′) The leaf launders and sets carry := ±1 (previous section); phase2Move therefore moves the head exactly one CellStruct in the transition's direction, and the overshoot-plus-< lands it on the destination's state cell, K·(±1) from where it started. Matches step's moveInDir.
• (E5′) phase2Move re-contaminates carry with the depth-0 stack value, which by (C3) is tmps_n's old contents: 0 or a bumped state ≥ 1, or (only when n = 1, where tmps_1 doubles as the overshoot cell) an arrival deposit ∓1 — in every case ≥ −1, re-establishing (E5) for the next visit. The overshoot deposit itself lands in the destination's tmps_1, an interior work cell, harmless by (C2)/(C1).
• Halt flag: the leaf executes ! exactly when the transition does not halt; run starts each body execution with the flag at 1; so the flag ends 0 (continue) iff C′ is live. Matches step's halted update. ∎

Theorem, and both corollaries

Theorem (bisimulation). For every k ≥ 0: if M runs for k steps from its initial configuration reaching C_k (without halting earlier), then k body executions of the compiled Burro program from the initial state reach a state B_k encoding C_k, with the halt flag after the k-th execution indicating exactly whether C_k is halted.

Proof. Induction on k. Base case: the blank Burro state encodes the initial configuration (above). Inductive step: the Step Simulation Lemma. ∎

Corollary 1 (halting). If M halts after exactly k steps, the compiled Burro program's run loop executes its body exactly k times and then stops, in a state whose cell fields spell out M's final tape. (This is what run-and-compare-turmac checks, machine by machine.)

Corollary 2 (non-halting). If M never halts, then for every k the k-th body execution ends with the halt flag at 0, so run loops again: the compiled Burro program never halts, and moreover at every step of its infinite run it encodes precisely the configuration M is in. A non-terminating computation is simulated as a non-terminating computation — not merely "undefined behavior".

Since a Turing machine can be given that carries out any effective computation, and the translation above turns any (total, deterministic) such machine into a Burro program that simulates it step for step, halting exactly when it halts, Burro is Turing-complete.

Epistemic status

Like the group-property proof in Definition.lhs, this is a careful but hand-written argument, not a mechanized one, and the history recounted in the carry-contamination section is a caution against overconfidence: the previous version of this translation was believed correct on the strength of an informal argument plus two passing tests, and was wrong. Three things back this document up executably:

• run-and-compare-turmac — final-configuration agreement on halting machines;
• bisim-check-turmac — per-step agreement, on halting and non-halting machines alike (bounded, since the halting problem is what it is), directly exercising the Theorem and Corollary 2 on eg/infinite-loop.turmac and eg/bouncing-infinite.turmac;
• Language.Turmac.Validator — static enforcement of the totality and determinism precondition the Dispatch Lemma depends on.

These are spot checks, not proofs; they can refute this document (as an earlier bisim-check-turmac run refuted its predecessor's assumptions) but not confirm it. The claims most deserving of future scrutiny are the stack-freshness assertions (depth 0, 1, 2 all reading 0 at the moments claimed) and the garbage-tolerance of tmps_1, interior work cells, and tmpc_m, since those are exactly the kind of bookkeeping the previous error hid in.