Windowed simulation

In n steps, a head reads only cells within distance n of where it started. The windowed simulation exploits this to simulate n steps on windows: for every tape, the zipper of the cells within distance n of its head. It cuts the windows of radius ⌈n / 2⌉ around the heads, simulates the first ⌈n / 2⌉ steps on them recursively, pastes the result back, and does the same for the remaining ⌊n / 2⌋ steps. A single step is Turing.MultiTapeTM.Universal.stepWith.

Cutting and pasting take time linear in the enclosing window, so n steps take time O(n log n) for a fixed machine; that cost analysis is Turing.MultiTapeTM.Universal.computableInO_universal_nlogn, in a separate module. This module defines the simulation and proves that it computes the universal function.

A windowed configuration (Turing.MultiTapeTM.Universal.Windowed.Win) holds the state, then the input window followed by the work windows. The head fields of the window zippers are not used. Input cells are coded so that a step can be taken without the position of the input head: some 0 is the left end at position 0, some (a + 1) the input symbol a, and none a blank after the input.

The correctness proof follows each window against its tape cell by cell: if every window agrees with its tape within distance n of the head, then n windowed steps take the same steps, the windows keep agreeing with the tapes there, and the cells beyond are untouched. Pasting a window back is exact because a list of a cut window either has exactly the cut length, in which case the run keeps it aligned with the rest of the outer list, or ends early, in which case the outer list has no cells beyond it either.

Main definitions

• Turing.MultiTapeTM.Universal.Windowed.extract, .restore: cutting windows and pasting them back.
• Turing.MultiTapeTM.Universal.Windowed.wstep: one step on windows.
• Turing.MultiTapeTM.Universal.Windowed.sim: the recursive simulation of n steps.
• Turing.MultiTapeTM.Universal.Windowed.initWin: the windows of the initial configuration.

Main results

• Turing.MultiTapeTM.Universal.Windowed.universal_eq_sim: the windowed simulation of t steps from the radius-t windows of the initial configuration computes the universal function.
• Turing.MultiTapeTM.Universal.Windowed.length_sim, .length_sim_le, .sim_cells, .sim_state, .sim_output: the number and lengths of the windows, their cells, the state and the emitted symbols, for the cost analysis.

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.Windowed.Win : Type

A windowed configuration: the state, then the input window followed by the work windows.

def Turing.MultiTapeTM.Universal.Windowed.cut (r : ℕ) (t : Tape) : Tape

The cells of t within distance r of its head, as a zipper with head field 0.

def Turing.MultiTapeTM.Universal.Windowed.paste (r : ℕ) (outer inner : Tape) : Tape

The window inner, cut from outer with radius r and then run, with the cells of outer beyond distance r of its head put back around it.

def Turing.MultiTapeTM.Universal.Windowed.extract (r : ℕ) (w : Win) : Win

The windows of radius r.

def Turing.MultiTapeTM.Universal.Windowed.restore (r : ℕ) (outer inner : Win) : Win

The windows inner, extracted from outer with radius r and then run, pasted back.

def Turing.MultiTapeTM.Universal.Windowed.inSym (c : Option ℕ) : Option ℕ

The input symbol of a coded input cell.

def Turing.MultiTapeTM.Universal.Windowed.inPos (c : Option ℕ) : ℕ

A stand-in for the position of the input head on a coded input cell: 0 at the left end and 1 elsewhere. Turing.MultiTapeTM.Universal.moveInput distinguishes only these cases.

def Turing.MultiTapeTM.Universal.Windowed.moveIn (t : Tape) (p p' : ℕ) : Tape

The input window, moved as the input head moved from p to p'.

def Turing.MultiTapeTM.Universal.Windowed.wstep (d : Desc) (w : Win) : Win × Option ℕ

One step on a windowed configuration, and the symbol it emits.

def Turing.MultiTapeTM.Universal.Windowed.firstHalf (n : ℕ) : ℕ

The number of steps of the first half of a block of n steps.

@[irreducible]

def Turing.MultiTapeTM.Universal.Windowed.sim (d : Desc) : ℕ → Win → Win × List ℕ

The windowed simulation of n steps, and the symbols emitted.

def Turing.MultiTapeTM.Universal.Windowed.initWin (d : Desc) (x : List ℕ) : Win

The windows of the initial configuration on the input x: the input head on the first input symbol, after the left end, and blank work tapes.

Cells of zippers

Steps on windows

Windows agreeing with tapes

Correctness of the windowed simulation

theorem Turing.MultiTapeTM.Universal.Windowed.sim_add_two (d : Desc) (n : ℕ) (w : Win) : sim d (n + 2) w = (restore ((n + 2) / 2) (restore (firstHalf (n + 2)) w (sim d (firstHalf (n + 2)) (extract (firstHalf (n + 2)) w)).1) (sim d ((n + 2) / 2) (extract ((n + 2) / 2) (restore (firstHalf (n + 2)) w (sim d (firstHalf (n + 2)) (extract (firstHalf (n + 2)) w)).1))).1, (sim d (firstHalf (n + 2)) (extract (firstHalf (n + 2)) w)).2 ++ (sim d ((n + 2) / 2) (extract ((n + 2) / 2) (restore (firstHalf (n + 2)) w (sim d (firstHalf (n + 2)) (extract (firstHalf (n + 2)) w)).1))).2)

The windowed simulation of n + 2 steps: the first half on cut windows, pasted back, then the second half.

theorem Turing.MultiTapeTM.Universal.Windowed.universal_eq_sim (d : Desc) (x : List ℕ) (t : ℕ) : universal (d, x, t) = ((sim d t (extract t (initWin d x))).2, (sim d t (extract t (initWin d x))).1.1.isNone)

The windowed simulation computes the universal function: started from the radius-t windows of the initial configuration, t windowed steps give the output and the halting status after t steps.

Sizes of the windows

Facts about the shapes of the windows, the cells they hold, the state and the emitted symbols, for the cost analysis of the windowed simulation.

theorem Turing.MultiTapeTM.Universal.Windowed.length_sim (d : Desc) (n : ℕ) (w : Win) : (sim d n w).1.2.length = w.2.length

The windowed simulation keeps the number of windows.

theorem Turing.MultiTapeTM.Universal.Windowed.length_sim_le (d : Desc) (n : ℕ) (w : Win) {k : ℕ} {W W' : Tape} (hW : w.2[k]? = some W) (hW' : (sim d n w).1.2[k]? = some W') : W'.left.length ≤ W.left.length + n ∧ W'.right.length ≤ max W.right.length 1 + n

In n windowed steps, each window grows by at most n cells on each side, where the right list, which holds the cell under the head, counts as at least one cell.

theorem Turing.MultiTapeTM.Universal.Windowed.sim_cells (d : Desc) (S : Option ℕ → Prop) (h0 : S none) (htable : ∀ e ∈ d.table, ∀ a ∈ e.2.workTapes, ∀ (o : Option ℕ), a.1 = some o → S o) (n : ℕ) (w : Win) (hw : ∀ W ∈ w.2, ∀ o ∈ W.left ++ W.right, S o) (W : Tape) : W ∈ (sim d n w).1.2 → ∀ o ∈ W.left ++ W.right, S o

The cells of the windows after the windowed simulation come from the windows before it or are written by a transition: a property of cells that holds for the blank, for every symbol written by a transition and for all cells of the windows before, holds for all cells after.

theorem Turing.MultiTapeTM.Universal.Windowed.sim_state (d : Desc) (T : Option ℕ → Prop) (h0 : T none) (htable : ∀ e ∈ d.table, T e.2.state) (n : ℕ) (w : Win) (hw : T w.1) : T (sim d n w).1.1

The state after the windowed simulation is the state before it, the halting state, or the next state of a transition.

theorem Turing.MultiTapeTM.Universal.Windowed.sim_output (d : Desc) (n : ℕ) (w : Win) (o : ℕ) : o ∈ (sim d n w).2 → ∃ e ∈ d.table, e.2.output = some o

Every symbol emitted by the windowed simulation is the output of a transition.