Skip to content

Quadratic overhead of single-tape simulation

9 fully proved

Multi-stack steps on the TM1 emulator

TheoremThe emulator walks right to the top of a stack#✓fully proved

Let \(M\) be a multi-stack machine, \(k\) a stack, \(L\) tape contents whose \(k\)-th track lists a stack \(S\) from bottom to top, and \(n \le |S|\). In the \(\mathrm{TM1}\) emulator of \(M\), the configuration in the state that walks to stack \(k\) (for a given stack action and continuation), with internal state \(v\) and head at the bottom marker of \(L\), reaches in exactly \(n\) steps the same configuration with the head moved \(n\) cells to the right.

theorem relatesInSteps_go {k : K} (o : StAct K Γ σ k) (q : TM2.Stmt Γ Λ σ) (v : σ)
    {S : List (Γ k)} {L : ListBlank (∀ k, Option (Γ k))}
    (hL : L.map (proj k) = ListBlank.mk (S.map some).reverse) (n : ℕ) (H : n ≤ S.length) :
    RelatesInSteps (fun a b ↦ b ∈ TM1.step (tr M) a)
      ⟨some (.go k o q), v, Tape.mk' ∅ (addBottom L)⟩
      ⟨some (.go k o q), v, (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L))⟩ n
Used by 1
Used byRunning one statement on the emulator

TheoremThe emulator walks back to the bottom#✓fully proved

Let \(M\) be a multi-stack machine and \(L\) tape contents. For every \(n\), in the \(\mathrm{TM1}\) emulator of \(M\), the configuration in the return state (for a given continuation), with internal state \(v\) and head \(n\) cells to the right of the bottom marker of \(L\), reaches in exactly \(n\) steps the same configuration with the head at the bottom marker.

theorem relatesInSteps_ret {q : TM2.Stmt Γ Λ σ} {v : σ} {L : ListBlank (∀ k, Option (Γ k))}
    (n : ℕ) :
    RelatesInSteps (fun a b ↦ b ∈ TM1.step (tr M) a)
      ⟨some (.ret q), v, (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L))⟩
      ⟨some (.ret q), v, Tape.mk' ∅ (addBottom L)⟩ n
Used by 1
Used byRunning one statement on the emulator

TheoremRunning one statement on the emulator#✓fully proved

Let \(M\) be a multi-stack machine and \(N\) a statement over the same stack alphabets, labels and internal states, and write \(|N|\) for the structural size of \(N\). Let \(H \in \mathbb{N}\), let \(v\) be an internal state, let \(S\) be a family of stacks \(S_k\), each of height at most \(H\), and let \(L\) be tape contents whose \(k\)-th track lists \(S_k\) from bottom to top, for every \(k\). Running the translation of \(N\) in the \(\mathrm{TM1}\) emulator of \(M\) from state \(v\), with the head at the bottom marker of \(L\), gives a configuration that reaches, in some number \(m \le |N| (2 (H + |N|) + 2)\) of emulator steps, a configuration representing the result of running \(N\) from state \(v\) on the stacks \(S\): it has the corresponding label and the same internal state, and its head is at the bottom marker of a tape whose \(k\)-th track lists the \(k\)-th resulting stack from bottom to top.

theorem exists_relatesInSteps_stepAux (N : TM2.Stmt Γ Λ σ) :
    ∀ (H : ℕ) (v : σ) (S : ∀ k, List (Γ k)) (L : ListBlank (∀ k, Option (Γ k))),
      (∀ k, L.map (proj k) = ListBlank.mk ((S k).map some).reverse) →
      (∀ k, (S k).length ≤ H) →
      ∃ b m, TrCfg (TM2.stepAux N v S) b ∧
        RelatesInSteps (fun a b ↦ b ∈ TM1.step (tr M) a)
          (TM1.stepAux (trNormal N) v (Tape.mk' ∅ (addBottom L))) b m ∧
        m ≤ sizeOf N * (2 * (H + sizeOf N) + 2)
Uses 2 · Used by 1
Proof usesThe emulator walks right to the top of a stack · The emulator walks back to the bottom
Used byOne multi-stack step costs at most \(1 + B(2(H + B) + 2)\) emulator steps

TheoremOne multi-stack step costs at most \(1 + B(2(H + B) + 2)\) emulator steps#✓fully proved

Let \(M\) be a multi-stack machine in which the statement of every label has size at most \(B\), and consider its emulation by a single-tape machine with an internal store that keeps the stacks side by side on its tape. Let \(c\) be a configuration of \(M\) in which every stack has height at most \(H\), and let \(c_1\) be a configuration of the emulator that represents \(c\). If \(M\) moves from \(c\) to \(c'\) in one step, then there is a configuration \(c_1'\) of the emulator that represents \(c'\) and that the emulator reaches from \(c_1\) in at most \(1 + B(2(H + B) + 2)\) steps.

The size of a statement is its structural size as a term. This is a counted form of the correctness of the emulation.

theorem exists_relatesWithinSteps_tm1_of_step {B H : ℕ} (hB : ∀ l, sizeOf (M l) ≤ B)
    {c c' : TM2.Cfg Γ Λ σ} {c₁ : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ} (hc : TrCfg c c₁)
    (hH : ∀ k, (c.stk k).length ≤ H) (h : TM2.step M c = some c') :
    ∃ c₁', TrCfg c' c₁' ∧
      RelatesWithinSteps (fun a b ↦ b ∈ TM1.step (tr M) a) c₁ c₁'
        (1 + B * (2 * (H + B) + 2))
Uses 1 · Used by 1
Proof usesRunning one statement on the emulator
Used byQuadratic overhead of the single-tape emulation

TheoremThe emulation halts where the multi-stack machine halts#✓fully proved

A halted configuration is related only to configurations of the single-tape emulation that do not step.

theorem tm0_step_eq_none_of_step_eq_none [Inhabited Λ] [Inhabited σ] {c : TM2.Cfg Γ Λ σ}
    {c₁ : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ} (hc : TrCfg c c₁) (h : TM2.step M c = none) :
    TM0.step (MetaMathlibExt.TM2ToTM0.tr M) (TM1to0.trCfg (tr M) c₁) = none
Uses 1 · Used by 1
Statement usesTwo-step single-tape translation of a multi-stack machine
Used bySingle-tape emulation of halting multi-stack runs

TM1 steps on TM0

TheoremEach step of the \(\mathrm{TM1}\) emulator is at most three single-tape steps#✓fully proved

Let \(M\) be a multi-stack machine with a default label and a default internal state. If the \(\mathrm{TM1}\) emulator of \(M\) goes from \(c\) to \(c'\) in exactly \(m\) steps, then the single-tape emulation of \(M\) goes from the single-tape form of \(c\) to the single-tape form of \(c'\) in at most \(3m\) steps.

theorem relatesWithinSteps_tm0_of_relatesInSteps_tm1 [Inhabited Λ] [Inhabited σ]
    {c c' : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ} {m : ℕ}
    (h : RelatesInSteps (fun a b ↦ b ∈ TM1.step (tr M) a) c c' m) :
    RelatesWithinSteps (fun a b ↦ b ∈ TM0.step (MetaMathlibExt.TM2ToTM0.tr M) a)
      (TM1to0.trCfg (tr M) c) (TM1to0.trCfg (tr M) c') (3 * m)
Uses 1 · Used by 1
Statement usesTwo-step single-tape translation of a multi-stack machine
Used byQuadratic overhead of the single-tape emulation

Runs of bundled machines

DefinitionEmulation constant#✓fully proved

For a bundled multi-stack machine \(M\), the emulation constant is \(C = 3(2B + 1) + P\), where \(B = \sum_l |M(l)|\) is the total structural size of the statements \(M(l)\) over all labels \(l\) (so each statement has size at most \(B\)), and \(P\) is the push bound of \(M\), the total number of push instructions in its statements, which bounds the number of pushes in one step.

noncomputable def emulationConstant (tm : FinTM2) : ℕ :=
  3 * (2 * ∑ l, sizeOf (tm.m l) + 1) + MetaMathlibExt.TM2Composition.pushBound tm
Uses 1 · Used by 4
Statement usesPush bound of a finite multi-stack Turing machine
Used byThe decider within time · Problems in P are decided in polynomial time by single-tape machines · Single-tape emulation of halting multi-stack runs · Quadratic overhead of the single-tape emulation

TheoremQuadratic overhead of the single-tape emulation#✓fully proved

Let \(M\) be a bundled multi-stack machine with emulation constant \(C\), and \(L\) an input for its input stack. If \(M\), started on \(L\), reaches a configuration \(c\) after \(t\) steps, then the single-tape emulation of \(M\), started on the encoding of \(L\), reaches in some number \(n \le C t (|L| + C t + 1)\) of steps the single-tape form of a configuration of the \(\mathrm{TM1}\) emulator of \(M\) that represents \(c\): it has the corresponding label and the same internal state, and its head is at the bottom marker of a tape whose \(k\)-th track lists the \(k\)-th stack of \(c\) from bottom to top.

theorem exists_tm0_run_of_tm2_run (tm : FinTM2) (L : List (tm.Γ tm.k₀)) {c : tm.Cfg} {t : ℕ}
    (h : (flip bind tm.step)^[t] (some (initList tm L)) = some c) :
    ∃ (c₁ : TM1.Cfg (Γ' tm.K tm.Γ) (Λ' tm.K tm.Γ tm.Λ tm.σ) tm.σ) (n : ℕ),
      TrCfg c c₁ ∧
      RelatesInSteps (fun a b ↦ b ∈ TM0.step (MetaMathlibExt.TM2ToTM0.tr tm.m) a)
        (TM0.init (trInit tm.k₀ L)) (TM1to0.trCfg (tr tm.m) c₁) n ∧
      n ≤ emulationConstant tm * t * (L.length + emulationConstant tm * t + 1)
Uses 9 · Used by 1
Statement usesEmulation constant · Two-step single-tape translation of a multi-stack machine
Proof usesOne multi-stack step costs at most \(1 + B(2(H + B) + 2)\) emulator steps · Each step of the \(\mathrm{TM1}\) emulator is at most three single-tape steps · Stacks of the initial configuration are no longer than the input · Push bound of a finite multi-stack Turing machine · Number of push instructions in a TM2 statement · A halted run stays halted · The initial configuration of a bundled multi-stack machine
Used bySingle-tape emulation of halting multi-stack runs

TheoremSingle-tape emulation of halting multi-stack runs#✓fully proved

Let \(M\) be a bundled multi-stack machine with emulation constant \(C\), and \(L\) an input for its input stack. If \(M\), started on \(L\), reaches after \(t\) steps a configuration \(c\) from which it does not step, then the single-tape emulation of \(M\), started on the encoding of \(L\), reaches in some number \(n \le C t (|L| + C t + 1)\) of steps a configuration from which it does not step. That configuration is the single-tape form of a configuration of the \(\mathrm{TM1}\) emulator of \(M\) that represents \(c\): it has the corresponding label and the same internal state, and its head is at the bottom marker of a tape whose \(k\)-th track lists the \(k\)-th stack of \(c\) from bottom to top.

theorem exists_tm0_halt_of_tm2_halt (tm : FinTM2) (L : List (tm.Γ tm.k₀)) {c : tm.Cfg} {t : ℕ}
    (h : (flip bind tm.step)^[t] (some (initList tm L)) = some c) (hc : tm.step c = none) :
    ∃ (c₁ : TM1.Cfg (Γ' tm.K tm.Γ) (Λ' tm.K tm.Γ tm.Λ tm.σ) tm.σ) (n : ℕ),
      TrCfg c c₁ ∧
      RelatesInSteps (fun a b ↦ b ∈ TM0.step (MetaMathlibExt.TM2ToTM0.tr tm.m) a)
        (TM0.init (trInit tm.k₀ L)) (TM1to0.trCfg (tr tm.m) c₁) n ∧
      TM0.step (MetaMathlibExt.TM2ToTM0.tr tm.m) (TM1to0.trCfg (tr tm.m) c₁) = none ∧
      n ≤ emulationConstant tm * t * (L.length + emulationConstant tm * t + 1)
Uses 4 · Used by 1
Statement usesEmulation constant · Two-step single-tape translation of a multi-stack machine
Proof usesQuadratic overhead of the single-tape emulation · The emulation halts where the multi-stack machine halts
Used byThe decider within time

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.