The size of the simulated configurations

After j steps, the configuration of the simulation is bounded in the length of the encoded description, the length of the input and j: the state and all symbols on the work tapes and the output are numbers from the description, the input head stays on the input, every head moves by at most one cell per step, and every zipper grows by at most two cells per step.

Main definitions

• Turing.MultiTapeTM.Universal.cfgBound: the bound on the configurations.
• Turing.MultiTapeTM.Universal.stepBound: Turing.MultiTapeTM.Universal.stepTime at the largest sizes the invariant allows.

Main results

• Turing.MultiTapeTM.Universal.length_eCfg_iterate_le: the size of the configuration after j steps.
• Turing.MultiTapeTM.Universal.stepTime_iterate_le: the time of the step after j steps.

Numbers in the description

theorem Turing.MultiTapeTM.Universal.getD_le_length_eSym (o : Option ℕ) : o.getD 0 ≤ (eSym o).length

A symbol is at most the length of its encoding.

theorem Turing.MultiTapeTM.Universal.length_eSym_le {o : Option ℕ} {b : ℕ} (h : o.getD 0 ≤ b) : (eSym o).length ≤ b + 1

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.descLen (d : Desc) : ℕ

The length of the encoded description, which bounds all numbers in it.

theorem Turing.MultiTapeTM.Universal.length_act_le {d : Desc} {e : Key × Act} (he : e ∈ d.table) : (eAct e.2).length ≤ descLen d

An action of a transition of a description is encoded within its length.

theorem Turing.MultiTapeTM.Universal.state_le {d : Desc} {e : Key × Act} (he : e ∈ d.table) : e.2.state.getD 0 ≤ descLen d

The next state of a transition of a description is within its length.

theorem Turing.MultiTapeTM.Universal.output_le {d : Desc} {e : Key × Act} (he : e ∈ d.table) : e.2.output.getD 0 ≤ descLen d

The output symbol of a transition of a description is within its length.

theorem Turing.MultiTapeTM.Universal.write_le {d : Desc} {e : Key × Act} (he : e ∈ d.table) {ta : TapeAct} (hta : ta ∈ e.2.workTapes) : (ta.1.getD none).getD 0 ≤ descLen d

A symbol written by a transition of a description is within its length.

theorem Turing.MultiTapeTM.Universal.q₀_le (d : Desc) : d.q₀ ≤ descLen d

The initial state of a description is within its length.

theorem Turing.MultiTapeTM.Universal.tapes_le (d : Desc) : d.tapes ≤ descLen d

The number of work tapes of a description is within its length.

theorem Turing.MultiTapeTM.Universal.table_le (d : Desc) : d.table.length ≤ descLen d

The number of transitions of a description is within its length.

The invariant

structure Turing.MultiTapeTM.Universal.TapeInv (D j : ℕ) (t : Tape) : Prop

A work tape after at most j steps, with symbols at most D: the head is within [-j, j] and the zipper holds at most 2 * j cells.

• head : t.head.natAbs ≤ j
• length : t.left.length + t.right.length ≤ 2 * j
• val (o : Option ℕ) : o ∈ t.left ++ t.right → o.getD 0 ≤ D

structure Turing.MultiTapeTM.Universal.Inv (D X j : ℕ) (c : SCfg) : Prop

A configuration after at most j steps, for a description of length D and an input of length X.

• state : c.state.getD 0 ≤ D
• inputPos : c.inputPos ≤ X + 1
• tapes : c.workTapes.length ≤ D
• workTapes (t : Tape) : t ∈ c.workTapes → TapeInv D j t

theorem Turing.MultiTapeTM.Universal.length_applyTapes_eq (ts : List Tape) (as : List TapeAct) : (applyTapes ts as).length = ts.length

theorem Turing.MultiTapeTM.Universal.inv_init (d : Desc) (x : List ℕ) : Inv (descLen d) x.length 0 (init d)

The initial configuration satisfies the invariant.

theorem Turing.MultiTapeTM.Universal.Inv.apply {d : Desc} {x : List ℕ} {j : ℕ} {c : SCfg} (h : Inv (descLen d) x.length j c) {e : Key × Act} (he : e ∈ d.table) : Inv (descLen d) x.length (j + 1) (e.2.apply x c)

Firing an entry of the description preserves the invariant, with one more step.

theorem Turing.MultiTapeTM.Universal.inv_iterate (d : Desc) (x : List ℕ) (j : ℕ) : Inv (descLen d) x.length j ((stepOut d x)^[j] (init d, [])).1 ∧ ((stepOut d x)^[j] (init d, [])).2.length ≤ j ∧ ∀ o ∈ ((stepOut d x)^[j] (init d, [])).2, o ≤ descLen d

The configuration and the output after j steps.

The size bound

theorem Turing.MultiTapeTM.Universal.length_encIntUnary_le (z : ℤ) : (encIntUnary z).length ≤ z.natAbs + 1

theorem Turing.MultiTapeTM.Universal.length_encNat_le (n : ℕ) : (encNat n).length ≤ n

theorem Turing.MultiTapeTM.Universal.length_cells_le {D : ℕ} {l : List (Option ℕ)} (h : ∀ o ∈ l, o.getD 0 ≤ D) : ((encList eSym) l).length ≤ l.length * (2 * D + 3)

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.tapeBound (D j : ℕ) : ℕ

The bound on the encoded work tapes.

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.cfgBound (D X j : ℕ) : ℕ

The bound on the encoded configurations, after j steps.

theorem Turing.MultiTapeTM.Universal.length_eCfg_iterate_le (d : Desc) (x : List ℕ) (j : ℕ) : (eCfg ((stepOut d x)^[j] (init d, [])).1).length ≤ cfgBound (descLen d) x.length j

The size of the simulated configurations after j steps.

The time of a step

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.ctxBound (D N j : ℕ) : ℕ

The bound on the context of a step after j steps, for a description of length D and an input of encoded length N.

def Turing.MultiTapeTM.Universal.stepBound (D N j : ℕ) : ℕ

The bound on the time of a step after j steps, for a description of length D and an input of encoded length N: Turing.MultiTapeTM.Universal.stepTime at the largest sizes the invariant allows.

theorem Turing.MultiTapeTM.Universal.stepBound_mono {D N j D' N' j' : ℕ} (hD : D ≤ D') (hN : N ≤ N') (hj : j ≤ j') : stepBound D N j ≤ stepBound D' N' j'

theorem Turing.MultiTapeTM.Universal.length_eCtx_le (d : Desc) (x : List ℕ) {j : ℕ} {c : SCfg} (h : Inv (descLen d) x.length j c) : (eCtx ((d, x), c)).length ≤ ctxBound (descLen d) ((encList encUnary) x).length j

theorem Turing.MultiTapeTM.Universal.stepTime_iterate_le (d : Desc) (x : List ℕ) (j : ℕ) : stepTime ((d, x), ((stepOut d x)^[j] (init d, [])).1) ≤ stepBound (descLen d) ((encList encUnary) x).length j

The time of a step after j steps, in the length of the description, the length of the encoded input and j.