Step machines of tidily computable functions

A step machine (Turing.StepMachine) whose initial state, halting test and step are tidily computable is tidily computable. Each step costs the time of the step function and of a few operations linear in the size of the state, but nothing for the input: the realizing machine keeps its input head where the step machine has it. The space is that of the step function plus the size of the states.

Main definitions

• Turing.MultiTapeTM.encMove: the encoding of moves of the input head.
• Turing.MultiTapeTM.encPeek: the encoding of a state behind the symbol under the input head.
• Turing.StepMachine.Tidy: step machines with tidily computable halting test and step.

Main results

• Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.stepMachine: step machines of tidily computable functions are tidily computable, with no cost for the input head.
• Turing.StepMachine.Tidy.computableTidilyInTimeAndSpace: the same for tidy step machines, with the bounds of the steps along the run.

A flag as a word

def Turing.MultiTapeTM.stepFlagWord (b : Bool) : List Bool

A flag as a word: [true] if set, blank otherwise.

theorem Turing.MultiTapeTM.linear_stepFlagWord : ComputableTidilyInLinearTimeAndSpace stepFlagWord encBool encBits

Tidy machines on selected tapes

theorem Turing.MultiTapeTM.transformsTapes_outputToWord {β : Type u_1} {δ : Type u_2} {k K : ℕ} {S : Type u_3} {tm : MultiTapeTM k Bool S} {encB : β ↪ List Bool} {encD : δ ↪ List Bool} {f : β → δ} {t s : β → ℕ} (h : tm.ComputesFunTidilyInTimeAndSpace encB encD f t s) {e : Fin (k + 1) ↪ Fin K} {V : Fin K} (he : e (Fin.last k) = V) (b : β) : (tm.outputToWord.extendTapes e).TransformsTapes (fun (inp : List Bool) (ws : Fin K → List Bool) => inp = encB b ∧ ws = fun (x : Fin K) => []) (fun (x : List Bool) (x_1 ws' : Fin K → List Bool) (em : List Bool) => ws' = Function.update (fun (x : Fin K) => []) V (encD (f b)) ∧ em = []) (t b + (encD (f b)).length + 2) (s b + 2 * (encD (f b)).length + 2 * K + 3)

A tidy machine writing its output to tape V.

theorem Turing.MultiTapeTM.transformsTapes_inputFromWord_fun {β : Type u_1} {δ : Type u_2} {k K : ℕ} {S : Type u_3} {tm : MultiTapeTM k Bool S} {encB : β ↪ List Bool} {encD : δ ↪ List Bool} {f : β → δ} {t s : β → ℕ} (h : tm.ComputesFunTidilyInTimeAndSpace encB encD f t s) {e : Fin (k + 2) ↪ Fin K} {V : Fin K} (he : e (Fin.natAdd k 0) = V) (b : β) : ((tm.inputFromWord true).extendTapes e).TransformsTapes (fun (x : List Bool) (ws : Fin K → List Bool) => ws = Function.update (fun (x : Fin K) => []) V (encB b)) (fun (x : List Bool) (ws ws' : Fin K → List Bool) (em : List Bool) => ws' = ws ∧ em = encD (f b)) (t b + 4) (s b + 2 * (encB b).length + 3 * K + 10)

A tidy machine run on the word on tape V, emitting its output.

theorem Turing.MultiTapeTM.transformsTapes_onWords {β : Type u_1} {δ : Type u_2} {k K : ℕ} {S : Type u_3} {tm : MultiTapeTM k Bool S} {encB : β ↪ List Bool} {encD : δ ↪ List Bool} {f : β → δ} {t s : β → ℕ} (h : tm.ComputesFunTidilyInTimeAndSpace encB encD f t s) {e : Fin (k + 1 + 2) ↪ Fin K} {V O : Fin K} (hi : e (Fin.natAdd (k + 1) 0) = V) (ho : e (Fin.castAdd 2 (Fin.last k)) = O) (b : β) : ((tm.onWords true).extendTapes e).TransformsTapes (fun (x : List Bool) (ws : Fin K → List Bool) => ws = Function.update (fun (x : Fin K) => []) V (encB b)) (fun (x : List Bool) (ws ws' : Fin K → List Bool) (em : List Bool) => ws' = Function.update ws O (encD (f b)) ∧ em = []) (t b + (encD (f b)).length + 6) (s b + 2 * (encB b).length + 2 * (encD (f b)).length + 4 * K + 15)

A tidy machine run on the word on tape V, writing its output to tape O.

def Turing.MultiTapeTM.encMove : SignType ↪ List Bool

Moves of the input head: none, to the left, to the right.

@[simp]

theorem Turing.MultiTapeTM.moveOfCell_encMove (m : SignType) : moveOfCell (encMove m).head? = m

theorem Turing.MultiTapeTM.peekWord_injective : Function.Injective peekWord

def Turing.MultiTapeTM.encPeek {τ : Type u_1} (enc : τ ↪ List Bool) : Option Bool × τ ↪ List Bool

A value behind the symbol under the input head, recorded by peekWord.

@[simp]

theorem Turing.MultiTapeTM.encPeek_apply {τ : Type u_1} (enc : τ ↪ List Bool) (p : Option Bool × τ) : (encPeek enc) p = peekWord p.1 ++ enc p.2

Converting to and from encPeek

theorem Turing.MultiTapeTM.peek_snd {τ : Type} {enc : τ ↪ List Bool} : ComputableTidilyInO Prod.snd (encPeek enc) enc (fun (p : Option Bool × τ) => ((encPeek enc) p).length) fun (p : Option Bool × τ) => ((encPeek enc) p).length

The value behind the recorded symbol.

theorem Turing.MultiTapeTM.peek_fst {τ : Type} {enc : τ ↪ List Bool} : ComputableTidilyInO Prod.fst (encPeek enc) (encOption encBool) (fun (p : Option Bool × τ) => ((encPeek enc) p).length) fun (p : Option Bool × τ) => ((encPeek enc) p).length

The recorded symbol.

theorem Turing.MultiTapeTM.peek_none {τ : Type} {enc : τ ↪ List Bool} : ComputableTidilyInO (fun (t : τ) => (none, t)) enc (encPeek enc) (fun (t : τ) => (enc t).length) fun (t : τ) => (enc t).length

No symbol recorded in front of a value.

theorem Turing.MultiTapeTM.constZero {α β : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} (b : β) : ComputableTidilyInO (fun (x : α) => b) encIn encMid (fun (a : α) => (encIn a).length) fun (x : α) => 0

A constant, in zero space.

The parts of a round

@[reducible, inline]

abbrev Turing.MultiTapeTM.encAug {σ : Type} (encS : σ ↪ List Bool) : σ × SignType ↪ List Bool

The state and its pending move.

The theorem

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.stepMachine {σ γ ω : Type} {encS : σ ↪ List Bool} {encIn : γ ↪ List Bool} {encOut : ω ↪ List Bool} (init : γ → σ) (halt : σ → Bool) (step : σ → Option Bool → σ × SignType × List Bool) (g : γ → ω) (rounds : γ → ℕ) {TI SI : γ → ℕ} {TH SH : σ → ℕ} {TS SS : σ × Option Bool → ℕ} (hinit : ComputableTidilyInO init encIn encS TI SI) (hhalt : ComputableTidilyInO halt encS encBool TH SH) (hstep : ComputableTidilyInO (fun (p : σ × Option Bool) => step p.1 p.2) (encPair encS (encOption encBool)) (encPair encS (encPair encMove encBits)) TS SS) (hrounds : ∀ (x : γ), { init := init x, halt := halt, step := step }.HaltsAt (encIn x) (rounds x)) (hg : ∀ (x : γ), encOut (g x) = ({ init := init x, halt := halt, step := step }.run (encIn x) (rounds x)).out) {tMax sMax lMax : γ → ℕ} (htMax : ∀ (x : γ), ∀ i ≤ rounds x, TS (({ init := init x, halt := halt, step := step }.run (encIn x) i).state, inputSymbolAt (encIn x) ({ init := init x, halt := halt, step := step }.run (encIn x) i).pos) + TH ({ init := init x, halt := halt, step := step }.run (encIn x) i).state ≤ tMax x) (hsMax : ∀ (x : γ), ∀ i ≤ rounds x, SS (({ init := init x, halt := halt, step := step }.run (encIn x) i).state, inputSymbolAt (encIn x) ({ init := init x, halt := halt, step := step }.run (encIn x) i).pos) + SH ({ init := init x, halt := halt, step := step }.run (encIn x) i).state ≤ sMax x) (hlMax : ∀ (x : γ), ∀ i ≤ rounds x, (encS ({ init := init x, halt := halt, step := step }.run (encIn x) i).state).length ≤ lMax x) : ∃ (c : ℕ), ComputableTidilyInTimeAndSpace g encIn encOut (fun (x : γ) => c * (TI x + (rounds x + 1) * (tMax x + lMax x + 1) + (encIn x).length)) fun (x : γ) => c * (SI x + sMax x + lMax x + 1)

Step machines of tidily computable functions are tidily computable. Let the step machine ⟨init x, halt, step⟩ halt on the input encIn x after rounds x steps with the output encOut (g x). If init, halt and step are tidily computable, then so is g, in time O(TI x + (rounds x + 1) * (tMax x + lMax x + 1) + n) and space O(SI x + sMax x + lMax x + 1), where tMax, sMax bound the time and space of halt and step along the run and lMax the size of the states. The input head is never rewound between steps.

structure Turing.StepMachine.Tidy {σ : Type} (m : StepMachine σ Bool Bool) (encS : σ ↪ List Bool) (T S : σ → ℕ) : Prop

Tidy step machines: the halting test and the step of m are tidily computable within T and S of the state.

• computable_halt : MultiTapeTM.ComputableTidilyInO m.halt encS MultiTapeTM.encBool T S
• computable_step : MultiTapeTM.ComputableTidilyInO (fun (p : σ × Option Bool) => m.step p.1 p.2) (MultiTapeTM.encPair encS (MultiTapeTM.encOption MultiTapeTM.encBool)) (MultiTapeTM.encPair encS (MultiTapeTM.encPair MultiTapeTM.encMove MultiTapeTM.encBits)) (fun (p : σ × Option Bool) => T p.1) fun (p : σ × Option Bool) => S p.1

def Turing.StepMachine.withInit {σ : Type u_1} {Γ : Type u_2} {Out : Type u_3} (m : StepMachine σ Γ Out) (s : σ) : StepMachine σ Γ Out

The step machine m started in the state s.

theorem Turing.StepMachine.Tidy.computableTidilyInTimeAndSpace_of_init {σ γ ω : Type} {encS : σ ↪ List Bool} {encIn : γ ↪ List Bool} {encOut : ω ↪ List Bool} {m : StepMachine σ Bool Bool} {T S : σ → ℕ} (hm : m.Tidy encS T S) {init : γ → σ} {TI SI : γ → ℕ} (hinit : MultiTapeTM.ComputableTidilyInO init encIn encS TI SI) (g : γ → ω) (rounds : γ → ℕ) (hrounds : ∀ (x : γ), (m.withInit (init x)).HaltsAt (encIn x) (rounds x)) (hg : ∀ (x : γ), encOut (g x) = ((m.withInit (init x)).run (encIn x) (rounds x)).out) {tMax sMax : γ → ℕ} (hmax : ∀ (x : γ), ∀ i ≤ rounds x, T ((m.withInit (init x)).run (encIn x) i).state ≤ tMax x ∧ S ((m.withInit (init x)).run (encIn x) i).state ≤ sMax x) : MultiTapeTM.ComputableTidilyInBigO g encIn encOut (fun (x : γ) => TI x + (rounds x + 1) * (tMax x + sMax x + SI x + 1) + (encIn x).length) fun (x : γ) => SI x + sMax x

Tidy step machines compute tidily. If the tidy step machine m, started in the state init x computed within TI x and SI x, halts on encIn x after rounds x steps with the output encOut (g x), and its steps along the run take time tMax x and space sMax x, then g is tidily computable in time O(TI x + (rounds x + 1) * (tMax x + sMax x + SI x + 1) + n) and space O(SI x + sMax x): the initial state bounds the states along the run, besides the steps.

theorem Turing.StepMachine.Tidy.computableTidilyInTimeAndSpace {σ γ ω : Type} {encS : σ ↪ List Bool} {encIn : γ ↪ List Bool} {encOut : ω ↪ List Bool} {m : StepMachine σ Bool Bool} {T S : σ → ℕ} (hm : m.Tidy encS T S) (g : γ → ω) (rounds : γ → ℕ) (hrounds : ∀ (x : γ), m.HaltsAt (encIn x) (rounds x)) (hg : ∀ (x : γ), encOut (g x) = (m.run (encIn x) (rounds x)).out) {tMax sMax : γ → ℕ} (hmax : ∀ (x : γ), ∀ i ≤ rounds x, T (m.run (encIn x) i).state ≤ tMax x ∧ S (m.run (encIn x) i).state ≤ sMax x) : MultiTapeTM.ComputableTidilyInBigO g encIn encOut (fun (x : γ) => (rounds x + 1) * (tMax x + sMax x + 1) + (encIn x).length) sMax

Tidy step machines compute tidily, from their initial state: as Turing.StepMachine.Tidy.computableTidilyInTimeAndSpace_of_init, in time O((rounds x + 1) * (tMax x + sMax x + 1) + n) and space O(sMax x).