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 `Test`s. 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.