UTM initialization machine

initTM : TM 6 is the first phase of the universal Turing machine (docs/UTM-design.md). On input pair α x it:

1. parses the α-region of the input (α's bits doubled, terminated by the separator 01), translating each 2-bit group into one desc symbol (symOfPair) written onto the desc tape (work tape 4);
2. copies x onto the virtual input tape (work tape 0) shifted one cell right (the +1-shift representation: work-0 cell 1 stays □, x[i] goes to cell i + 2);
3. copies the first desc field (the qstart field, i.e. the symbols before the first □) onto the state tape (work tape 3);
4. parks all work-tape heads at cell 1 and halts, leaving the output tape untouched.

The specification is initTM_hoareTime. Malformed inputs (a 10 cell pair or a blank in the middle of a 2-cell group in the α-region) make the machine halt immediately; the specification only covers well-formed inputs.

inductive Complexity.TM.InitQ : Type

Control states of initTM.

• start — the forced first step (every head bounces off ▷ to cell 1);
• readFst pending — phase 1, at the first cell of a 2-cell input group; pending holds an α-bit waiting for its partner (desc symbols are built from two α-bits);
• readSnd fst pending — phase 1, at the second cell of a 2-cell group whose first cell held the bit fst;
• copyX — phase 2, copying x to work tape 0 (shifted);
• rewindDesc — phase 3, rewinding the desc tape (work 4) to cell 1;
• copyField — phase 3, copying the qstart field of the desc tape onto the state tape (work 3);
• rewindDesc2, rewindState, rewindV0 — final rewinds of work tapes 4, 3, 0;
• done — halt.

• start : InitQ
• readFst (pending : Option Bool) : InitQ
• readSnd (fst : Bool) (pending : Option Bool) : InitQ
• copyX : InitQ
• rewindDesc : InitQ
• copyField : InitQ
• rewindDesc2 : InitQ
• rewindState : InitQ
• rewindV0 : InitQ
• done : InitQ

@[implicit_reducible]

instance Complexity.TM.instDecidableEqInitQ : DecidableEq InitQ

Equations

• Complexity.TM.instDecidableEqInitQ = Complexity.TM.instDecidableEqInitQ.decEq

def Complexity.TM.instDecidableEqInitQ.decEq (x✝ x✝¹ : InitQ) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Complexity.TM.instFintypeInitQ : Fintype InitQ

Equations

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

def Complexity.TM.initTM : TM 6

The UTM initialization machine. See the module docstring and docs/UTM-design.md for the phase structure.

Equations

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

theorem Complexity.TM.initTM_hoareTime (α x : List Bool) : initTM.HoareTime (fun (inp : Tape) (work : Fin 6 → Tape) (out : Tape) => inp = Tape.init (List.map Γ.ofBool (pair α x)) ∧ (∀ (i : Fin 6), work i = Tape.init []) ∧ out = Tape.init []) (fun (inp : Tape) (work : Fin 6 → Tape) (out : Tape) => inp.cells = (Tape.init (List.map Γ.ofBool (pair α x))).cells ∧ ((work 0).cells = fun (k : ℕ) => if k = 0 then Γ.start else if k = 1 then Γ.blank else (List.map Γ.ofBool x)[k - 2]?.getD Γ.blank) ∧ (work 0).head = 1 ∧ (work 1).HoldsExact [] ∧ (work 1).head = 1 ∧ (work 2).HoldsExact [] ∧ (work 2).head = 1 ∧ (work 3).HoldsExact (takeField (groupPairs α)).1 ∧ (work 3).head = 1 ∧ (work 4).HoldsExact (groupPairs α) ∧ (work 4).head = 1 ∧ (work 5).HoldsExact [] ∧ (work 5).head = 1 ∧ out.cells = (Tape.init []).cells ∧ out.head = 1) (4 * (pair α x).length + 4 * (groupPairs α).length + 24)

initTM specification. Started on input pair α x with all work tapes and the output tape empty, initTM halts within 4·|pair α x| + 4·|groupPairs α| + 24 steps having:

• left the input tape cells untouched;
• copied x onto the virtual input tape (work 0) in the +1-shift representation (the VShift shadow of Tape.init (x.map Γ.ofBool));
• translated α onto the desc tape (work 4): groupPairs α;
• copied the qstart field (takeField (groupPairs α)).1 onto the state tape (work 3);
• left work tapes 1, 2, 5 and the output tape blank;
• parked every work-tape head and the output head at cell 1.

theorem Complexity.TM.initTM_hoareTime_started (α x : List Bool) : initTM.HoareTime (fun (inp : Tape) (work : Fin 6 → Tape) (out : Tape) => inp.cells = (Tape.init (List.map Γ.ofBool (pair α x))).cells ∧ inp.head = 1 ∧ (∀ (i : Fin 6), work i = (Tape.init []).move Dir3.right) ∧ out.cells = (Tape.init []).cells ∧ out.head = 1) (fun (inp : Tape) (work : Fin 6 → Tape) (out : Tape) => inp.cells = (Tape.init (List.map Γ.ofBool (pair α x))).cells ∧ ((work 0).cells = fun (k : ℕ) => if k = 0 then Γ.start else if k = 1 then Γ.blank else (List.map Γ.ofBool x)[k - 2]?.getD Γ.blank) ∧ (work 0).head = 1 ∧ (work 1).HoldsExact [] ∧ (work 1).head = 1 ∧ (work 2).HoldsExact [] ∧ (work 2).head = 1 ∧ (work 3).HoldsExact (takeField (groupPairs α)).1 ∧ (work 3).head = 1 ∧ (work 4).HoldsExact (groupPairs α) ∧ (work 4).head = 1 ∧ (work 5).HoldsExact [] ∧ (work 5).head = 1 ∧ out.cells = (Tape.init []).cells ∧ out.head = 1) (4 * (pair α x).length + 4 * (groupPairs α).length + 24)

initTM specification, started form. Identical postcondition and time bound to initTM_hoareTime, but the tapes arrive already bounced off ▷: the input head is parked at cell 1 over the same cells, every work tape is (Tape.init []).move Dir3.right (blank cells, head 1), and the output tape is blank with head 1. This is the form in which a lifted initTM receives its tapes when it runs mid-sequence rather than as the first phase of a machine.