Step machines with plain resource certificates

The halting test, step and initial state have charged plain resource certificates. Their realizing machines are normalized only within this internal compiler proof. The input head stays where the step machine has it between rounds, so each round pays for its callbacks and state, not a new traversal of the whole input.

Whole-run conclusions use independent, uncharged ComputableInBigO bounds. An emitter may write an unbounded output with constant workspace; no bound on the whole output is added.

Main definitions

• Turing.MultiTapeTM.encMove, .encPeek: the unchanged encodings used by the compiler.
• Turing.StepMachine.ResourceCertificate: charged plain certificates for halt and step.

Main results

• Turing.StepMachine.ResourceCertificate.computableInBigO_of_init: compile a computed initial state, retaining the original time/workspace formulas and halting/output hypotheses.
• Turing.StepMachine.ResourceCertificate.computableInBigO: the fixed-initial-state case.

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 : ComputableInLinearTimeAndSpace stepFlagWord encBool encBits

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} : ComputableInO 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} : ComputableInO 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} : ComputableInO (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.

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

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

Plain certificates for the halting test and step. Each callback charges its encoded result to S; the whole-run output is not charged to workspace.

• computable_halt : MultiTapeTM.ComputableInO m.halt encS MultiTapeTM.encBool T S
• computable_step : MultiTapeTM.ComputableInO (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.ResourceCertificate.computableInBigO_of_init {σ γ ω : Type} {encS : σ ↪ List Bool} {encIn : γ ↪ List Bool} {encOut : ω ↪ List Bool} {m : StepMachine σ Bool Bool} {T S : σ → ℕ} (hm : m.ResourceCertificate encS T S) {init : γ → σ} {TI SI : γ → ℕ} (hinit : MultiTapeTM.ComputableInO 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.ComputableInBigO 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

Compile a resource-certified step machine. If 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 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.ResourceCertificate.computableInBigO {σ γ ω : Type} {encS : σ ↪ List Bool} {encIn : γ ↪ List Bool} {encOut : ω ↪ List Bool} {m : StepMachine σ Bool Bool} {T S : σ → ℕ} (hm : m.ResourceCertificate 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.ComputableInBigO g encIn encOut (fun (x : γ) => (rounds x + 1) * (tMax x + sMax x + 1) + (encIn x).length) sMax

Compile a resource-certified step machine, from its initial state: as Turing.StepMachine.ResourceCertificate.computableInBigO_of_init, in time O((rounds x + 1) * (tMax x + sMax x + 1) + n) and space O(sMax x).