The cost of the initial windows

From the input of the universal function — a description d, an input x and a number of steps t in binary — the first problem of the windowed simulation is the description, t in unary and the windows of radius t of the initial configuration. It is computable in time O(N + (D + 1) ^ 3 + (t + 1) * (L + 1)) for the encoded input length N, the length D of the description and the length L of t in binary: t is converted to unary by doubling, the input symbols are recoded by a finite-state rewrite in linear time, and the input window is cut with a linear-time take.

The computation goes through the intermediate value (d, t, x') with t in unary and the coded input cells x' = x.map fun a => some (a + 1):

• t is converted by a left fold of u ↦ 2 * u + b over the binary digits of t, most significant first; each round is linear in the unary state, which is at most t.
• In encList encUnary x, the element a is (true true)^a false; in the encoding of x' it is (true true)^(a + 2) false. The rewrite true ↦ true, false ↦ true false, applied four times, maps the one to the other, and every application is a finite-state transducer.
• The input window keeps the first t + 1 coded cells; the blank work windows are built by ComputableTidilyInDegree.replicate, within time cubic in the number of work tapes.

Main results

• Turing.MultiTapeTM.Universal.Windowed.initProb_inO: the first problem.

The initial windows

From binary to unary by doubling

Recoding the input symbols

The intermediate value

theorem Turing.MultiTapeTM.Universal.Windowed.initProb_inO : ComputableInO (fun (i : Desc × List ℕ × ℕ) => (i.1, i.2.2, extract i.2.2 (initWin i.1 i.2.1))) eIn eProb (fun (i : Desc × List ℕ × ℕ) => (eIn i).length + (descLen i.1 + 1) ^ 3 + (i.2.2 + 1) * ((encNat i.2.2).length + 1)) fun (i : Desc × List ℕ × ℕ) => (eIn i).length + (descLen i.1 + 1) ^ 3 + (i.2.2 + 1) * ((encNat i.2.2).length + 1)

The first problem of the windowed simulation, in time linear in the encoded input, cubic in the length of the description and O((t + 1) * (L + 1)) for t steps written with L binary digits.