Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.MachineBridge

Correctness of the finite-alphabet multitape simulator #

The tape invariant uses coordinates relative to each work head. Initialization copies the input to its symbol tracks, then rewinds those heads; simulation preserves all relative cells.

theorem Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.encode_injective {Γ : Type u_1} [Inhabited Γ] :

Function.Injective encode

theorem Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.decode_encode {Γ : Type u_1} [Inhabited Γ] (a : Γ) :

decode (encode a) = a

theorem Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.encode_default {Γ : Type u_1} [Inhabited Γ] :

encode default = fun (x : Γ) => none

theorem Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.move_nth {Γ : Type u_1} [Inhabited Γ] (d : HeadMove) (t : Turing.Tape Γ) (z : ℤ) :

(d.apply t).nth z = t.nth (z + ↑(moveSign d))

structure Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.Sim (M : FiniteMultiTapeMachine) {input : List Bool} (c : M.Cfg) (d : Turing.Cfg (Fintype.card (M.K × M.Γ)) Bool (Control M.Q) input) :

Relative tape contents agree and the simulator is running the source control.

state : d.state = some (Control.run c.q)
The controls correspond.
output : d.output = []
No output is emitted before source halting.
tape (i : Fin (Fintype.card (M.K × M.Γ))) (z : ℤ) : d.workTapes i (d.workTapePos i + z) = encode ((c.tapes ((trackEquiv M) i).1).nth z) ((trackEquiv M) i).2
Every track agrees at every offset from its head.

Instances For

theorem Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.Sim.read {M : FiniteMultiTapeMachine} {input : List Bool} {c : M.Cfg} {d : Turing.Cfg (Fintype.card (M.K × M.Γ)) Bool (Control M.Q) input} (h : Sim M c d) (k : M.K) :

(decode fun (a : M.Γ) => d.workTapeSymbols (track M k a)) = (c.tapes k).head

theorem Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.Sim.step {M : FiniteMultiTapeMachine} {input : List Bool} {c c' : M.Cfg} {d : Turing.Cfg (Fintype.card (M.K × M.Γ)) Bool (Control M.Q) input} (h : Sim M c d) (hs : M.step c = some c') :

Sim M c' (Turing.MultiTapeTM.step d)

theorem Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.Sim.halt {M : FiniteMultiTapeMachine} {input : List Bool} {c : M.Cfg} {d : Turing.Cfg (Fintype.card (M.K × M.Γ)) Bool (Control M.Q) input} (h : Sim M c d) (hs : M.step c = none) :

(Turing.MultiTapeTM.step d).state = none ∧ (Turing.MultiTapeTM.step d).output = [M.accept c.q]

theorem Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.Sim.run {M : FiniteMultiTapeMachine} {input : List Bool} {c c' : M.Cfg} {d : Turing.Cfg (Fintype.card (M.K × M.Γ)) Bool (Control M.Q) input} (h : Sim M c d) (t : ℕ) (hs : runSteps M.step t (some c) = some c') :

Sim M c' (Turing.MultiTapeTM.runFrom d t)

theorem Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.nth_mk₁ {Γ : Type u_1} [Inhabited Γ] (l : List Γ) (z : ℤ) :

(Turing.Tape.mk₁ l).nth z = if z < 0 then default else l.getI z.toNat

theorem Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.nth_mk₁_nil {Γ : Type u_1} [Inhabited Γ] (z : ℤ) :

(Turing.Tape.mk₁ []).nth z = default

theorem Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.nth_mk₁_append_singleton {Γ : Type u_1} [Inhabited Γ] (l : List Γ) (a : Γ) (z : ℤ) :

(Turing.Tape.mk₁ (l ++ [a])).nth z = if z = ↑l.length then a else (Turing.Tape.mk₁ l).nth z

noncomputable def Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.inputContents (M : FiniteMultiTapeMachine) (bits : List Bool) (i : Track M) (z : ℤ) :

The track contents after copying an input prefix.

Equations

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

Instances For

theorem Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.inputContents_nil (M : FiniteMultiTapeMachine) :

inputContents M [] = fun (x : Track M) (x_1 : ℤ) => none

theorem Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.inputContents_append (M : FiniteMultiTapeMachine) (bits : List Bool) (b : Bool) (i : Track M) :

inputContents M (bits ++ [b]) i = if ((trackEquiv M) i).1 = M.inputTape then Function.update (inputContents M bits i) (↑bits.length) (encode (M.inputSymbol b) ((trackEquiv M) i).2) else inputContents M bits i

noncomputable def Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.copyCfg (M : FiniteMultiTapeMachine) (w : List Bool) (t : ℕ) (ht : t ≤ w.length) :

Turing.Cfg (Fintype.card (M.K × M.Γ)) Bool (Control M.Q) w

The configuration after copying an input prefix of length t.

Equations

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

Instances For

noncomputable def Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.rewindCfg (M : FiniteMultiTapeMachine) (w : List Bool) (t : ℕ) (ht : t ≤ w.length) :

Turing.Cfg (Fintype.card (M.K × M.Γ)) Bool (Control M.Q) w

The configuration with t input cells left to rewind.

Equations

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

Instances For

theorem Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.copyCfg_zero (M : FiniteMultiTapeMachine) (w : List Bool) :

copyCfg M w 0 ⋯ = Turing.MultiTapeTM.initCfg w

theorem Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.copyCfg_step (M : FiniteMultiTapeMachine) (w : List Bool) (t : ℕ) (ht : t < w.length) :

Turing.MultiTapeTM.step (copyCfg M w t ⋯) = copyCfg M w (t + 1) ⋯

theorem Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.copyCfg_end (M : FiniteMultiTapeMachine) (w : List Bool) :

Turing.MultiTapeTM.step (copyCfg M w w.length ⋯) = rewindCfg M w w.length ⋯

theorem Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.rewindCfg_step (M : FiniteMultiTapeMachine) (w : List Bool) (t : ℕ) (ht : t + 1 ≤ w.length) :

Turing.MultiTapeTM.step (rewindCfg M w (t + 1) ht) = rewindCfg M w t ⋯

theorem Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.runFrom_add (M : FiniteMultiTapeMachine) {w : List Bool} (d : Turing.Cfg (Fintype.card (M.K × M.Γ)) Bool (Control M.Q) w) (t u : ℕ) :

Turing.MultiTapeTM.runFrom d (t + u) = Turing.MultiTapeTM.runFrom (Turing.MultiTapeTM.runFrom d t) u

theorem Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.runFrom_succ (M : FiniteMultiTapeMachine) {w : List Bool} (d : Turing.Cfg (Fintype.card (M.K × M.Γ)) Bool (Control M.Q) w) (t : ℕ) :

Turing.MultiTapeTM.runFrom d (t + 1) = Turing.MultiTapeTM.step (Turing.MultiTapeTM.runFrom d t)

theorem Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.run_copy (M : FiniteMultiTapeMachine) (w : List Bool) (t : ℕ) (ht : t ≤ w.length) :

Turing.MultiTapeTM.runFrom (Turing.MultiTapeTM.initCfg w) t = copyCfg M w t ht

theorem Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.run_rewind (M : FiniteMultiTapeMachine) (w : List Bool) (t : ℕ) (ht : t ≤ w.length) :

Turing.MultiTapeTM.runFrom (rewindCfg M w t ht) t = rewindCfg M w 0 ⋯

theorem Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.rewindCfg_zero_sim (M : FiniteMultiTapeMachine) (w : List Bool) :

Sim M (M.init w) (Turing.MultiTapeTM.step (rewindCfg M w 0 ⋯))

theorem Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.init_sim (M : FiniteMultiTapeMachine) (w : List Bool) :

Sim M (M.init w) (Turing.MultiTapeTM.runFrom (Turing.MultiTapeTM.initCfg w) (2 * w.length + 2))

theorem Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.computes_proof (M : FiniteMultiTapeMachine) (w : List Bool) (b : Bool) (T : ℕ) (h : MultiTapeHaltsIn M w b T) :

(machine M).ComputesInTimeAndSpace w [b] (2 * w.length + T + 3) (Turing.MultiTapeTM.spaceUsed (Turing.MultiTapeTM.initCfg w) (2 * w.length + T + 3))

theorem Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.decidableInTimeAndSpace (M : FiniteMultiTapeMachine) (L : List Bool → Bool) (T : ℕ → ℕ) (h : ∀ (w : List Bool), MultiTapeHaltsIn M w (L w) (T w.length)) :

Turing.MultiTapeTM.DecidableInTimeAndSpace {w : List Bool | L w = true } (Function.Embedding.refl (List Bool)) (fun (w : List Bool) => 2 * w.length + T w.length + 3) fun (w : List Bool) => Turing.MultiTapeTM.spaceUsed (Turing.MultiTapeTM.initCfg w) (2 * w.length + T w.length + 3)

theorem Complexity.DepthThreeLowerBound.FiniteMultiTapeMachine.mem_P_proof {M : FiniteMultiTapeMachine} {L : List Bool → Bool} {p : Polynomial ℕ} (h : ∀ (w : List Bool), MultiTapeHaltsIn M w (L w) (Polynomial.eval w.length p)) :

{w : List Bool | L w = true } ∈ P