UTM extraction phase: extractTM

The final phase of the universal machine copies the simulated output — stored on work tape 2 (vOut) under the +1 shift, i.e. starting at cell 2 — onto the real output tape starting at cell 1, up to and including the first □.

Behavior

From qstart:

• Phase A (rewind): move the work-tape-2 head left until it reads ▷, then right once (to cell 1). All other tapes idle.
• Phase B (step to cell 2): move the work-tape-2 head right once more, to cell 2 — the first simulated output cell under the +1 shift.
• Phase C (copy): repeatedly copy the symbol under the work-2 head to the output tape; if the symbol is □, halt (after writing it); otherwise move both heads right and repeat.

All tapes other than work tape 2 and the output are exactly unchanged (readBackWrite writes and idleDir moves); work tape 2's cells are unchanged (only its head moves).

Main definitions

• TM.extractTM — the extraction machine

Main results

• TM.extractTM_hoareTime — full Hoare-time specification: if the first m cells starting at work-2 cell 2 are non-blank and cell m + 2 is blank, the machine copies cells 2 .. m+2 of tape 2 onto output cells 1 .. m+1 within B + m + 8 steps, where B bounds the initial work-2 head.

inductive Complexity.TM.ExtractPhase : Type

Control states of extractTM.

• rewind : ExtractPhase
• toCell2 : ExtractPhase
• copy : ExtractPhase
• done : ExtractPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqExtractPhase : DecidableEq ExtractPhase

Equations

• Complexity.TM.instDecidableEqExtractPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.TM.instFintypeExtractPhase : Fintype ExtractPhase

Equations

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

def Complexity.TM.extractTM : TM 6

Copy work tape 2 (vOut) cells 2, 3, … verbatim to output cells 1, 2, …, up to and including the first □. Work tape 2 is first rewound to cell 2; its cells are preserved (write-back), and all tapes other than work-2 and output are exactly unchanged.

Equations

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

theorem Complexity.TM.extractTM_hoareTime (m B : ℕ) (inp₀ : Tape) (work₀ : Fin 6 → Tape) (out₀ : Tape) (hblank : (work₀ 2).cells (m + 2) = Γ.blank) (hnb : ∀ j < m, (work₀ 2).cells (j + 2) ≠ Γ.blank) (hwf2 : (work₀ 2).StartInvariant) (hhead2 : (work₀ 2).head ≤ B) (hhead2' : 1 ≤ (work₀ 2).head) (hout0 : out₀.cells 0 = Γ.start) (houtns : ∀ (j : ℕ), 1 ≤ j → out₀.cells j ≠ Γ.start) (houth : out₀.head = 1) (hinp : inp₀.read ≠ Γ.start) (hothers : ∀ (i : Fin 6), i ≠ 2 → (work₀ i).read ≠ Γ.start) : extractTM.HoareTime (fun (inp : Tape) (work : Fin 6 → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin 6 → Tape) (out : Tape) => inp = inp₀ ∧ (∀ (i : Fin 6), i ≠ 2 → work i = work₀ i) ∧ (work 2).cells = (work₀ 2).cells ∧ ∀ j ≤ m, out.cells (j + 1) = (work₀ 2).cells (j + 2)) (B + m + 8)

extractTM specification. Let m be the number of non-blank cells starting at work-2 cell 2 (cell m + 2 is the first blank). Then extractTM copies work-2 cells 2 .. m+2 onto output cells 1 .. m+1 (the last one the terminating □), preserving the input tape, all work tapes other than 2 exactly, and work-2's cells, within B + m + 8 steps where B bounds the initial work-2 head position.