Running a decider from a work tape onto a work tape

⚠️ Unreviewed by Bolton

TM.applyTM is stated for a machine computing a function: its contract asks for TM.ComputesInTime and delivers Tape.HasOutput. A machine deciding a language is not a transducer — nothing is claimed about its output tape beyond cell one — so a caller that wants to run a decider inside a loop needs the same seam stated for a verdict.

That is what this file supplies. The proofs are the ones behind TM.applyTM_hoareTime and TM.applyTM_hoareTime_frame, with TM.retargetInputStarted_decidesVirtual in place of its computing counterpart.

Main results

• TM.retargetInputStarted_hoareTime_decide — the virtual-input seam, for a decider
• TM.applyTM_hoareTime_decide — the work-to-work evaluator's contract, for a decider
• TM.applyTM_hoareTime_decide_frame — the same with the disturbance framed, which is what a loop body needs in order to reset for the next call
• TM.applyTM_hoareTime_decide_space_frame — the frame taken from the source's space bound rather than its running time, which is the only version a space-bounded caller can afford

theorem Complexity.TM.retargetInputStarted_hoareTime_decide {k : ℕ} (M : TM k) {L : Language} {T : ℕ → ℕ} (hdec : M.DecidesInTime L T) (y : List Bool) : M.retargetInputStarted.HoareTime (fun (inp : Tape) (work : Fin (k + 1) → Tape) (out : Tape) => work = (M.retargetInputStartedCfg y inp).work ∧ out = (Tape.init []).move Dir3.right) (fun (_inp : Tape) (_work : Fin (k + 1) → Tape) (out : Tape) => (y ∈ L → out.cells 1 = Γ.one) ∧ (y ∉ L → out.cells 1 = Γ.zero)) (T y.length)

The virtual-input seam, for a decider. Started on the canonical entry configuration with y on the last work tape, the wrapper halts inside the source's time bound with the source's verdict on y in cell one of the real output.

theorem Complexity.TM.applyTM_hoareTime_decide {k : ℕ} (M : TM k) {L : Language} {T : ℕ → ℕ} (hdec : M.DecidesInTime L T) (y : List Bool) : M.applyTM.HoareTime (fun (inp : Tape) (work : Fin (k + 2) → Tape) (out : Tape) => (fun (i : Fin (k + 1)) => work i.castSucc) = (M.retargetInputStartedCfg y inp).work ∧ work (Fin.last (k + 1)) = parkedBlank ∧ out = parkedBlank) (fun (_inp : Tape) (work : Fin (k + 2) → Tape) (out : Tape) => ((y ∈ L → (work (Fin.last (k + 1))).cells 1 = Γ.one) ∧ (y ∉ L → (work (Fin.last (k + 1))).cells 1 = Γ.zero)) ∧ out = parkedBlank) (T y.length)

The work-to-work evaluator, for a decider. The verdict lands in cell one of the fresh last work tape, and the real output stays the parked blank tape a wipe needs.

theorem Complexity.TM.applyTM_hoareTime_decide_frame {k : ℕ} (M : TM k) {L : Language} {T : ℕ → ℕ} (hdec : M.DecidesInTime L T) (y : List Bool) (inp₀ : Tape) (hinp : Parked inp₀) (hinpSI : inp₀.StartInvariant) (H : ℕ) (hHy : y.length ≤ H) (hHT : 1 + T y.length ≤ H) : M.applyTM.HoareTime (fun (inp : Tape) (work : Fin (k + 2) → Tape) (out : Tape) => inp = inp₀ ∧ work = M.applyPre y inp₀ ∧ out = parkedBlank) (fun (inp : Tape) (work : Fin (k + 2) → Tape) (out : Tape) => inp = inp₀ ∧ out = parkedBlank ∧ ((y ∈ L → (work (Fin.last (k + 1))).cells 1 = Γ.one) ∧ (y ∉ L → (work (Fin.last (k + 1))).cells 1 = Γ.zero)) ∧ ∀ (i : Fin (k + 2)), (work i).StartInvariant ∧ (work i).head ≤ H ∧ ∀ (j : ℕ), H < j → (work i).cells j = Γ.blank) (T y.length)

The decider's evaluator, with its disturbance framed. Beyond the verdict, this records what a caller needs in order to reset for a second call: every tape's head is still within H, and every cell beyond H is still blank. Both follow from the run being T |y|-bounded and every entry tape being parked and blank past |y|.

theorem Complexity.TM.applyTM_entry_eq {k : ℕ} (M : TM k) (y : List Bool) (realInput : Tape) : { state := M.applyTM.qstart, input := realInput, work := M.applyPre y realInput, output := parkedBlank } = M.retargetInputStarted.retargetCfg (M.retargetInputStartedCfg y realInput)

The evaluator's entry configuration is the retargeted one, which is the form the window theorems are stated about.

theorem Complexity.TM.applyTM_hoareTime_decide_space_frame {k : ℕ} (M : TM k) {L : Language} {T S : ℕ → ℕ} (hdecT : M.DecidesInTime L T) (hdecS : M.DecidesInSpace L S) (y : List Bool) (inp₀ : Tape) (hinp : Parked inp₀) (hinpSI : inp₀.StartInvariant) (H : ℕ) (hHS : y.length + S y.length + 2 ≤ H) : M.applyTM.HoareTime (fun (inp : Tape) (work : Fin (k + 2) → Tape) (out : Tape) => inp = inp₀ ∧ work = M.applyPre y inp₀ ∧ out = parkedBlank) (fun (inp : Tape) (work : Fin (k + 2) → Tape) (out : Tape) => inp = inp₀ ∧ out = parkedBlank ∧ ((y ∈ L → (work (Fin.last (k + 1))).cells 1 = Γ.one) ∧ (y ∉ L → (work (Fin.last (k + 1))).cells 1 = Γ.zero)) ∧ ∀ (i : Fin (k + 2)), (work i).StartInvariant ∧ (work i).head ≤ H ∧ ∀ (j : ℕ), H < j → (work i).cells j = Γ.blank) (T y.length)

The decider's evaluator, framed by its space bound. The disturbance is bounded by the source machine's space, not by its running time: a space-bounded machine may run for exponentially many steps, and a caller that had to wipe that many cells could not stay in polynomial space.