The cost of cutting, pasting and stepping windows

Cutting windows (Turing.MultiTapeTM.Universal.Windowed.extract) and pasting them back (Turing.MultiTapeTM.Universal.Windowed.restore) take time linear in the encoded windows for each window, so time O((K + 1) * N) for K windows of total encoded length N; every operation on the cells of a window is linear in their encoded length. A windowed step (Turing.MultiTapeTM.Universal.Windowed.wstep) takes time cubic in the encoded description and windows. Halving a number of steps in unary takes linear time.

Main results

• Turing.MultiTapeTM.Universal.Windowed.extract_inO, .restore_inO: cutting and pasting.
• Turing.MultiTapeTM.Universal.Windowed.wstep_inO: a windowed step.
• Turing.MultiTapeTM.Universal.Windowed.firstHalf_inO, .half_inO: halving in unary.

Sizes

Cutting and pasting a window

Cutting and pasting all windows

theorem Turing.MultiTapeTM.Universal.Windowed.extract_inO : ComputableInO (fun (p : ℕ × Win) => extract p.1 p.2) (encPair encUnary eWin) eWin (fun (p : ℕ × Win) => (p.2.2.length + 1) * (((encPair encUnary eWin) p).length + 1)) fun (p : ℕ × Win) => (p.2.2.length + 1) * (((encPair encUnary eWin) p).length + 1)

Cutting windows of radius r, in time linear in the encoded windows for each window.

theorem Turing.MultiTapeTM.Universal.Windowed.restore_inO : ComputableInO (fun (p : ℕ × Win × Win) => restore p.1 p.2.1 p.2.2) (encPair encUnary (encPair eWin eWin)) eWin (fun (p : ℕ × Win × Win) => (p.2.1.2.length + 1) * (((encPair encUnary (encPair eWin eWin)) p).length + 1)) fun (p : ℕ × Win × Win) => (p.2.1.2.length + 1) * (((encPair encUnary (encPair eWin eWin)) p).length + 1)

Pasting windows back, in time linear in the encoded windows for each window.

Halving in unary

theorem Turing.MultiTapeTM.Universal.Windowed.firstHalf_inO : ComputableInO firstHalf encUnary encUnary (fun (n : ℕ) => (encUnary n).length) fun (n : ℕ) => (encUnary n).length

The first half of a number of steps, in unary, in linear time.

theorem Turing.MultiTapeTM.Universal.Windowed.half_inO : ComputableInO (fun (x : ℕ) => x / 2) encUnary encUnary (fun (n : ℕ) => (encUnary n).length) fun (n : ℕ) => (encUnary n).length

Half a number of steps, rounded down, in unary, in linear time.

A windowed step

Coded input cells

The step

Sizes

theorem Turing.MultiTapeTM.Universal.Windowed.wstep_inO : ComputableInO (fun (p : Desc × Win) => wstep p.1 p.2) (encPair eDesc eWin) (encPair eWin eSym) (fun (p : Desc × Win) => (((encPair eDesc eWin) p).length + 1) ^ 3) fun (p : Desc × Win) => (((encPair eDesc eWin) p).length + 1) ^ 3

A windowed step, in time cubic in the encoded description and windows.