Publishing a work-tape bit on the output tape

Every branching combinator in the library — TM.ifTM and TM.loopTM alike — decides on the real output tape's verdict cell. A machine that keeps its intermediate results on work tapes therefore has no way to branch on them, and the library has no subroutine that moves a bit from a work tape to the output.

TM.writeOutputBitTM is that subroutine, and it is as small as it can be: a single transition that writes the symbol under a designated work head onto the output tape, leaving every tape otherwise exactly as it was. Parked tapes stay parked, so it composes with everything.

Main results

• TM.writeOutputBitTM — publish a work-tape bit on the output tape
• TM.writeOutputBitTM_hoareTime_frame — its contract, with a full external frame
• TM.writeOutputBitTM_clears — pointed at a blank tape it clears the output, which is what the wipe subroutine requires

def Complexity.TM.writeOutputBitTM {n : ℕ} (vIdx : Fin n) : TM n

Publish the symbol under work head vIdx on the output tape, in one transition.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.TM.writeOutputBitTM_hoareTime_frame {n : ℕ} (vIdx : Fin n) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hinp : Parked inp₀) (hwork : ∀ (i : Fin n), Parked (work₀ i)) (hout : Parked out₀) : (writeOutputBitTM vIdx).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀.write (readBackWrite (work₀ vIdx).read).toΓ) 1

Publishing a bit. One transition writes the symbol under work head vIdx at the output head, leaving the input and every work tape exactly as they were and moving no head.

theorem Complexity.TM.writeOutputBitTM_clears {n : ℕ} (vIdx : Fin n) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hinp : Parked inp₀) (hwork : ∀ (i : Fin n), Parked (work₀ i)) (hout : Parked out₀) (hblank : (work₀ vIdx).read = Γ.blank) (hhead : out₀.head = 1) (hcells : ∀ (j : ℕ), j ≠ 1 → out₀.cells j = (Tape.init []).cells j) : (writeOutputBitTM vIdx).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = (Tape.init []).move Dir3.right) 1

Clearing the output needs no new machine. Pointing the publisher at a work tape whose head reads blank writes a blank to the output; if the output was only ever written at its verdict cell, that restores it to the parked blank tape the wipe subroutine demands.