Resource certificates for read-machine simulations

If the halting test, the address and the step of a read machine have plain charged resource certificates, then the step of Turing.ReadMachine.toStepMachine has a resource certificate on its states, which add the position of the head: the work space grows by the length of the position in binary, and the time by a factor of the position, to compare it with the address.

Main results

• Turing.ReadMachine.pairFalse_inSpace, Turing.ReadMachine.comp_pairFalse_inSpace: evaluating a function of a state and a bit at the bit false within the space budget of the step.
• Turing.ReadMachine.toStepMachine_resourceCertificate: the simulating step machine has a plain resource certificate.

Computing within fixed budgets

theorem Turing.ReadMachine.budget_comp {γ β δ : Type} {encIn : γ ↪ List Bool} {encB : β ↪ List Bool} {encD : δ ↪ List Bool} {Bt Bs : γ → ℕ} {f : γ → β} {g : β → δ} {Tg Sg : β → ℕ} (hg : MultiTapeTM.ComputableInO g encB encD Tg Sg) (hf : MultiTapeTM.ComputableInO f encIn encB Bt Bs) (hT : MultiTapeTM.BigOLe (fun (x : γ) => Tg (f x)) Bt) (hS : MultiTapeTM.BigOLe (fun (x : γ) => Sg (f x)) Bs) : MultiTapeTM.ComputableInO (fun (x : γ) => g (f x)) encIn encD Bt Bs

Composition within the budgets.

theorem Turing.ReadMachine.budget_comp_linear {γ β δ : Type} {encIn : γ ↪ List Bool} {encB : β ↪ List Bool} {encD : δ ↪ List Bool} {Bt Bs : γ → ℕ} {f : γ → β} {g : β → δ} (hg : MultiTapeTM.ComputableInO g encB encD (fun (b : β) => (encB b).length) fun (b : β) => (encB b).length) (hf : MultiTapeTM.ComputableInO f encIn encB Bt Bs) (hst : MultiTapeTM.BigOLe Bs Bt) : MultiTapeTM.ComputableInO (fun (x : γ) => g (f x)) encIn encD Bt Bs

Composition with a map computed in linear time and space, within the budgets.

theorem Turing.ReadMachine.budget_prod {γ β δ : Type} {encIn : γ ↪ List Bool} {encB : β ↪ List Bool} {encD : δ ↪ List Bool} {Bt Bs : γ → ℕ} {f : γ → β} {g : γ → δ} (hf : MultiTapeTM.ComputableInO f encIn encB Bt Bs) (hg : MultiTapeTM.ComputableInO g encIn encD Bt Bs) : MultiTapeTM.ComputableInO (fun (x : γ) => (f x, g x)) encIn (MultiTapeTM.encPair encB encD) Bt Bs

Pairs within the budgets.

theorem Turing.ReadMachine.budget_ite {γ β : Type} {encIn : γ ↪ List Bool} {encB : β ↪ List Bool} {Bt Bs : γ → ℕ} {c : γ → Bool} {f g : γ → β} (hc : MultiTapeTM.ComputableInO c encIn MultiTapeTM.encBool Bt Bs) (hf : MultiTapeTM.ComputableInO f encIn encB Bt Bs) (hg : MultiTapeTM.ComputableInO g encIn encB Bt Bs) : MultiTapeTM.ComputableInO (fun (x : γ) => if c x = true then f x else g x) encIn encB Bt Bs

Conditionals within the budgets.

theorem Turing.ReadMachine.budget_const {γ β : Type} {encIn : γ ↪ List Bool} {encB : β ↪ List Bool} {Bt Bs : γ → ℕ} (b : β) (hl : MultiTapeTM.BigOLe (fun (x : γ) => (encIn x).length) Bs) (hst : MultiTapeTM.BigOLe Bs Bt) : MultiTapeTM.ComputableInO (fun (x : γ) => b) encIn encB Bt Bs

A constant within the budgets.

theorem Turing.ReadMachine.budget_finite {γ β δ : Type} {encIn : γ ↪ List Bool} {encB : β ↪ List Bool} {encD : δ ↪ List Bool} {Bt Bs : γ → ℕ} {f : γ → β} [Finite β] (g : β → δ) (hf : MultiTapeTM.ComputableInO f encIn encB Bt Bs) (hst : MultiTapeTM.BigOLe Bs Bt) : MultiTapeTM.ComputableInO (fun (x : γ) => g (f x)) encIn encD Bt Bs

A function of finitely many values, within the budgets.

theorem Turing.ReadMachine.pairFalse_inSpace {α : Type} {enc : α ↪ List Bool} {B : α × Bool → ℕ} (hB : ∀ (x : α), ((MultiTapeTM.encPair enc MultiTapeTM.encBool) (x, false)).length ≤ B (x, false)) : MultiTapeTM.ComputableTidilyInSpace (fun (x : α) => (x, false)) enc (MultiTapeTM.encPair enc MultiTapeTM.encBool) fun (x : α) => B (x, false)

Pairing a state with the bit false, within any space budget at least the encoded pair length.

theorem Turing.ReadMachine.comp_pairFalse_inSpace {β : Type} {encB : β ↪ List Bool} {α : Type} {enc : α ↪ List Bool} {B : α × Bool → ℕ} (hB : ∀ (x : α), ((MultiTapeTM.encPair enc MultiTapeTM.encBool) (x, false)).length ≤ B (x, false)) {f : α × Bool → β} (h : MultiTapeTM.ComputableTidilyInSpace f (MultiTapeTM.encPair enc MultiTapeTM.encBool) encB B) : MultiTapeTM.ComputableTidilyInSpace (fun (x : α) => f (x, false)) enc encB fun (x : α) => B (x, false)

Evaluating a function of a state and a bit at the bit false, within the space budget of the step.

@[reducible, inline]

abbrev Turing.ReadMachine.encStepIn {σ : Type} (encS : σ ↪ List Bool) : (σ × ℕ) × Option Bool ↪ List Bool

The input of a step of the simulating machine.

@[reducible, inline]

abbrev Turing.ReadMachine.inLen {σ : Type} (encS : σ ↪ List Bool) (p : (σ × ℕ) × Option Bool) : ℕ

The length of the input of a step.

@[reducible, inline]

abbrev Turing.ReadMachine.spaceB {σ : Type} (encS : σ ↪ List Bool) (S : σ → ℕ) (p : (σ × ℕ) × Option Bool) : ℕ

The space budget of a step.

@[reducible, inline]

abbrev Turing.ReadMachine.timeB {σ : Type} (encS : σ ↪ List Bool) (T S : σ → ℕ) (p : (σ × ℕ) × Option Bool) : ℕ

The time budget of a step.

theorem Turing.ReadMachine.spaceB_le_timeB {σ : Type} {encS : σ ↪ List Bool} {T S : σ → ℕ} (p : (σ × ℕ) × Option Bool) : spaceB encS S p ≤ timeB encS T S p

theorem Turing.ReadMachine.inLen_le_spaceB {σ : Type} {encS : σ ↪ List Bool} {S : σ → ℕ} (p : (σ × ℕ) × Option Bool) : inLen encS p ≤ spaceB encS S p

theorem Turing.ReadMachine.inLen_le_timeB {σ : Type} {encS : σ ↪ List Bool} {T S : σ → ℕ} (p : (σ × ℕ) × Option Bool) : inLen encS p ≤ timeB encS T S p

theorem Turing.ReadMachine.budget_proj {σ : Type} {encS : σ ↪ List Bool} {T S : σ → ℕ} : MultiTapeTM.ComputableInO (fun (p : (σ × ℕ) × Option Bool) => p.1.1) (encStepIn encS) encS (timeB encS T S) (spaceB encS S) ∧ MultiTapeTM.ComputableInO (fun (p : (σ × ℕ) × Option Bool) => p.1.2) (encStepIn encS) MultiTapeTM.encNat (timeB encS T S) (spaceB encS S) ∧ MultiTapeTM.ComputableInO (fun (p : (σ × ℕ) × Option Bool) => p.2) (encStepIn encS) (MultiTapeTM.encOption MultiTapeTM.encBool) (timeB encS T S) (spaceB encS S)

The projections of the input are within the budgets.

theorem Turing.ReadMachine.lt_bigOLe {σ : Type} {encS : σ ↪ List Bool} {T S : σ → ℕ} {u : (σ × ℕ) × Option Bool → ℕ} (h : MultiTapeTM.BigOLe u (spaceB encS S)) : MultiTapeTM.BigOLe (fun (p : (σ × ℕ) × Option Bool) => (p.1.2 + 1) * (u p + 1) ^ 2) (timeB encS T S)

The time of a comparison with the head position is within the time budget.

theorem Turing.ReadMachine.sq_bigOLe {σ : Type} {encS : σ ↪ List Bool} {T S : σ → ℕ} {u : (σ × ℕ) × Option Bool → ℕ} (h : MultiTapeTM.BigOLe u (spaceB encS S)) : MultiTapeTM.BigOLe (fun (p : (σ × ℕ) × Option Bool) => (u p + 1) ^ 2) (timeB encS T S)

A square of something within the space budget is within the time budget.

def Turing.ReadMachine.stepBy {σ : Type} (m : ReadMachine σ) (p : (σ × ℕ) × Option Bool) : (σ × ℕ) × SignType × List Bool

The step of the simulating machine, written with its components.

theorem Turing.ReadMachine.stepBy_eq {σ : Type} {m : ReadMachine σ} (p : (σ × ℕ) × Option Bool) : m.stepBy p = m.toStepMachine.step p.1 p.2

@[reducible, inline]

abbrev Turing.ReadMachine.stateT {σ : Type} (encS : σ ↪ List Bool) (T S : σ → ℕ) (q : σ × ℕ) : ℕ

The time bound of a state of the simulating machine.

@[reducible, inline]

abbrev Turing.ReadMachine.stateS {σ : Type} (encS : σ ↪ List Bool) (S : σ → ℕ) (q : σ × ℕ) : ℕ

The space bound of a state of the simulating machine.

theorem Turing.ReadMachine.inLen_le {σ : Type} {encS : σ ↪ List Bool} (p : (σ × ℕ) × Option Bool) : inLen encS p ≤ 2 * ((MultiTapeTM.encPair encS MultiTapeTM.encNat) p.1).length + 3

theorem Turing.ReadMachine.toStepMachine_resourceCertificate {σ : Type} {m : ReadMachine σ} {encS : σ ↪ List Bool} {T S : σ → ℕ} (hhalt : MultiTapeTM.ComputableInO m.halt encS MultiTapeTM.encBool T S) (haddr : MultiTapeTM.ComputableInO m.addr encS (MultiTapeTM.encOption MultiTapeTM.encNat) T S) (hstep : MultiTapeTM.ComputableInO (fun (p : σ × Bool) => m.step p.1 p.2) (MultiTapeTM.encPair encS MultiTapeTM.encBool) (MultiTapeTM.encPair encS MultiTapeTM.encBits) (fun (p : σ × Bool) => T p.1) fun (p : σ × Bool) => S p.1) : m.toStepMachine.ResourceCertificate (MultiTapeTM.encPair encS MultiTapeTM.encNat) (stateT encS T S) (stateS encS S)

The simulating step machine has a resource certificate, if the halting test, address and step have plain resource certificates with the given state bounds.