The s-m-n theorem in polynomial time

The description Turing.MultiTapeTM.Universal.hardwire d p, which behaves on every input x as d behaves on p ++ x (Turing.MultiTapeTM.Universal.Desc.computes_hardwire), is computed from d and p in polynomial time (Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_hardwire): this is the s-m-n theorem for native descriptions, the counterpart of Sipser, Lemma 6.1. The transitions of hardwire d p are lists built from those of d and from the symbols of p by the list operations of the polynomial-time calculus, which fun_prop assembles from the fields of keys, actions and descriptions, using the shared bit coding rules in Complexity.Computability.Machines.Turing.MultiTape.Universal.PolyTime.

Main results

• Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_hardwire: the s-m-n theorem.

References

• M. Sipser, Introduction to the Theory of Computation

Fields of keys, actions and descriptions

theorem Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_keyFields : ComputableTidilyInPolyTime (fun (k : Key) => (k.state, k.input, k.work)) eKey (encPair encUnary (encPair eSym (encList eSym)))

theorem Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_key_state : ComputableTidilyInPolyTime Key.state eKey encUnary

theorem Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_key_input : ComputableTidilyInPolyTime Key.input eKey eSym

theorem Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_key_work : ComputableTidilyInPolyTime Key.work eKey (encList eSym)

theorem Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_key_mk {γ : Type} {encIn : γ ↪ List Bool} {state : γ → ℕ} {input : γ → Option ℕ} {work : γ → List (Option ℕ)} (hstate : ComputableTidilyInPolyTime state encIn encUnary) (hinput : ComputableTidilyInPolyTime input encIn eSym) (hwork : ComputableTidilyInPolyTime work encIn (encList eSym)) : ComputableTidilyInPolyTime (fun (x : γ) => { state := state x, input := input x, work := work x }) encIn eKey

theorem Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_actFields : ComputableTidilyInPolyTime (fun (a : Act) => (a.inputTape, a.workTapes, a.output, a.state)) eAct (encPair encSign (encPair (encList eTA) (encPair eSym eSym)))

theorem Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_act_inputTape : ComputableTidilyInPolyTime Act.inputTape eAct encSign

theorem Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_act_workTapes : ComputableTidilyInPolyTime Act.workTapes eAct (encList eTA)

theorem Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_act_output : ComputableTidilyInPolyTime Act.output eAct eSym

theorem Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_act_state : ComputableTidilyInPolyTime Act.state eAct eSym

theorem Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_act_mk {γ : Type} {encIn : γ ↪ List Bool} {inputTape : γ → SignType} {workTapes : γ → List TapeAct} {output state : γ → Option ℕ} (hinputTape : ComputableTidilyInPolyTime inputTape encIn encSign) (hworkTapes : ComputableTidilyInPolyTime workTapes encIn (encList eTA)) (houtput : ComputableTidilyInPolyTime output encIn eSym) (hstate : ComputableTidilyInPolyTime state encIn eSym) : ComputableTidilyInPolyTime (fun (x : γ) => { inputTape := inputTape x, workTapes := workTapes x, output := output x, state := state x }) encIn eAct

theorem Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_descFields : ComputableTidilyInPolyTime (fun (d : Desc) => (d.tapes, d.q₀, d.table)) eDesc (encPair encUnary (encPair encUnary (encList (encPair eKey eAct))))

theorem Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_desc_tapes : ComputableTidilyInPolyTime Desc.tapes eDesc encUnary

theorem Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_desc_q₀ : ComputableTidilyInPolyTime Desc.q₀ eDesc encUnary

theorem Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_desc_table : ComputableTidilyInPolyTime Desc.table eDesc (encList (encPair eKey eAct))

theorem Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_desc_mk {γ : Type} {encIn : γ ↪ List Bool} {tapes q₀ : γ → ℕ} {table : γ → List (Key × Act)} (htapes : ComputableTidilyInPolyTime tapes encIn encUnary) (hq₀ : ComputableTidilyInPolyTime q₀ encIn encUnary) (htable : ComputableTidilyInPolyTime table encIn (encList (encPair eKey eAct))) : ComputableTidilyInPolyTime (fun (x : γ) => { tapes := tapes x, q₀ := q₀ x, table := table x }) encIn eDesc

Helpers

theorem Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_option_map {γ : Type} {encIn : γ ↪ List Bool} {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {value : γ → Option α} {f : γ → α → β} (hvalue : ComputableTidilyInPolyTime value encIn (encOption encA)) (hf : ComputableTidilyInPolyTime (fun (p : γ × α) => f p.1 p.2) (encPair encIn encA) encB) : ComputableTidilyInPolyTime (fun (x : γ) => Option.map (f x) (value x)) encIn (encOption encB)

Mapping a computed option.

theorem Turing.MultiTapeTM.Universal.Hardwire.vlift_eq_elim (i : Option ℕ) : Redirect.vlift i = i.elim [some Redirect.marker, none] fun (b : ℕ) => if b = Redirect.marker then [] else [some b]

theorem Turing.MultiTapeTM.Universal.Hardwire.redirectEntry_hardwire (e : Key × Act) : Redirect.redirectEntry (fun (q : ℕ) => 2 * q + 1) none [] 0 id e = fun (s : Option ℕ) => ({ state := 2 * e.1.state + 1, input := none, work := s :: e.1.work }, { inputTape := SignType.zero, workTapes := (none, Redirect.vmove s e.2.inputTape) :: e.2.workTapes, output := e.2.output, state := Option.map (fun (q : ℕ) => 2 * q + 1) e.2.state })

The transitions of hardwire d p

theorem Turing.MultiTapeTM.Universal.Hardwire.computableTidilyInPolyTime_writeEntries : ComputableTidilyInPolyTime (fun (dp : Desc × List Bool) => writeEntries dp.2 dp.1.tapes) (encPair eDesc encBits) (encList (encPair eKey eAct))

theorem Turing.MultiTapeTM.Universal.Hardwire.computableTidilyInPolyTime_redirect : ComputableTidilyInPolyTime (fun (d : Desc) => Redirect.redirect (fun (q : ℕ) => 2 * q + 1) none [] 0 id d.table) eDesc (encList (encPair eKey eAct))

theorem Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_hardwire : ComputableTidilyInPolyTime (fun (dp : Desc × List Bool) => hardwire dp.1 dp.2) (encPair eDesc encBits) eDesc

The s-m-n theorem: the description with an input prefix built in, Turing.MultiTapeTM.Universal.hardwire d p, is computed from d and p in polynomial time.