The universal machine within a space budget

Turing.MultiTapeTM.Universal.budgetedUniversal (d, x, t, b) runs the machine described by d on x for t steps, as the universal function does, but within the budget b: a step whose configuration of the simulation is encoded by more than b bits is not taken, and the simulation stays at the last configuration within the budget (Turing.MultiTapeTM.Universal.budgetStep). It returns the first two symbols of the output and whether the machine has halted: enough to tell whether the output is a single given symbol, without storing an output that may be as long as the run.

It is computed by the in-place run of the universal machine (Turing.MultiTapeTM.Universal.computableTidilyInTimeAndSpace_universal_inPlace): the same multi-pass fold over the input, one pass per step, reading the symbol under the simulated input head by counting down the symbols of x, with the budget and the first two symbols of the output added to its state, and a budget test at the end of each pass. So it is tidily computable within space linear in Turing.MultiTapeTM.Universal.budgetSpace: the description, the budget, the number of steps and the length of x in binary, and the largest symbol of x (Turing.MultiTapeTM.Universal.computableTidilyInO_budgetedUniversal), never the length of x itself or the space the described machine would use beyond the budget.

Within the budget it agrees with the universal function (Turing.MultiTapeTM.Universal.budgetedUniversal_eq_of_le), and on the description of a machine it returns the first two symbols of the output of the machine whenever the bound Turing.MultiTapeTM.Universal.cfgSpace on the configurations of the simulation, linear in the cells the machine visits, is within the budget (Turing.MultiTapeTM.Universal.budgetedUniversal_desc).

Main definitions

• Turing.MultiTapeTM.Universal.budgetStep: a step of the simulation within a budget.
• Turing.MultiTapeTM.Universal.budgetedUniversal: the universal function within a space budget.
• Turing.MultiTapeTM.Universal.budgetSpace: the bound on the states of its fold.

Main results

• Turing.MultiTapeTM.Universal.budgetStep_iterate: the run within the budget is the run of the simulation up to some step.
• Turing.MultiTapeTM.Universal.budgetedUniversal_eq_of_le, Turing.MultiTapeTM.Universal.budgetedUniversal_desc: within the budget, the universal function.
• Turing.MultiTapeTM.Universal.computableTidilyInTimeAndSpace_budgetedUniversal, Turing.MultiTapeTM.Universal.computableTidilyInO_budgetedUniversal: it is tidily computable in space linear in budgetSpace.
• Turing.MultiTapeTM.Universal.budgetSpace_le: budgetSpace is linear in the description, the budget and the lengths of the number of steps and of the length of the input in binary, plus the largest symbol of the input.

Implementation notes

The fold reuses the parts of the in-place fold (Turing.MultiTapeTM.Universal.foldNext, Turing.MultiTapeTM.Universal.stepAt, Turing.MultiTapeTM.Universal.foldEnd) on the state of the in-place fold, and its proof of computability adapts that of Turing.MultiTapeTM.Universal.computableTidilyInTimeAndSpace_universal_inPlace, by Christian Reitwiessner. The events of the input, the extraction of the parts the initial state reads, the bounds on the countdown and the simplified time bound restate private lemmas and the extracting transducer of the module Complexity.Computability.Machines.Turing.MultiTape.Universal.InPlace for the encoding Turing.MultiTapeTM.Universal.eInS, whose input ends in a budget.

References

• M. Sipser, Introduction to the Theory of Computation, Theorem 9.3: the simulation within a space budget in the proof of the space hierarchy theorem.

Simulating within a budget

def Turing.MultiTapeTM.Universal.budgetStep (d : Desc) (x : List ℕ) (b : ℕ) (p : SCfg × List ℕ) : SCfg × List ℕ

A step of the simulation within the budget b, keeping the first two symbols of the output: the step of the machine described by d on x, unless the configuration it reaches is encoded by more than b bits, in which case the configuration and the output stay.

def Turing.MultiTapeTM.Universal.budgetedUniversal (i : Desc × List ℕ × ℕ × ℕ) : List ℕ × Bool

The universal function within a space budget. The machine described by i.1 runs on the input i.2.1 for i.2.2.1 steps within the budget i.2.2.2 (budgetStep); the result is the first two symbols of its output and whether it has halted.

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.eInS : Desc × List ℕ × ℕ × ℕ ↪ List Bool

The encoding of inputs of budgetedUniversal: the number of steps in binary, the budget in unary.

theorem Turing.MultiTapeTM.Universal.budgetStep_iterate (d : Desc) (x : List ℕ) (b i : ℕ) : ∃ j ≤ i, (budgetStep d x b)^[i] (init d, []) = (run d x j, List.take 2 ((stepOut d x)^[j] (init d, [])).2) ∧ (j = 0 ∨ (eCfg (run d x j)).length ≤ b)

The run within the budget is the run of the simulation up to some step, with the first two symbols of its output; past the start, that configuration is within the budget.

theorem Turing.MultiTapeTM.Universal.budgetedUniversal_eq_of_le (d : Desc) (x : List ℕ) (b : ℕ) {t : ℕ} (hb : ∀ j < t, (eCfg (run d x (j + 1))).length ≤ b) : budgetedUniversal (d, x, t, b) = (List.take 2 (universal (d, x, t)).1, (universal (d, x, t)).2)

Within the budget, the universal function: if every configuration of the simulation within t steps is encoded within b bits, budgetedUniversal returns the first two symbols of the output of the universal function and whether the machine has halted.

theorem Turing.MultiTapeTM.Universal.budgetedUniversal_desc {k : ℕ} {Symbol S : Type} [Fintype S] [Fintype Symbol] (eS : S ↪ ℕ) (eY : Symbol ↪ ℕ) (tm : MultiTapeTM k Symbol S) (x : List Symbol) (t b : ℕ) (hb : cfgSpace (desc eS eY tm) (List.map (⇑eY) x) t ≤ b) : budgetedUniversal (desc eS eY tm, List.map (⇑eY) x, t, b) = (List.take 2 (List.map (⇑eY) (runFrom (tm.initCfg x) t).output), (runFrom (tm.initCfg x) t).state.isNone)

On the description of a machine, within a budget that holds the configurations of the simulation (Turing.MultiTapeTM.Universal.cfgSpace, linear in the space of the machine), the budgeted universal function returns the first two symbols of the numbered output of the machine and whether it has halted.

The fold within a budget

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.SSt : Type

The states of the fold within a budget: the state of the in-place fold (Turing.MultiTapeTM.Universal.St), the budget and the first two symbols of the output so far.

The events of the input, and the parts of the input the initial state reads

The lemmas of this section restate private lemmas of the module Complexity.Computability.Machines.Turing.MultiTape.Universal.InPlace for the encoding Turing.MultiTapeTM.Universal.eInS, whose input ends in a budget.

The size of the states

def Turing.MultiTapeTM.Universal.budgetSpace (i : Desc × List ℕ × ℕ × ℕ) : ℕ

A bound on the states of the fold within the budget b: the description, a configuration within the budget or the initial one, the number of steps and the position of the input head in binary, the largest symbol of the input, the budget in unary and two symbols of the output.

The parts of the fold, within bounds in the length of the state

The universal machine within a space budget

theorem Turing.MultiTapeTM.Universal.computableTidilyInTimeAndSpace_budgetedUniversal : ∃ (c : ℕ), ComputableTidilyInTimeAndSpace budgetedUniversal eInS eOut (fun (i : Desc × List ℕ × ℕ × ℕ) => c * ((i.2.2.1 + 1) * ((eInS i).length + 1) ^ 2 * (budgetSpace i + 1) ^ 3)) fun (i : Desc × List ℕ × ℕ × ℕ) => c * (budgetSpace i + 1)

The universal machine within a space budget. The budgeted universal function is tidily computable within space linear in the bound budgetSpace on the states of its fold, by the multi-pass fold of the in-place universal machine with the budget test at the end of each pass. Each of the t passes reads the whole input.

theorem Turing.MultiTapeTM.Universal.budgetSpace_le (d : Desc) (x : List ℕ) (b t : ℕ) : budgetSpace (d, x, t, b) ≤ 60 * (descLen d + 1) + 6 * b + 4 * (encNat t).length + 4 * (encNat (x.length + 1)).length + 2 * List.foldr max 0 x

The space of the universal machine within a budget: budgetSpace is linear in the description, the budget and the lengths of the number of steps and of the length of the input in binary, plus the largest symbol of the input.

theorem Turing.MultiTapeTM.Universal.length_eOut_budgetedUniversal_le (d : Desc) (x : List ℕ) (b t : ℕ) : (eOut (budgetedUniversal (d, x, t, b))).length ≤ budgetSpace (d, x, t, b)

The encoded result of the universal function within a budget is within budgetSpace.

theorem Turing.MultiTapeTM.Universal.computableTidilyInO_budgetedUniversal : ComputableTidilyInO budgetedUniversal eInS eOut (fun (i : Desc × List ℕ × ℕ × ℕ) => (i.2.2.1 + 1) * ((eInS i).length + 1) ^ 2 * (budgetSpace i + 1) ^ 3) budgetSpace

The universal machine within a space budget, up to constants: within time O((t + 1) * (n + 1) ^ 2 * (budgetSpace + 1) ^ 3) on an encoded input of length n and space O(budgetSpace) (Turing.MultiTapeTM.Universal.budgetSpace_le).