Building an input prefix into a description

A description d and a word p give a description Turing.MultiTapeTM.Universal.hardwire d p of a machine that behaves on every input of bits x as the machine described by d behaves on p ++ x (Turing.MultiTapeTM.Universal.Desc.computes_hardwire). This is the s-m-n theorem for descriptions, the counterpart of the machines printing a fixed word in Sipser, Lemma 6.1; that the new description is computed from d and p in polynomial time is proved in Complexity.Computability.Machines.Turing.MultiTape.Halting.SMN.

The machine first writes a marker, then p, then a copy of its input on a new work tape, the virtual input tape, and rewinds that tape to the marker. It then runs the transitions of d with every reading and every move of the input head redirected to the virtual input tape (Turing.MultiTapeTM.Universal.Redirect.redirect): the marker stands for the blank left of the input, and moves are clamped at both ends as the input head's are. The redirected run is the run of d, step for step (Turing.MultiTapeTM.Universal.Redirect.iterate_stepOut_redirect), since on the virtual input tape the redirected transitions read what d reads on its input. Redirection is independent of the prefix and is reused, after other preparations of the virtual input tape, in Complexity.Computability.Machines.Turing.MultiTape.Halting.Rice.

Main definitions

• Turing.MultiTapeTM.Universal.Redirect.vtape: a virtual input tape.
• Turing.MultiTapeTM.Universal.Redirect.redirect: transitions reading the input from the virtual input tape.
• Turing.MultiTapeTM.Universal.hardwire: the description with an input prefix built in.

Main results

• Turing.MultiTapeTM.Universal.Desc.computes_iff_of_iterate: a description whose run is, after some steps, the image of the run of another description computes the same outputs.
• Turing.MultiTapeTM.Universal.Redirect.iterate_stepOut_redirect: redirected runs.
• Turing.MultiTapeTM.Universal.Desc.computes_hardwire, Turing.MultiTapeTM.Universal.Desc.halts_hardwire: the behavior of hardwire d p.

References

• M. Sipser, Introduction to the Theory of Computation

Runs of descriptions

theorem Turing.MultiTapeTM.Universal.Redirect.stepOut_of_state_eq_none {d : Desc} {x : List ℕ} {c : SCfg} (h : c.state = none) (out : List ℕ) : stepOut d x (c, out) = (c, out)

A halted configuration is fixed by stepOut.

theorem Turing.MultiTapeTM.Universal.Redirect.iterate_stepOut_of_state_eq_none {d : Desc} {x : List ℕ} {s : SCfg × List ℕ} {t t' : ℕ} (h : ((stepOut d x)^[t] s).1.state = none) (ht : t ≤ t') : (stepOut d x)^[t'] s = (stepOut d x)^[t] s

Once halted, a run stays where it is.

theorem Turing.MultiTapeTM.Universal.Redirect.step_of_find? {d : Desc} {x : List ℕ} {c : SCfg} {q : ℕ} (hq : c.state = some q) {e : Key × Act} (he : List.find? (fun (x_1 : Key × Act) => decide (x_1.1 = c.key x q)) d.table = some e) : step d x c = (e.2.apply x c, e.2.output)

One step through the transition e found for the current key.

theorem Turing.MultiTapeTM.Universal.Redirect.step_of_find?_eq_none {d : Desc} {x : List ℕ} {c : SCfg} {q : ℕ} (hq : c.state = some q) (he : List.find? (fun (x_1 : Key × Act) => decide (x_1.1 = c.key x q)) d.table = none) : step d x c = ({ state := none, inputPos := c.inputPos, workTapes := c.workTapes }, none)

One step halting for want of a transition for the current key.

theorem Turing.MultiTapeTM.Universal.Redirect.find?_eq_some_of_mem {l : List (Key × Act)} {e : Key × Act} (hmem : e ∈ l) (huniq : ∀ e' ∈ l, e'.1 = e.1 → e'.2 = e.2) : List.find? (fun (x : Key × Act) => decide (x.1 = e.1)) l = some e

A transition is found for a key when it is the only one in the table, up to its action.

theorem Turing.MultiTapeTM.Universal.Desc.computes_iff_of_iterate {d D : Desc} {x X : List ℕ} (F : SCfg → SCfg) (hF : ∀ (c : SCfg), (F c).state = none ↔ c.state = none) (u : ℕ) (hu : ∀ (t : ℕ), (stepOut D X)^[u + t] (init D, []) = (F ((stepOut d x)^[t] (init d, [])).1, ((stepOut d x)^[t] (init d, [])).2)) (o : List ℕ) : D.Computes X o ↔ d.Computes x o

Runs agreeing after some steps. If, after u steps, the run of D on X is the image under F of the run of d on x, with the same outputs, and F preserves exactly the halted configurations, then D and d halt with the same outputs.

Virtual input tapes

def Turing.MultiTapeTM.Universal.Redirect.marker : ℕ

The symbol marking the left end of a virtual input.

def Turing.MultiTapeTM.Universal.Redirect.vcells (xs : List ℕ) : List (Option ℕ)

The cells of a virtual input: the marker, then the input.

def Turing.MultiTapeTM.Universal.Redirect.vtape (base : ℤ) (l : List (Option ℕ)) (xs : List ℕ) (v : ℕ) : Tape

A virtual input tape for the input xs: the marker at position base, the input right of it and blanks beyond, the cells l left of the marker, nearest first, and the head on the v-th cell right of the marker.

def Turing.MultiTapeTM.Universal.Redirect.wtape (cs : List (Option ℕ)) : Tape

A tape holding the cells cs left of its head, which is on the first blank after them.

def Turing.MultiTapeTM.Universal.Redirect.vsym (s : Option ℕ) : Option ℕ

The input symbol that a virtual input tape stands for when it reads s: the marker stands for the blank left of the input.

def Turing.MultiTapeTM.Universal.Redirect.vmove (s : Option ℕ) (m : SignType) : SignType

The move of the head of a virtual input tape reading s, for the move m of the input head: at the marker and at the blank after the input, the moves that the input head cannot make are dropped.

theorem Turing.MultiTapeTM.Universal.Redirect.length_vcells (xs : List ℕ) : (vcells xs).length = xs.length + 1

theorem Turing.MultiTapeTM.Universal.Redirect.wtape_vcells (xs : List ℕ) : wtape (vcells xs) = vtape 0 [] xs (xs.length + 1)

@[simp]

theorem Turing.MultiTapeTM.Universal.Redirect.read_wtape (cs : List (Option ℕ)) : (wtape cs).read = none

theorem Turing.MultiTapeTM.Universal.Redirect.wtape_write_move (cs : List (Option ℕ)) (s : Option ℕ) : ((wtape cs).write s).move SignType.pos = wtape (cs ++ [s])

Writing at the first blank and moving on appends a cell.

theorem Turing.MultiTapeTM.Universal.Redirect.read_vtape_zero {xs : List ℕ} {base : ℤ} {l : List (Option ℕ)} : (vtape base l xs 0).read = some marker

theorem Turing.MultiTapeTM.Universal.Redirect.read_vtape_succ {xs : List ℕ} {base : ℤ} {l : List (Option ℕ)} (v : ℕ) : (vtape base l xs (v + 1)).read = inputSymbol xs (v + 1)

theorem Turing.MultiTapeTM.Universal.Redirect.vtape_move_pos {xs : List ℕ} {base : ℤ} {l : List (Option ℕ)} {v : ℕ} (hv : v ≤ xs.length) : (vtape base l xs v).move SignType.pos = vtape base l xs (v + 1)

theorem Turing.MultiTapeTM.Universal.Redirect.vtape_move_neg {xs : List ℕ} {base : ℤ} {l : List (Option ℕ)} {v : ℕ} (hv : v ≤ xs.length) : (vtape base l xs (v + 1)).move SignType.neg = vtape base l xs v

theorem Turing.MultiTapeTM.Universal.Redirect.vsym_read_vtape {xs : List ℕ} {base : ℤ} {l : List (Option ℕ)} {v : ℕ} (hxs : ∀ a ∈ xs, a ≠ marker) : vsym (vtape base l xs v).read = inputSymbol xs v

On a virtual input tape, the redirected reading is the reading of the input head.

theorem Turing.MultiTapeTM.Universal.Redirect.move_vmove_vtape {xs : List ℕ} {base : ℤ} {l : List (Option ℕ)} {v : ℕ} (hxs : ∀ a ∈ xs, a ≠ marker) (hv : v ≤ xs.length + 1) (m : SignType) : (vtape base l xs v).move (vmove (vtape base l xs v).read m) = vtape base l xs (moveInput v (inputSymbol xs v) m)

On a virtual input tape, the redirected move is the move of the input head.

Work tapes

theorem Turing.MultiTapeTM.Universal.Redirect.applyTapes_nil (ts : List Tape) : applyTapes ts [] = ts

theorem Turing.MultiTapeTM.Universal.Redirect.applyTapes_append_idle {preT : List Tape} {pre : List (Option ℕ)} (h : pre.length = preT.length) (ts : List Tape) (as : List TapeAct) : applyTapes (preT ++ ts) (List.map (fun (x : Option ℕ) => (none, SignType.zero)) pre ++ as) = preT ++ applyTapes ts as

Actions that neither write nor move leave tapes as they are.

theorem Turing.MultiTapeTM.Universal.Redirect.applyTapes_append_take (ts us : List Tape) (as : List TapeAct) : applyTapes (ts ++ us) (List.take ts.length as) = applyTapes ts as ++ us

Actions cut to the first work tapes leave the others as they are.

theorem Turing.MultiTapeTM.Universal.Redirect.inputPos_step_le {d : Desc} {xs : List ℕ} {c : SCfg} (hc : c.inputPos ≤ xs.length + 1) : (step d xs c).1.inputPos ≤ xs.length + 1

A step keeps the input head on the input or its boundaries.

theorem Turing.MultiTapeTM.Universal.Redirect.length_workTapes_step {d : Desc} {xs : List ℕ} {c : SCfg} : (step d xs c).1.workTapes.length = c.workTapes.length

A step keeps the number of work tapes.

Redirecting the input

def Turing.MultiTapeTM.Universal.Redirect.vlift : Option ℕ → List (Option ℕ)

The symbols that a virtual input tape reads where the input head reads i: the marker or a blank for a blank, and i itself otherwise. Nothing stands for the marker itself, so transitions reading the marker on the input are dropped.

theorem Turing.MultiTapeTM.Universal.Redirect.mem_vlift {i s : Option ℕ} : s ∈ vlift i ↔ i = vsym s

def Turing.MultiTapeTM.Universal.Redirect.redirectEntry (φ : ℕ → ℕ) (r : Option ℕ) (pre : List (Option ℕ)) (suf : ℕ) (adj : List TapeAct → List TapeAct) (e : Key × Act) (s : Option ℕ) : Key × Act

The transition e reading s on the virtual input tape, the first work tape: the state renamed by φ, the input head reading r and kept in place, the work tapes of e after further tapes reading pre, left alone, and before suf blank ones, and the actions on the work tapes of e adjusted by adj.

def Turing.MultiTapeTM.Universal.Redirect.redirect (φ : ℕ → ℕ) (r : Option ℕ) (pre : List (Option ℕ)) (suf : ℕ) (adj : List TapeAct → List TapeAct) (table : List (Key × Act)) : List (Key × Act)

Redirected transitions: the transitions of table reading the input from the virtual input tape (Turing.MultiTapeTM.Universal.Redirect.redirectEntry).

theorem Turing.MultiTapeTM.Universal.Redirect.find?_redirect {φ : ℕ → ℕ} {r : Option ℕ} {pre : List (Option ℕ)} {suf : ℕ} {adj : List TapeAct → List TapeAct} (hφ : Function.Injective φ) (q : ℕ) (s : Option ℕ) (ws : List (Option ℕ)) (table : List (Key × Act)) : List.find? (fun (x : Key × Act) => decide (x.1 = { state := φ q, input := r, work := s :: (pre ++ (ws ++ List.replicate suf none)) })) (redirect φ r pre suf adj table) = Option.map (fun (e : Key × Act) => redirectEntry φ r pre suf adj e s) (List.find? (fun (x : Key × Act) => decide (x.1 = { state := q, input := vsym s, work := ws })) table)

The redirected transition found for a key is the redirection of the transition found for the key it stands for.

def Turing.MultiTapeTM.Universal.Redirect.redirectCfg (φ : ℕ → ℕ) (rp : ℕ) (base : ℤ) (l : List (Option ℕ)) (xs : List ℕ) (preT sufT : List Tape) (c : SCfg) : SCfg

The configuration standing for the configuration c of a redirected description: the state renamed by φ, the input head at rp, the virtual input tape for xs with the head at the input position of c, and the work tapes of c between preT and sufT.

theorem Turing.MultiTapeTM.Universal.Redirect.step_redirect {φ : ℕ → ℕ} {r : Option ℕ} {pre : List (Option ℕ)} {suf : ℕ} {adj : List TapeAct → List TapeAct} {D d : Desc} {X xs : List ℕ} {rp : ℕ} {base : ℤ} {l : List (Option ℕ)} {preT sufT : List Tape} (hφ : Function.Injective φ) (hD : ∀ (q : ℕ) (ws : List (Option ℕ)), List.find? (fun (x : Key × Act) => decide (x.1 = { state := φ q, input := r, work := ws })) D.table = List.find? (fun (x : Key × Act) => decide (x.1 = { state := φ q, input := r, work := ws })) (redirect φ r pre suf adj d.table)) (hrp : inputSymbol X rp = r) (hxs : ∀ a ∈ xs, a ≠ marker) (hpre : List.map Tape.read preT = pre) (hsuf : List.map Tape.read sufT = List.replicate suf none) {c : SCfg} (hc : c.inputPos ≤ xs.length + 1) (hadj : ∀ (was : List TapeAct), applyTapes (c.workTapes ++ sufT) (adj was) = applyTapes c.workTapes was ++ sufT) : step D X (redirectCfg φ rp base l xs preT sufT c) = (redirectCfg φ rp base l xs preT sufT (step d xs c).1, (step d xs c).2)

A redirected step: in a description holding the redirected transitions of d for the renamed states, a step from a configuration standing for c stands for the step of d from c, and emits the same symbol.

theorem Turing.MultiTapeTM.Universal.Redirect.iterate_stepOut_redirect {φ : ℕ → ℕ} {r : Option ℕ} {pre : List (Option ℕ)} {suf : ℕ} {adj : List TapeAct → List TapeAct} {D d : Desc} {X xs : List ℕ} {rp : ℕ} {base : ℤ} {l : List (Option ℕ)} {preT sufT : List Tape} (hφ : Function.Injective φ) (hD : ∀ (q : ℕ) (ws : List (Option ℕ)), List.find? (fun (x : Key × Act) => decide (x.1 = { state := φ q, input := r, work := ws })) D.table = List.find? (fun (x : Key × Act) => decide (x.1 = { state := φ q, input := r, work := ws })) (redirect φ r pre suf adj d.table)) (hrp : inputSymbol X rp = r) (hxs : ∀ a ∈ xs, a ≠ marker) (hpre : List.map Tape.read preT = pre) (hsuf : List.map Tape.read sufT = List.replicate suf none) {n : ℕ} (hadj : ∀ (ts : List Tape), ts.length = n → ∀ (was : List TapeAct), applyTapes (ts ++ sufT) (adj was) = applyTapes ts was ++ sufT) (t : ℕ) {c : SCfg} (hc : c.inputPos ≤ xs.length + 1) (hn : c.workTapes.length = n) (out : List ℕ) : (stepOut D X)^[t] (redirectCfg φ rp base l xs preT sufT c, out) = (redirectCfg φ rp base l xs preT sufT ((stepOut d xs)^[t] (c, out)).1, ((stepOut d xs)^[t] (c, out)).2)

Redirected runs: from a configuration standing for c, the run of D stands for the run of d from c, with the same output.

Rewinding the virtual input tape

@[simp]

theorem Turing.MultiTapeTM.Universal.Redirect.read_blank : Tape.blank.read = none

theorem Turing.MultiTapeTM.Universal.Redirect.map_read_replicate_blank (k : ℕ) : List.map Tape.read (List.replicate k Tape.blank) = List.replicate k none

@[simp]

theorem Turing.MultiTapeTM.Universal.Redirect.eBit_false : eBit false = 0

@[simp]

theorem Turing.MultiTapeTM.Universal.Redirect.eBit_true : eBit true = 1

def Turing.MultiTapeTM.Universal.Redirect.bitSyms : List (Option ℕ)

The symbols that the input head reads on an input of bits: blanks and the bits.

theorem Turing.MultiTapeTM.Universal.Redirect.inputSymbol_map_eBit_mem (x : List Bool) (p : ℕ) : inputSymbol (List.map (⇑eBit) x) p ∈ bitSyms

def Turing.MultiTapeTM.Universal.Redirect.rewindEntries (q : ℕ) (r : Option ℕ) (rest : List (Option ℕ)) (next : ℕ) : List (Key × Act)

Transitions rewinding the virtual input tape, the first work tape, in the state q, with the input head reading r and the other work tapes reading rest: over blanks and bits to the marker, and then onto the first cell after it, in the state next.

theorem Turing.MultiTapeTM.Universal.Redirect.iterate_stepOut_rewind {D : Desc} {X : List ℕ} {q next rp : ℕ} {rest : List Tape} {base : ℤ} {l : List (Option ℕ)} {w : List ℕ} (hD : ∀ e ∈ rewindEntries q (inputSymbol X rp) (List.map Tape.read rest) next, List.find? (fun (x : Key × Act) => decide (x.1 = e.1)) D.table = some e) (hw : ∀ a ∈ w, a = 0 ∨ a = 1) (out : List ℕ) {v : ℕ} (hv : v ≤ w.length + 1) : (stepOut D X)^[v + 1] ({ state := some q, inputPos := rp, workTapes := vtape base l w v :: rest }, out) = ({ state := some next, inputPos := rp, workTapes := vtape base l w 1 :: rest }, out)

Rewinding a virtual input tape of bits from the v-th cell takes v + 1 steps.

Building in an input prefix

def Turing.MultiTapeTM.Universal.Hardwire.writeEntries (p : List Bool) (k : ℕ) : List (Key × Act)

The transitions writing the marker and the prefix p on the virtual input tape, before k blank work tapes, whatever the input head reads: the marker in the state 0, and the i-th symbol from the end of p in the state 2 * i + 6. The state after the last symbol is 4.

def Turing.MultiTapeTM.Universal.Hardwire.copyEntries (k : ℕ) : List (Key × Act)

The transitions copying the input of bits to the virtual input tape in the state 4, before k blank work tapes, and moving to the state 2 at its end.

def Turing.MultiTapeTM.Universal.hardwire (d : Desc) (p : List Bool) : Desc

The description d with the input prefix p built in. It writes the marker and p on a new first work tape, the virtual input tape (Turing.MultiTapeTM.Universal.Hardwire.writeEntries), copies the input after them (Turing.MultiTapeTM.Universal.Hardwire.copyEntries), rewinds that tape (Turing.MultiTapeTM.Universal.Redirect.rewindEntries) and runs the transitions of d reading the input from it (Turing.MultiTapeTM.Universal.Redirect.redirect). These steps use even states, and the states of d become odd.

def Turing.MultiTapeTM.Universal.Hardwire.act (p : List Bool) (q₀ : ℕ) (key : Key) : Act

The action of the preparing transitions of hardwire d p, as a function of their keys.

def Turing.MultiTapeTM.Universal.Hardwire.prep (d : Desc) (p : List Bool) : List (Key × Act)

The preparing transitions of hardwire d p.

theorem Turing.MultiTapeTM.Universal.Hardwire.table_hardwire (d : Desc) (p : List Bool) : (hardwire d p).table = prep d p ++ Redirect.redirect (fun (q : ℕ) => 2 * q + 1) none [] 0 id d.table

theorem Turing.MultiTapeTM.Universal.Hardwire.prep_spec {d : Desc} {p : List Bool} {e : Key × Act} (he : e ∈ prep d p) : e.1.state % 2 = 0 ∧ e.2 = act p (2 * d.q₀ + 1) e.1

The preparing transitions have even states, and their actions are functions of their keys.

theorem Turing.MultiTapeTM.Universal.Hardwire.state_redirect {d : Desc} {e : Key × Act} (he : e ∈ Redirect.redirect (fun (q : ℕ) => 2 * q + 1) none [] 0 id d.table) : e.1.state % 2 = 1

theorem Turing.MultiTapeTM.Universal.Hardwire.find?_prep {d : Desc} {p : List Bool} {e : Key × Act} (he : e ∈ prep d p) : List.find? (fun (x : Key × Act) => decide (x.1 = e.1)) (hardwire d p).table = some e

Each preparing transition is the one found for its key.

theorem Turing.MultiTapeTM.Universal.Hardwire.find?_redirect_hardwire (d : Desc) (p : List Bool) (q : ℕ) (ws : List (Option ℕ)) : List.find? (fun (x : Key × Act) => decide (x.1 = { state := 2 * q + 1, input := none, work := ws })) (hardwire d p).table = List.find? (fun (x : Key × Act) => decide (x.1 = { state := 2 * q + 1, input := none, work := ws })) (Redirect.redirect (fun (q : ℕ) => 2 * q + 1) none [] 0 id d.table)

For odd states, the transitions found are the redirected transitions of d.

theorem Turing.MultiTapeTM.Universal.Hardwire.stepOut_of_mem_prep (d : Desc) (p x : List Bool) {c : SCfg} {q : ℕ} (hq : c.state = some q) {e : Key × Act} (he : e ∈ prep d p) (hkey : c.key (List.map (⇑eBit) x) q = e.1) (out : List ℕ) : stepOut (hardwire d p) (List.map (⇑eBit) x) (c, out) = (e.2.apply (List.map (⇑eBit) x) c, out ++ e.2.output.toList)

A step through a preparing transition.

theorem Turing.MultiTapeTM.Universal.Hardwire.iterate_write (d : Desc) (p x : List Bool) {j : ℕ} (hj : j ≤ p.length) : (stepOut (hardwire d p) (List.map (⇑eBit) x))^[j + 1] (init (hardwire d p), []) = ({ state := some (2 * (p.length - j) + 4), inputPos := 1, workTapes := Redirect.wtape (some Redirect.marker :: List.map (some ∘ ⇑eBit) (List.take j p)) :: List.replicate d.tapes Tape.blank }, [])

Writing the marker and the first j symbols of the prefix takes j + 1 steps.

theorem Turing.MultiTapeTM.Universal.Hardwire.iterate_copy (d : Desc) (p x : List Bool) {j : ℕ} (hj : j ≤ x.length) : (stepOut (hardwire d p) (List.map (⇑eBit) x))^[p.length + 1 + j] (init (hardwire d p), []) = ({ state := some 4, inputPos := j + 1, workTapes := Redirect.wtape (some Redirect.marker :: List.map (some ∘ ⇑eBit) (p ++ List.take j x)) :: List.replicate d.tapes Tape.blank }, [])

Copying the first j symbols of the input takes j further steps.

theorem Turing.MultiTapeTM.Universal.Hardwire.iterate_prepare (d : Desc) (p x : List Bool) : (stepOut (hardwire d p) (List.map (⇑eBit) x))^[2 * (p.length + x.length) + 4] (init (hardwire d p), []) = (Redirect.redirectCfg (fun (q : ℕ) => 2 * q + 1) (x.length + 1) 0 [] (List.map (⇑eBit) (p ++ x)) [] [] (init d), [])

The preparation: after 2 * (p.length + x.length) + 4 steps, hardwire d p is in the configuration standing for the initial configuration of d on p ++ x, redirected.

theorem Turing.MultiTapeTM.Universal.Desc.computes_hardwire (d : Desc) (p x : List Bool) (o : List ℕ) : (hardwire d p).Computes (List.map (⇑eBit) x) o ↔ d.Computes (List.map (⇑eBit) (p ++ x)) o

The behavior of hardwire d p: on every input of bits x, it halts with output o exactly when d halts on p ++ x with output o.

theorem Turing.MultiTapeTM.Universal.Desc.halts_hardwire (d : Desc) (p x : List Bool) : (hardwire d p).Halts (List.map (⇑eBit) x) ↔ d.Halts (List.map (⇑eBit) (p ++ x))

Halting of hardwire d p: on every input of bits x, it halts exactly when d halts on p ++ x.