The cost of a step of the simulation

States, symbols and moves are encoded in unary (Turing.MultiTapeTM.encUnary), head positions on the work tapes as unary integers (Turing.MultiTapeTM.encIntUnary), the position of the input head in binary (Turing.MultiTapeTM.encNat), and a structure as the framed tuple of its fields.

Reading, writing and moving on a zipper are computable in linear time and space (Turing.MultiTapeTM.ComputableInDegree with degrees one). A step of the simulation (Turing.MultiTapeTM.Universal.step_inO) takes space linear in the length L of the encoded context (the description, the input and the configuration). Its time bound separates the configuration length from description lookup and input scanning: for K work tapes, E transitions, description length D, encoded input length N, input position p and binary position length P, the bound is (K + E + 1) * (D + 1) * (L + 1) + (N + 1) * (P + 1) ^ 2. The first word in a transition comparison comes from the description, so its length is bounded by D, even when the simulated configuration is large. The input scanner streams the encoded list with a binary countdown, whose arithmetic is charged to P. The configuration is still copied each round; this bound does not implement the buffered Hennie–Stearns simulation.

Main definitions

• Turing.MultiTapeTM.Universal.eDesc, .eCfg: the encodings of descriptions and configurations, declared with enc_structure, which also supplies their fun_prop rules.
• Turing.MultiTapeTM.Universal.Ctx, .WCtx: the contexts of a step, with and without the input, and their named parts (Ctx.desc, Ctx.input, Ctx.cfg, WCtx.desc, WCtx.cfg, WCtx.sym).
• Turing.MultiTapeTM.Universal.stepTime: the time bound of a step.

Main results

• Turing.MultiTapeTM.Universal.step_inO: a step is computable (Turing.MultiTapeTM.ComputableInO) within the time stepTime and linear space.
• Turing.MultiTapeTM.Universal.stepWith_inO, .applyTapes_inO, .reads_inO, .moveInput_inO: its parts.

Encodings

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.eSym : Option ℕ ↪ List Bool

Symbols and blanks.

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.eKeyFields : ℕ × Option ℕ × List (Option ℕ) ↪ List Bool

The tuple of the fields of eKey.

theorem Turing.MultiTapeTM.Universal.eKey_input_deg : ComputableInDegree Key.input eKey eSym 1 1

theorem Turing.MultiTapeTM.Universal.eKey_fields_deg : ComputableInDegree (fun (a : Key) => (a.state, a.input, a.work)) eKey eKeyFields 1 1

theorem Turing.MultiTapeTM.Universal.eKey_state_inO : ComputableInO Key.state eKey encUnary (fun (a : Key) => (eKey a).length) fun (a : Key) => (eKey a).length

theorem Turing.MultiTapeTM.Universal.eKey_work_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Key} : ComputableInPolyTime g✝ encIn✝ eKey → ComputableInPolyTime (fun (a : γ✝) => (g✝ a).work) encIn✝ (encList eSym)

theorem Turing.MultiTapeTM.Universal.eKey_input_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Key} : ComputableInSpace g✝ encIn✝ eKey S✝ → ComputableInSpace (fun (a : γ✝) => (g✝ a).input) encIn✝ eSym S✝

theorem Turing.MultiTapeTM.Universal.eKey_mk_deg : ComputableInDegree (fun (p : ℕ × Option ℕ × List (Option ℕ)) => { state := p.1, input := p.2.1, work := p.2.2 }) eKeyFields eKey 1 1

theorem Turing.MultiTapeTM.Universal.eKey_work_deg : ComputableInDegree Key.work eKey (encList eSym) 1 1

theorem Turing.MultiTapeTM.Universal.eKey_state_deg : ComputableInDegree Key.state eKey encUnary 1 1

def Turing.MultiTapeTM.Universal.eKey : Key ↪ List Bool

Keys of transitions, as their fields.

theorem Turing.MultiTapeTM.Universal.eKey_state_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Key} : ComputableInPolyTime g✝ encIn✝ eKey → ComputableInPolyTime (fun (a : γ✝) => (g✝ a).state) encIn✝ encUnary

theorem Turing.MultiTapeTM.Universal.eKey_work_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Key} : ComputableInSpace g✝ encIn✝ eKey S✝ → ComputableInSpace (fun (a : γ✝) => (g✝ a).work) encIn✝ (encList eSym) S✝

theorem Turing.MultiTapeTM.Universal.eKey_state_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Key} : ComputableInSpace g✝ encIn✝ eKey S✝ → ComputableInSpace (fun (a : γ✝) => (g✝ a).state) encIn✝ encUnary S✝

@[simp]

theorem Turing.MultiTapeTM.Universal.eKey_apply (a : Key) : eKey a = eKeyFields (a.state, a.input, a.work)

theorem Turing.MultiTapeTM.Universal.eKey_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → ℕ} {x1 : γ → Option ℕ} {x2 : γ → List (Option ℕ)} (h0 : ComputableInPolyTime x0 encIn encUnary) (h1 : ComputableInPolyTime x1 encIn eSym) (h2 : ComputableInPolyTime x2 encIn (encList eSym)) : ComputableInPolyTime (fun (x : γ) => { state := x0 x, input := x1 x, work := x2 x }) encIn eKey

theorem Turing.MultiTapeTM.Universal.eKey_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 T0 S0 : γ → ℕ} {x1 : γ → Option ℕ} {T1 S1 : γ → ℕ} {x2 : γ → List (Option ℕ)} {T2 S2 : γ → ℕ} (h0 : ComputableInO x0 encIn encUnary T0 S0) (h1 : ComputableInO x1 encIn eSym T1 S1) (h2 : ComputableInO x2 encIn (encList eSym) T2 S2) : ComputableInO (fun (x : γ) => { state := x0 x, input := x1 x, work := x2 x }) encIn eKey (fun (x : γ) => T0 x + (T1 x + T2 x)) fun (x : γ) => S0 x + (S1 x + S2 x)

theorem Turing.MultiTapeTM.Universal.eKey_work_inO : ComputableInO Key.work eKey (encList eSym) (fun (a : Key) => (eKey a).length) fun (a : Key) => (eKey a).length

theorem Turing.MultiTapeTM.Universal.eKey_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget x0 : γ → ℕ} {x1 : γ → Option ℕ} {x2 : γ → List (Option ℕ)} (h0 : ComputableInSpace x0 encIn encUnary budget) (h1 : ComputableInSpace x1 encIn eSym budget) (h2 : ComputableInSpace x2 encIn (encList eSym) budget) : ComputableInSpace (fun (x : γ) => { state := x0 x, input := x1 x, work := x2 x }) encIn eKey budget

theorem Turing.MultiTapeTM.Universal.eKey_input_inO : ComputableInO Key.input eKey eSym (fun (a : Key) => (eKey a).length) fun (a : Key) => (eKey a).length

theorem Turing.MultiTapeTM.Universal.eKey_input_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Key} : ComputableInPolyTime g✝ encIn✝ eKey → ComputableInPolyTime (fun (a : γ✝) => (g✝ a).input) encIn✝ eSym

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.TapeAct : Type

An action on a work tape.

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.eTA : Option (Option ℕ) × SignType ↪ List Bool

Actions on a work tape.

theorem Turing.MultiTapeTM.Universal.eAct_state_inO : ComputableInO Act.state eAct eSym (fun (a : Act) => (eAct a).length) fun (a : Act) => (eAct a).length

theorem Turing.MultiTapeTM.Universal.eAct_state_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Act} : ComputableInSpace g✝ encIn✝ eAct S✝ → ComputableInSpace (fun (a : γ✝) => (g✝ a).state) encIn✝ eSym S✝

theorem Turing.MultiTapeTM.Universal.eAct_workTapes_inO : ComputableInO Act.workTapes eAct (encList eTA) (fun (a : Act) => (eAct a).length) fun (a : Act) => (eAct a).length

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.eActFields : SignType × List (Option (Option ℕ) × SignType) × Option ℕ × Option ℕ ↪ List Bool

The tuple of the fields of eAct.

theorem Turing.MultiTapeTM.Universal.eAct_workTapes_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Act} : ComputableInPolyTime g✝ encIn✝ eAct → ComputableInPolyTime (fun (a : γ✝) => (g✝ a).workTapes) encIn✝ (encList eTA)

theorem Turing.MultiTapeTM.Universal.eAct_workTapes_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Act} : ComputableInSpace g✝ encIn✝ eAct S✝ → ComputableInSpace (fun (a : γ✝) => (g✝ a).workTapes) encIn✝ (encList eTA) S✝

theorem Turing.MultiTapeTM.Universal.eAct_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → SignType} {x1 : γ → List (Option (Option ℕ) × SignType)} {x2 x3 : γ → Option ℕ} (h0 : ComputableInPolyTime x0 encIn encSign) (h1 : ComputableInPolyTime x1 encIn (encList eTA)) (h2 : ComputableInPolyTime x2 encIn eSym) (h3 : ComputableInPolyTime x3 encIn eSym) : ComputableInPolyTime (fun (x : γ) => { inputTape := x0 x, workTapes := x1 x, output := x2 x, state := x3 x }) encIn eAct

theorem Turing.MultiTapeTM.Universal.eAct_fields_deg : ComputableInDegree (fun (a : Act) => (a.inputTape, a.workTapes, a.output, a.state)) eAct eActFields 1 1

theorem Turing.MultiTapeTM.Universal.eAct_output_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Act} : ComputableInSpace g✝ encIn✝ eAct S✝ → ComputableInSpace (fun (a : γ✝) => (g✝ a).output) encIn✝ eSym S✝

theorem Turing.MultiTapeTM.Universal.eAct_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → SignType} {T0 S0 : γ → ℕ} {x1 : γ → List (Option (Option ℕ) × SignType)} {T1 S1 : γ → ℕ} {x2 : γ → Option ℕ} {T2 S2 : γ → ℕ} {x3 : γ → Option ℕ} {T3 S3 : γ → ℕ} (h0 : ComputableInO x0 encIn encSign T0 S0) (h1 : ComputableInO x1 encIn (encList eTA) T1 S1) (h2 : ComputableInO x2 encIn eSym T2 S2) (h3 : ComputableInO x3 encIn eSym T3 S3) : ComputableInO (fun (x : γ) => { inputTape := x0 x, workTapes := x1 x, output := x2 x, state := x3 x }) encIn eAct (fun (x : γ) => T0 x + (T1 x + (T2 x + T3 x))) fun (x : γ) => S0 x + (S1 x + (S2 x + S3 x))

@[simp]

theorem Turing.MultiTapeTM.Universal.eAct_apply (a : Act) : eAct a = eActFields (a.inputTape, a.workTapes, a.output, a.state)

def Turing.MultiTapeTM.Universal.eAct : Act ↪ List Bool

Actions, as their fields.

theorem Turing.MultiTapeTM.Universal.eAct_output_deg : ComputableInDegree Act.output eAct eSym 1 1

theorem Turing.MultiTapeTM.Universal.eAct_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget : γ → ℕ} {x0 : γ → SignType} {x1 : γ → List (Option (Option ℕ) × SignType)} {x2 x3 : γ → Option ℕ} (h0 : ComputableInSpace x0 encIn encSign budget) (h1 : ComputableInSpace x1 encIn (encList eTA) budget) (h2 : ComputableInSpace x2 encIn eSym budget) (h3 : ComputableInSpace x3 encIn eSym budget) : ComputableInSpace (fun (x : γ) => { inputTape := x0 x, workTapes := x1 x, output := x2 x, state := x3 x }) encIn eAct budget

theorem Turing.MultiTapeTM.Universal.eAct_output_inO : ComputableInO Act.output eAct eSym (fun (a : Act) => (eAct a).length) fun (a : Act) => (eAct a).length

theorem Turing.MultiTapeTM.Universal.eAct_inputTape_inO : ComputableInO Act.inputTape eAct encSign (fun (a : Act) => (eAct a).length) fun (a : Act) => (eAct a).length

theorem Turing.MultiTapeTM.Universal.eAct_state_deg : ComputableInDegree Act.state eAct eSym 1 1

theorem Turing.MultiTapeTM.Universal.eAct_output_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Act} : ComputableInPolyTime g✝ encIn✝ eAct → ComputableInPolyTime (fun (a : γ✝) => (g✝ a).output) encIn✝ eSym

theorem Turing.MultiTapeTM.Universal.eAct_inputTape_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Act} : ComputableInPolyTime g✝ encIn✝ eAct → ComputableInPolyTime (fun (a : γ✝) => (g✝ a).inputTape) encIn✝ encSign

theorem Turing.MultiTapeTM.Universal.eAct_inputTape_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Act} : ComputableInSpace g✝ encIn✝ eAct S✝ → ComputableInSpace (fun (a : γ✝) => (g✝ a).inputTape) encIn✝ encSign S✝

theorem Turing.MultiTapeTM.Universal.eAct_inputTape_deg : ComputableInDegree Act.inputTape eAct encSign 1 1

theorem Turing.MultiTapeTM.Universal.eAct_workTapes_deg : ComputableInDegree Act.workTapes eAct (encList eTA) 1 1

theorem Turing.MultiTapeTM.Universal.eAct_mk_deg : ComputableInDegree (fun (p : SignType × List (Option (Option ℕ) × SignType) × Option ℕ × Option ℕ) => { inputTape := p.1, workTapes := p.2.1, output := p.2.2.1, state := p.2.2.2 }) eActFields eAct 1 1

theorem Turing.MultiTapeTM.Universal.eAct_state_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Act} : ComputableInPolyTime g✝ encIn✝ eAct → ComputableInPolyTime (fun (a : γ✝) => (g✝ a).state) encIn✝ eSym

theorem Turing.MultiTapeTM.Universal.eDesc_q₀_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Desc} : ComputableInPolyTime g✝ encIn✝ eDesc → ComputableInPolyTime (fun (a : γ✝) => (g✝ a).q₀) encIn✝ encUnary

theorem Turing.MultiTapeTM.Universal.eDesc_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget x0 x1 : γ → ℕ} {x2 : γ → List (Key × Act)} (h0 : ComputableInSpace x0 encIn encUnary budget) (h1 : ComputableInSpace x1 encIn encUnary budget) (h2 : ComputableInSpace x2 encIn (encList (encPair eKey eAct)) budget) : ComputableInSpace (fun (x : γ) => { tapes := x0 x, q₀ := x1 x, table := x2 x }) encIn eDesc budget

theorem Turing.MultiTapeTM.Universal.eDesc_q₀_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Desc} : ComputableInSpace g✝ encIn✝ eDesc S✝ → ComputableInSpace (fun (a : γ✝) => (g✝ a).q₀) encIn✝ encUnary S✝

theorem Turing.MultiTapeTM.Universal.eDesc_table_inO : ComputableInO Desc.table eDesc (encList (encPair eKey eAct)) (fun (a : Desc) => (eDesc a).length) fun (a : Desc) => (eDesc a).length

theorem Turing.MultiTapeTM.Universal.eDesc_q₀_deg : ComputableInDegree Desc.q₀ eDesc encUnary 1 1

theorem Turing.MultiTapeTM.Universal.eDesc_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 T0 S0 x1 T1 S1 : γ → ℕ} {x2 : γ → List (Key × Act)} {T2 S2 : γ → ℕ} (h0 : ComputableInO x0 encIn encUnary T0 S0) (h1 : ComputableInO x1 encIn encUnary T1 S1) (h2 : ComputableInO x2 encIn (encList (encPair eKey eAct)) T2 S2) : ComputableInO (fun (x : γ) => { tapes := x0 x, q₀ := x1 x, table := x2 x }) encIn eDesc (fun (x : γ) => T0 x + (T1 x + T2 x)) fun (x : γ) => S0 x + (S1 x + S2 x)

theorem Turing.MultiTapeTM.Universal.eDesc_table_deg : ComputableInDegree Desc.table eDesc (encList (encPair eKey eAct)) 1 1

theorem Turing.MultiTapeTM.Universal.eDesc_table_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Desc} : ComputableInPolyTime g✝ encIn✝ eDesc → ComputableInPolyTime (fun (a : γ✝) => (g✝ a).table) encIn✝ (encList (encPair eKey eAct))

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.eDescFields : ℕ × ℕ × List (Key × Act) ↪ List Bool

The tuple of the fields of eDesc.

theorem Turing.MultiTapeTM.Universal.eDesc_fields_deg : ComputableInDegree (fun (a : Desc) => (a.tapes, a.q₀, a.table)) eDesc eDescFields 1 1

@[simp]

theorem Turing.MultiTapeTM.Universal.eDesc_apply (a : Desc) : eDesc a = eDescFields (a.tapes, a.q₀, a.table)

theorem Turing.MultiTapeTM.Universal.eDesc_tapes_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Desc} : ComputableInPolyTime g✝ encIn✝ eDesc → ComputableInPolyTime (fun (a : γ✝) => (g✝ a).tapes) encIn✝ encUnary

theorem Turing.MultiTapeTM.Universal.eDesc_tapes_deg : ComputableInDegree Desc.tapes eDesc encUnary 1 1

theorem Turing.MultiTapeTM.Universal.eDesc_q₀_inO : ComputableInO Desc.q₀ eDesc encUnary (fun (a : Desc) => (eDesc a).length) fun (a : Desc) => (eDesc a).length

def Turing.MultiTapeTM.Universal.eDesc : Desc ↪ List Bool

Descriptions, as their fields.

theorem Turing.MultiTapeTM.Universal.eDesc_mk_deg : ComputableInDegree (fun (p : ℕ × ℕ × List (Key × Act)) => { tapes := p.1, q₀ := p.2.1, table := p.2.2 }) eDescFields eDesc 1 1

theorem Turing.MultiTapeTM.Universal.eDesc_tapes_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Desc} : ComputableInSpace g✝ encIn✝ eDesc S✝ → ComputableInSpace (fun (a : γ✝) => (g✝ a).tapes) encIn✝ encUnary S✝

theorem Turing.MultiTapeTM.Universal.eDesc_table_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Desc} : ComputableInSpace g✝ encIn✝ eDesc S✝ → ComputableInSpace (fun (a : γ✝) => (g✝ a).table) encIn✝ (encList (encPair eKey eAct)) S✝

theorem Turing.MultiTapeTM.Universal.eDesc_tapes_inO : ComputableInO Desc.tapes eDesc encUnary (fun (a : Desc) => (eDesc a).length) fun (a : Desc) => (eDesc a).length

theorem Turing.MultiTapeTM.Universal.eDesc_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 x1 : γ → ℕ} {x2 : γ → List (Key × Act)} (h0 : ComputableInPolyTime x0 encIn encUnary) (h1 : ComputableInPolyTime x1 encIn encUnary) (h2 : ComputableInPolyTime x2 encIn (encList (encPair eKey eAct))) : ComputableInPolyTime (fun (x : γ) => { tapes := x0 x, q₀ := x1 x, table := x2 x }) encIn eDesc

theorem Turing.MultiTapeTM.Universal.eTape_right_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Tape} : ComputableInSpace g✝ encIn✝ eTape S✝ → ComputableInSpace (fun (a : γ✝) => (g✝ a).right) encIn✝ (encList eSym) S✝

theorem Turing.MultiTapeTM.Universal.eTape_fields_deg : ComputableInDegree (fun (a : Tape) => (a.head, a.left, a.right)) eTape eTapeFields 1 1

theorem Turing.MultiTapeTM.Universal.eTape_left_deg : ComputableInDegree Tape.left eTape (encList eSym) 1 1

theorem Turing.MultiTapeTM.Universal.eTape_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget : γ → ℕ} {x0 : γ → ℤ} {x1 x2 : γ → List (Option ℕ)} (h0 : ComputableInSpace x0 encIn encIntUnary budget) (h1 : ComputableInSpace x1 encIn (encList eSym) budget) (h2 : ComputableInSpace x2 encIn (encList eSym) budget) : ComputableInSpace (fun (x : γ) => { head := x0 x, left := x1 x, right := x2 x }) encIn eTape budget

theorem Turing.MultiTapeTM.Universal.eTape_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → ℤ} {T0 S0 : γ → ℕ} {x1 : γ → List (Option ℕ)} {T1 S1 : γ → ℕ} {x2 : γ → List (Option ℕ)} {T2 S2 : γ → ℕ} (h0 : ComputableInO x0 encIn encIntUnary T0 S0) (h1 : ComputableInO x1 encIn (encList eSym) T1 S1) (h2 : ComputableInO x2 encIn (encList eSym) T2 S2) : ComputableInO (fun (x : γ) => { head := x0 x, left := x1 x, right := x2 x }) encIn eTape (fun (x : γ) => T0 x + (T1 x + T2 x)) fun (x : γ) => S0 x + (S1 x + S2 x)

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.eTapeFields : ℤ × List (Option ℕ) × List (Option ℕ) ↪ List Bool

The tuple of the fields of eTape.

def Turing.MultiTapeTM.Universal.eTape : Tape ↪ List Bool

Work tapes, as their fields.

theorem Turing.MultiTapeTM.Universal.eTape_head_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Tape} : ComputableInPolyTime g✝ encIn✝ eTape → ComputableInPolyTime (fun (a : γ✝) => (g✝ a).head) encIn✝ encIntUnary

theorem Turing.MultiTapeTM.Universal.eTape_right_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Tape} : ComputableInPolyTime g✝ encIn✝ eTape → ComputableInPolyTime (fun (a : γ✝) => (g✝ a).right) encIn✝ (encList eSym)

theorem Turing.MultiTapeTM.Universal.eTape_mk_deg : ComputableInDegree (fun (p : ℤ × List (Option ℕ) × List (Option ℕ)) => { head := p.1, left := p.2.1, right := p.2.2 }) eTapeFields eTape 1 1

theorem Turing.MultiTapeTM.Universal.eTape_left_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Tape} : ComputableInSpace g✝ encIn✝ eTape S✝ → ComputableInSpace (fun (a : γ✝) => (g✝ a).left) encIn✝ (encList eSym) S✝

theorem Turing.MultiTapeTM.Universal.eTape_left_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Tape} : ComputableInPolyTime g✝ encIn✝ eTape → ComputableInPolyTime (fun (a : γ✝) => (g✝ a).left) encIn✝ (encList eSym)

theorem Turing.MultiTapeTM.Universal.eTape_right_deg : ComputableInDegree Tape.right eTape (encList eSym) 1 1

theorem Turing.MultiTapeTM.Universal.eTape_head_inO : ComputableInO Tape.head eTape encIntUnary (fun (a : Tape) => (eTape a).length) fun (a : Tape) => (eTape a).length

theorem Turing.MultiTapeTM.Universal.eTape_right_inO : ComputableInO Tape.right eTape (encList eSym) (fun (a : Tape) => (eTape a).length) fun (a : Tape) => (eTape a).length

@[simp]

theorem Turing.MultiTapeTM.Universal.eTape_apply (a : Tape) : eTape a = eTapeFields (a.head, a.left, a.right)

theorem Turing.MultiTapeTM.Universal.eTape_left_inO : ComputableInO Tape.left eTape (encList eSym) (fun (a : Tape) => (eTape a).length) fun (a : Tape) => (eTape a).length

theorem Turing.MultiTapeTM.Universal.eTape_head_deg : ComputableInDegree Tape.head eTape encIntUnary 1 1

theorem Turing.MultiTapeTM.Universal.eTape_head_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Tape} : ComputableInSpace g✝ encIn✝ eTape S✝ → ComputableInSpace (fun (a : γ✝) => (g✝ a).head) encIn✝ encIntUnary S✝

theorem Turing.MultiTapeTM.Universal.eTape_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → ℤ} {x1 x2 : γ → List (Option ℕ)} (h0 : ComputableInPolyTime x0 encIn encIntUnary) (h1 : ComputableInPolyTime x1 encIn (encList eSym)) (h2 : ComputableInPolyTime x2 encIn (encList eSym)) : ComputableInPolyTime (fun (x : γ) => { head := x0 x, left := x1 x, right := x2 x }) encIn eTape

theorem Turing.MultiTapeTM.Universal.eCfg_mk_deg : ComputableInDegree (fun (p : Option ℕ × ℕ × List Tape) => { state := p.1, inputPos := p.2.1, workTapes := p.2.2 }) eCfgFields eCfg 1 1

theorem Turing.MultiTapeTM.Universal.eCfg_workTapes_deg : ComputableInDegree SCfg.workTapes eCfg (encList eTape) 1 1

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.eCfgFields : Option ℕ × ℕ × List Tape ↪ List Bool

The tuple of the fields of eCfg.

theorem Turing.MultiTapeTM.Universal.eCfg_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → Option ℕ} {T0 S0 x1 T1 S1 : γ → ℕ} {x2 : γ → List Tape} {T2 S2 : γ → ℕ} (h0 : ComputableInO x0 encIn eSym T0 S0) (h1 : ComputableInO x1 encIn encNat T1 S1) (h2 : ComputableInO x2 encIn (encList eTape) T2 S2) : ComputableInO (fun (x : γ) => { state := x0 x, inputPos := x1 x, workTapes := x2 x }) encIn eCfg (fun (x : γ) => T0 x + (T1 x + T2 x)) fun (x : γ) => S0 x + (S1 x + S2 x)

theorem Turing.MultiTapeTM.Universal.eCfg_state_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → SCfg} : ComputableInPolyTime g✝ encIn✝ eCfg → ComputableInPolyTime (fun (a : γ✝) => (g✝ a).state) encIn✝ eSym

theorem Turing.MultiTapeTM.Universal.eCfg_state_inO : ComputableInO SCfg.state eCfg eSym (fun (a : SCfg) => (eCfg a).length) fun (a : SCfg) => (eCfg a).length

def Turing.MultiTapeTM.Universal.eCfg : SCfg ↪ List Bool

Configurations, as their fields.

theorem Turing.MultiTapeTM.Universal.eCfg_state_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → SCfg} : ComputableInSpace g✝ encIn✝ eCfg S✝ → ComputableInSpace (fun (a : γ✝) => (g✝ a).state) encIn✝ eSym S✝

theorem Turing.MultiTapeTM.Universal.eCfg_inputPos_deg : ComputableInDegree SCfg.inputPos eCfg encNat 1 1

theorem Turing.MultiTapeTM.Universal.eCfg_inputPos_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → SCfg} : ComputableInPolyTime g✝ encIn✝ eCfg → ComputableInPolyTime (fun (a : γ✝) => (g✝ a).inputPos) encIn✝ encNat

@[simp]

theorem Turing.MultiTapeTM.Universal.eCfg_apply (a : SCfg) : eCfg a = eCfgFields (a.state, a.inputPos, a.workTapes)

theorem Turing.MultiTapeTM.Universal.eCfg_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → Option ℕ} {x1 : γ → ℕ} {x2 : γ → List Tape} (h0 : ComputableInPolyTime x0 encIn eSym) (h1 : ComputableInPolyTime x1 encIn encNat) (h2 : ComputableInPolyTime x2 encIn (encList eTape)) : ComputableInPolyTime (fun (x : γ) => { state := x0 x, inputPos := x1 x, workTapes := x2 x }) encIn eCfg

theorem Turing.MultiTapeTM.Universal.eCfg_fields_deg : ComputableInDegree (fun (a : SCfg) => (a.state, a.inputPos, a.workTapes)) eCfg eCfgFields 1 1

theorem Turing.MultiTapeTM.Universal.eCfg_workTapes_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → SCfg} : ComputableInPolyTime g✝ encIn✝ eCfg → ComputableInPolyTime (fun (a : γ✝) => (g✝ a).workTapes) encIn✝ (encList eTape)

theorem Turing.MultiTapeTM.Universal.eCfg_workTapes_inO : ComputableInO SCfg.workTapes eCfg (encList eTape) (fun (a : SCfg) => (eCfg a).length) fun (a : SCfg) => (eCfg a).length

theorem Turing.MultiTapeTM.Universal.eCfg_inputPos_inO : ComputableInO SCfg.inputPos eCfg encNat (fun (a : SCfg) => (eCfg a).length) fun (a : SCfg) => (eCfg a).length

theorem Turing.MultiTapeTM.Universal.eCfg_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget : γ → ℕ} {x0 : γ → Option ℕ} {x1 : γ → ℕ} {x2 : γ → List Tape} (h0 : ComputableInSpace x0 encIn eSym budget) (h1 : ComputableInSpace x1 encIn encNat budget) (h2 : ComputableInSpace x2 encIn (encList eTape) budget) : ComputableInSpace (fun (x : γ) => { state := x0 x, inputPos := x1 x, workTapes := x2 x }) encIn eCfg budget

theorem Turing.MultiTapeTM.Universal.eCfg_inputPos_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → SCfg} : ComputableInSpace g✝ encIn✝ eCfg S✝ → ComputableInSpace (fun (a : γ✝) => (g✝ a).inputPos) encIn✝ encNat S✝

theorem Turing.MultiTapeTM.Universal.eCfg_state_deg : ComputableInDegree SCfg.state eCfg eSym 1 1

theorem Turing.MultiTapeTM.Universal.eCfg_workTapes_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → SCfg} : ComputableInSpace g✝ encIn✝ eCfg S✝ → ComputableInSpace (fun (a : γ✝) => (g✝ a).workTapes) encIn✝ (encList eTape) S✝

theorem Turing.MultiTapeTM.Universal.state_inO : ComputableInO SCfg.state eCfg eSym (fun (c : SCfg) => (eCfg c).length) fun (c : SCfg) => (eCfg c).length

The state of a configuration, in linear time.

Reading, writing and moving on a work tape, in linear time

theorem Turing.MultiTapeTM.Universal.read_deg : ComputableInDegree Tape.read eTape eSym 1 1

The symbol under the head.

theorem Turing.MultiTapeTM.Universal.movePos_deg : ComputableInDegree (fun (t : Tape) => t.move SignType.pos) eTape eTape 1 1

A right move.

theorem Turing.MultiTapeTM.Universal.moveNeg_deg : ComputableInDegree (fun (t : Tape) => t.move SignType.neg) eTape eTape 1 1

A left move.

Applying actions to all work tapes

theorem Turing.MultiTapeTM.Universal.applyTapes_nil_right (ts : List Tape) : applyTapes ts [] = ts

Applying no actions leaves the work tapes unchanged.

theorem Turing.MultiTapeTM.Universal.Tape.apply_none_zero (t : Tape) : t.apply (none, 0) = t

The action that neither writes nor moves leaves a work tape unchanged.

Sizes

theorem Turing.MultiTapeTM.one_le_length_encIntUnary (z : ℤ) : 1 ≤ (encIntUnary z).length

An integer's unary encoding is nonempty. Its natural home is the Primitives module, next to length_encIntUnary; it is stated here, in that namespace, because Primitives has about 2,400 transitive importers against about 500 here.

theorem Turing.MultiTapeTM.Universal.length_eSym_read_le (t : Tape) : (eSym t.read).length ≤ (eTape t).length

The symbol under the head is no longer than the work tape.

All work tapes

theorem Turing.MultiTapeTM.Universal.applyTapes_inO : ComputableInO (Function.uncurry applyTapes) (encPair (encList eTape) (encList eTA)) (encList eTape) (fun (p : List Tape × List (Option (Option ℕ) × SignType)) => (p.1.length + 1) * (((encPair (encList eTape) (encList eTA)) p).length + 1)) fun (p : List Tape × List (Option (Option ℕ) × SignType)) => ((encPair (encList eTape) (encList eTA)) p).length

Applying actions to the work tapes, within time the number of work tapes times the length of the arguments, and linear space.

theorem Turing.MultiTapeTM.Universal.reads_inO : ComputableInO (fun (ts : List Tape) => List.map Tape.read ts) (encList eTape) (encList eSym) (fun (ts : List Tape) => (ts.length + 1) * (((encList eTape) ts).length + 1)) fun (ts : List Tape) => ((encList eTape) ts).length

The symbols under the heads of the work tapes, within time the number of work tapes times their length, and linear space.

The input head

theorem Turing.MultiTapeTM.Universal.moveInput_inO : ComputableInO (fun (q : ℕ × Option ℕ × SignType) => moveInput q.1 q.2.1 q.2.2) (encPair encNat (encPair eSym encSign)) encNat (fun (q : ℕ × Option ℕ × SignType) => ((encPair encNat (encPair eSym encSign)) q).length + ((encNat q.1).length + 1) ^ 2) fun (q : ℕ × Option ℕ × SignType) => ((encPair encNat (encPair eSym encSign)) q).length + 1

Moving the input head, charging binary arithmetic only to the encoded position length.

A step without the input

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.WCtx : Type

The context of a step without the input: the description, the configuration and the symbol under the input head.

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.eWCtx : WCtx ↪ List Bool

The encoding of contexts without the input.

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.WCtx.desc (c : WCtx) : Desc

The description of a context without the input.

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.WCtx.cfg (c : WCtx) : SCfg

The configuration of a context without the input.

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.WCtx.sym (c : WCtx) : Option ℕ

The symbol under the input head, in a context without the input.

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.Ctx : Type

The context of a step: the description, the input and the configuration.

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.eCtx : Ctx ↪ List Bool

The encoding of contexts.

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.Ctx.desc (c : Ctx) : Desc

The description of a context.

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.Ctx.input (c : Ctx) : List ℕ

The input of a context.

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.Ctx.cfg (c : Ctx) : SCfg

The configuration of a context.

def Turing.MultiTapeTM.Universal.wTime (c : WCtx) : ℕ

A step without input lookup: tape passes and description comparisons are linear in context length; only binary input-head arithmetic is quadratic in its own encoded length.

Rules for fun_prop

theorem Turing.MultiTapeTM.Universal.stepWith_inO : ComputableInO (fun (c : WCtx) => stepWith c.desc c.cfg c.sym) eWCtx (encPair eCfg eSym) wTime fun (c : WCtx) => (eWCtx c).length

One step of the simulation without the input, within the time wTime and linear space. The machine is assembled from the definition of stepWith, and its bounds are checked once.

A step

def Turing.MultiTapeTM.Universal.stepTime (c : Ctx) : ℕ

The step bound separates linear configuration passes from a streaming input lookup with binary countdown arithmetic. In particular, the whole configuration length is never squared.

theorem Turing.MultiTapeTM.Universal.step_inO : ComputableInO (fun (c : Ctx) => step c.desc c.input c.cfg) eCtx (encPair eCfg eSym) stepTime fun (c : Ctx) => (eCtx c).length

One step of the simulation, on contexts, within the time stepTime and linear space: the symbol under the input head, and the step without the input.