pairSelfTM: build pair x x from input x

The input-preparation prefix of the time-hierarchy diagonalizer D : TM 8. Starting from the fresh initial configuration on input x, it builds the self-pair pair x x onto work tape 7 and leaves every other tape clean:

• input tape: cells unchanged, head parked at cell 1;
• work tapes ≠ 7: exactly the started blank tape (Tape.init []).move right;
• work tape 7: exactly the started pair tape (Tape.init ((pair x x).map Γ.ofBool)).move right;
• output tape: blank cells, head parked at cell 1.

Tape layout of D: tapes 0–5 are the UTM's six tapes, 6 is the clock, 7 holds the pair.

Phase structure

copyInputToWorkTM 0    copy x onto work tape 0
rewindWorkTM 0         rewind work tape 0 to cell 1
rewindInputTM          rewind the input head to cell 1
pairBuildTM 0 7        build pair x x on work tape 7 (x from input, y from tape 0)
rewindInputTM          re-park the input head at cell 1
rewindWorkTM 0         rewind work tape 0 (still holding x) to cell 1
clearWorkTM 0          erase work tape 0 back to the started blank tape

Main results

• pairSelfTM — the machine
• pairSelfTime — its running-time bound, 23·n + 58
• pairSelfTM_hoareTime — the Hoare specification described above
• pairSelfTime_le — the clean quadratic bound pairSelfTime n ≤ 58·(n+1)²

def Complexity.TM.pairSelfTM : TM 8

Build pair x x (the input paired with itself) on work tape 7, leaving all other tapes clean: input and output heads parked at cell 1, work tapes ≠ 7 as started blank tapes.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.TM.pairSelfTime (n : ℕ) : ℕ

Running-time bound for pairSelfTM on inputs of length n: the sum of the seven phase bounds plus the six seqTM seam steps.

Equations

• Complexity.TM.pairSelfTime n = 23 * n + 58

theorem Complexity.TM.pairSelfTM_hoareTime (x : List Bool) : pairSelfTM.HoareTime (fun (inp : Tape) (work : Fin 8 → Tape) (out : Tape) => inp = Tape.init (List.map Γ.ofBool x) ∧ (∀ (i : Fin 8), work i = Tape.init []) ∧ out = Tape.init []) (fun (inp : Tape) (work : Fin 8 → Tape) (out : Tape) => inp.cells = (Tape.init (List.map Γ.ofBool x)).cells ∧ inp.head = 1 ∧ (∀ (i : Fin 8), i ≠ 7 → work i = (Tape.init []).move Dir3.right) ∧ work 7 = (Tape.init (List.map Γ.ofBool (pair x x))).move Dir3.right ∧ out.cells = (Tape.init []).cells ∧ out.head = 1) (pairSelfTime x.length)

Input preparation for the diagonalizer. Starting from the fresh initial configuration on input x, pairSelfTM halts within pairSelfTime |x| steps with pair x x started on work tape 7, all other work tapes as started blank tapes, and the input and output heads parked at cell 1 with unchanged cells.

theorem Complexity.TM.pairSelfTime_le (n : ℕ) : pairSelfTime n ≤ 58 * (n + 1) ^ 2

Clean closed quadratic bound for pairSelfTime.