Documentation

Complexitylib.Models.TuringMachine.Combinators.Apply

Running a machine from a work tape onto a work tape #

A loop body cannot compute into the real output tape — it is one-way, so it cannot serve as scratch across iterations. TM.retargetInputStarted reads a machine's input off a work tape and TM.retargetOutput writes its output onto a fresh one; composing them gives TM.applyTM, a work-to-work evaluator, and composing their Hoare rules gives its contract.

Main results #

source
def Complexity.TM.applyTM {k : ℕ} (M : TM k) :
TM (k + 2)

Work-tape-to-work-tape evaluation. applyTM M : TM (k + 2) reads the source machine's input off work tape k, runs M on it, and leaves the result on work tape k + 1; the real input and output tapes are untouched.

Work tapes 0, …, k-1 are M's own scratch, so a caller that runs applyTM M more than once has to restore them between calls — that is what the precondition below demands.

Equations
Instances For
    source
    def Complexity.TM.applyPre {k : ℕ} (M : TM k) (y : List Bool) (realInput : Tape) :
    Fin (k + 2) → Tape

    The tapes applyTM M expects at entry: M's scratch blank, the virtual input holding y, the result tape blank.

    Equations
    Instances For
      source
      theorem Complexity.TM.applyTM_hoareTime {k : ℕ} (M : TM k) {f : List Bool → List Bool} {T : ℕ → ℕ} (hcomp : M.ComputesInTime f 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) => (work (Fin.last (k + 1))).HasOutput (f y) ∧ out = parkedBlank) (T y.length)

      The contract of the work-to-work evaluator. Given M's own time bound, applyTM M halts within that bound with f y on its result tape — provided M's scratch tapes were blank, work tape k held y, and the result tape was blank.

      source
      theorem Complexity.TM.applyPre_spec {k : ℕ} (M : TM k) (y : List Bool) (realInput : Tape) :
      (fun (i : Fin (k + 1)) => M.applyPre y realInput i.castSucc) = (M.retargetInputStartedCfg y realInput).work ∧ M.applyPre y realInput (Fin.last (k + 1)) = parkedBlank

      The entry tapes do satisfy the entry condition.

      source
      theorem Complexity.TM.applyTM_idlesInput {k : ℕ} (M : TM k) :
      M.applyTM.IdlesInput

      The work-to-work evaluator reads its input from a work tape, so it idles the real input head.

      source
      theorem Complexity.TM.applyPre_head {k : ℕ} (M : TM k) (y : List Bool) (realInput : Tape) (i : Fin (k + 2)) :
      (M.applyPre y realInput i).head = 1

      Every entry tape of the work-to-work evaluator is parked at cell 1.

      source
      theorem Complexity.TM.applyPre_startInvariant {k : ℕ} (M : TM k) (y : List Bool) (realInput : Tape) (i : Fin (k + 2)) :
      (M.applyPre y realInput i).StartInvariant

      Every entry tape of the work-to-work evaluator satisfies the left-marker invariant.

      source
      theorem Complexity.TM.applyPre_cells_blank {k : ℕ} (M : TM k) (y : List Bool) (realInput : Tape) (i : Fin (k + 2)) (j : ℕ) (hj : y.length < j) :
      (M.applyPre y realInput i).cells j = Γ.blank

      Every entry tape of the work-to-work evaluator is blank beyond the virtual input's length.

      source
      theorem Complexity.TM.applyTM_hoareTime_frame {k : ℕ} (M : TM k) {f : List Bool → List Bool} {T : ℕ → ℕ} (hcomp : M.ComputesInTime f 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 ∧ (work (Fin.last (k + 1))).HasOutput (f y) ∧ ∀ (i : Fin (k + 2)), (work i).StartInvariant ∧ (work i).head ≤ H ∧ ∀ (j : ℕ), H < j → (work i).cells j = Γ.blank) (T y.length)

      The work-to-work evaluator, with its disturbance framed. Beyond computing f y onto the result tape, this records the two facts a caller needs in order to reset the machine 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|.