The simulating machine as rewriting, and the transport to a drawn machine

Two bridges. The first identifies runs of the zipper semantics (DescriptiveComplexity.HaltHard.lstep) with derivations of the rewriting system DescriptiveComplexity.HaltPcp.MRule of the machine packaged as a DescriptiveComplexity.TMData (DescriptiveComplexity.HaltHard.simTM, over the three-block universe DescriptiveComplexity.HaltHard.SimU – states, symbols, and one transition per applicable state–symbol pair; the machine is deterministic, so the pair is the transition). A zipper configuration is a configuration word (DescriptiveComplexity.HaltHard.wordOf), one lstep is one rewriting step, and the boot and halting phases close the two ends: DescriptiveComplexity.HaltHard.derives_startWord_iff_evalDom states the result directly against Turing.ToPartrec.Cont.eval, through DescriptiveComplexity.HaltHard.reach_acc_iff_evalDom.

The second bridge is the rule-correspondence transport: a machine whose predicates are the images of simTM's along an injection (DescriptiveComplexity.HaltHard.TMEmbed – the shape of the machine the interpretation of Interp.lean draws, whose universe also carries the tape positions and the junk) derives the halting word from an image word exactly when simTM does from its preimage (DescriptiveComplexity.HaltHard.TMEmbed.derives_halt_iff). Together with DescriptiveComplexity.HaltPcp.acceptsU_iff_derives on the drawn side, this turns DescriptiveComplexity.TMData.AcceptsU of the drawn machine into termination of the abstract evaluation, with no tape-function bookkeeping.

The universe of the simulating machine

@[reducible, inline]

abbrev DescriptiveComplexity.HaltHard.SimU (c : Turing.ToPartrec.Code) : Type

The universe of the simulating machine as a DescriptiveComplexity.TMData: states, symbols, and one transition per state–symbol pair the table acts on.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.HaltHard.stq {c : Turing.ToPartrec.Code} (q : SimQ c) : SimU c

A state, as an element of the machine universe.

Equations

• DescriptiveComplexity.HaltHard.stq q = Sum.inl q

@[reducible, inline]

abbrev DescriptiveComplexity.HaltHard.sts {c : Turing.ToPartrec.Code} (σ : SimSym c) : SimU c

A symbol, as an element of the machine universe.

Equations

• DescriptiveComplexity.HaltHard.sts σ = Sum.inr (Sum.inl σ)

@[reducible, inline]

abbrev DescriptiveComplexity.HaltHard.stt {c : Turing.ToPartrec.Code} (τ : SimQ c × SimSym c) : SimU c

A transition – a state–symbol pair – as an element of the machine universe.

Equations

• DescriptiveComplexity.HaltHard.stt τ = Sum.inr (Sum.inr τ)

def DescriptiveComplexity.HaltHard.simTM (c : Turing.ToPartrec.Code) : TMData (SimU c)

The simulating machine as machine data: one transition per pair on which the table acts, its attributes read off simStep. The position block is empty – the rewriting system of a machine never mentions positions, and the bridge to a drawn machine goes through words alone.

Equations

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

Zipper configurations as words

def DescriptiveComplexity.HaltHard.symsOf {c : Turing.ToPartrec.Code} (l : List (SimSym c)) : List (HaltPcp.TapeLetter (SimU c))

The symbol letters of a run of tape letters.

Equations

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

@[simp]

theorem DescriptiveComplexity.HaltHard.symsOf_nil {c : Turing.ToPartrec.Code} : symsOf [] = []

@[simp]

theorem DescriptiveComplexity.HaltHard.symsOf_cons {c : Turing.ToPartrec.Code} (σ : SimSym c) (l : List (SimSym c)) : symsOf (σ :: l) = HaltPcp.TapeLetter.sym (sts σ) :: symsOf l

@[simp]

theorem DescriptiveComplexity.HaltHard.symsOf_append {c : Turing.ToPartrec.Code} (l l' : List (SimSym c)) : symsOf (l ++ l') = symsOf l ++ symsOf l'

def DescriptiveComplexity.HaltHard.wordOf {c : Turing.ToPartrec.Code} (x : LCfg c) : List (HaltPcp.TapeLetter (SimU c))

The word of a zipper configuration: the recorded cells left to right between the endmarkers, the state letter wedged before the head's cell.

Equations

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

theorem DescriptiveComplexity.HaltHard.halt_not_mem_wordOf {c : Turing.ToPartrec.Code} (x : LCfg c) : HaltPcp.TapeLetter.halt ∉ wordOf x

theorem DescriptiveComplexity.HaltHard.boot_not_mem_wordOf {c : Turing.ToPartrec.Code} (x : LCfg c) : HaltPcp.TapeLetter.boot ∉ wordOf x

Locating the unique marked letter

theorem DescriptiveComplexity.HaltHard.eq_of_unique_marked {Γ : Type} {P : Γ → Prop} {A x : List Γ} {s s' : Γ} {B y : List Γ} : (∀ a ∈ A, ¬P a) → (∀ a ∈ B, ¬P a) → P s' → A ++ s :: B = x ++ s' :: y → A = x ∧ s = s' ∧ B = y

Splitting a list at a marked letter when the reference decomposition has none on either side: the two decompositions coincide.

def DescriptiveComplexity.HaltHard.IsStateL {c : Turing.ToPartrec.Code} (a : HaltPcp.TapeLetter (SimU c)) : Prop

Being a state letter.

Equations

• DescriptiveComplexity.HaltHard.IsStateL a = ∃ (u : DescriptiveComplexity.HaltHard.SimU c), a = DescriptiveComplexity.HaltPcp.TapeLetter.state u

theorem DescriptiveComplexity.HaltHard.not_isStateL_left {c : Turing.ToPartrec.Code} (L : List (SimSym c)) (a : HaltPcp.TapeLetter (SimU c)) : a ∈ HaltPcp.TapeLetter.lft :: symsOf L → ¬IsStateL a

theorem DescriptiveComplexity.HaltHard.not_isStateL_right {c : Turing.ToPartrec.Code} (s : SimSym c) (R : List (SimSym c)) (a : HaltPcp.TapeLetter (SimU c)) : a ∈ HaltPcp.TapeLetter.sym (sts s) :: (symsOf R ++ [HaltPcp.TapeLetter.rgt]) → ¬IsStateL a

theorem DescriptiveComplexity.HaltHard.wordOf_state_split {c : Turing.ToPartrec.Code} {q : SimQ c} {L : List (SimSym c)} {s : SimSym c} {R : List (SimSym c)} {u v : List (HaltPcp.TapeLetter (SimU c))} {w : SimU c} {m : List (HaltPcp.TapeLetter (SimU c))} (h : wordOf { q := q, L := L, s := s, R := R } = u ++ HaltPcp.TapeLetter.state w :: m ++ v) : u = HaltPcp.TapeLetter.lft :: symsOf L.reverse ∧ w = stq q ∧ m ++ v = HaltPcp.TapeLetter.sym (sts s) :: (symsOf R ++ [HaltPcp.TapeLetter.rgt])

Splitting the word of a configuration at a state letter: the state letter is the configuration's, and the two sides are its two half-tapes.

Decoding the attributes of a transition

theorem DescriptiveComplexity.HaltHard.decode_attrs {c : Turing.ToPartrec.Code} {τ u a u' b : SimU c} (hsrc : (simTM c).Src τ u) (hread : (simTM c).Read τ a) (hdst : (simTM c).Dst τ u') (hwrite : (simTM c).Write τ b) : ∃ (q : SimQ c) (σ : SimSym c) (b₀ : SimSym c) (q₀ : SimQ c) (d : Bool), u = stq q ∧ a = sts σ ∧ simStep q σ = some (b₀, q₀, d) ∧ u' = stq q₀ ∧ b = sts b₀ ∧ ((simTM c).Right τ ↔ d = true)

The attribute values of a transition of simTM all decode through one application of the table, and its direction is the Right predicate.

One machine step is one rewriting step

theorem DescriptiveComplexity.HaltHard.step_wordOf {c : Turing.ToPartrec.Code} {x y : LCfg c} (h : lstep x = some y) : Pcp.History.Step (HaltPcp.MRule (simTM c)) (wordOf x) (wordOf y)

Forward: one zipper step rewrites the word by one move rule.

theorem DescriptiveComplexity.HaltHard.step_inversion_wordOf {c : Turing.ToPartrec.Code} {x : LCfg c} {w : List (HaltPcp.TapeLetter (SimU c))} (h : Pcp.History.Step (HaltPcp.MRule (simTM c)) (wordOf x) w) : (∃ (y : LCfg c), lstep x = some y ∧ w = wordOf y) ∨ x.q = SimQ.acc

Backward: a rewriting step from a configuration word either performs the configuration's own machine step, or fires the halting rule – in which case the configuration accepts.

Whole runs

theorem DescriptiveComplexity.HaltHard.derives_wordOf_of_reach {c : Turing.ToPartrec.Code} {x y : LCfg c} (h : Reach x y) : Pcp.History.Derives (HaltPcp.MRule (simTM c)) (wordOf x) (wordOf y)

A run of the machine is a derivation between the two words.

theorem DescriptiveComplexity.HaltHard.derives_halt_of_acc {c : Turing.ToPartrec.Code} {x : LCfg c} (hx : x.q = SimQ.acc) : Pcp.History.Derives (HaltPcp.MRule (simTM c)) (wordOf x) [HaltPcp.TapeLetter.halt]

From an accepting configuration the derivation closes: the state letter becomes the halting letter, which swallows the rest of the word.

theorem DescriptiveComplexity.HaltHard.reach_acc_of_derives {c : Turing.ToPartrec.Code} {w : List (HaltPcp.TapeLetter (SimU c))} : Pcp.History.Derives (HaltPcp.MRule (simTM c)) w [HaltPcp.TapeLetter.halt] → ∀ (x : LCfg c), w = wordOf x → ∃ (y : LCfg c), y.q = SimQ.acc ∧ Reach x y

Backward: a derivation of the halting word from a configuration word yields an accepting run of the machine.

The boot phase, and the abstract statement

theorem DescriptiveComplexity.HaltHard.derives_startWord_iff {c : Turing.ToPartrec.Code} (σ₀ : SimSym c) (R₀ : List (SimSym c)) : Pcp.History.Derives (HaltPcp.MRule (simTM c)) (HaltPcp.startWord (List.map sts (σ₀ :: R₀))) [HaltPcp.TapeLetter.halt] ↔ ∃ (y : LCfg c), y.q = SimQ.acc ∧ Reach { q := SimQ.retL, L := [], s := σ₀, R := R₀ } y

Derivability from the start word is machine acceptance, at the zipper: the first step of any derivation is the boot rule, and boot lands the machine in the resting state at the left end of the spelled tape.

theorem DescriptiveComplexity.HaltHard.derives_startWord_iff_evalDom {c : Turing.ToPartrec.Code} {k : PCont c} {fr : List (SimSym c)} (hfr : FrameSeg k fr) (v : List ℕ) (j t : ℕ) : Pcp.History.Derives (HaltPcp.MRule (simTM c)) (HaltPcp.startWord (List.map sts (SimSym.endL :: (fr ++ SimSym.mid :: valR v j t)))) [HaltPcp.TapeLetter.halt] ↔ (k.toCont.eval v).Dom

The abstract bridge: the rewriting system of the simulating machine derives the halting word from the spelled resting configuration of k and v exactly when the abstract evaluation of k on v terminates.

Transport along an injection

The machine the interpretation draws has the same states, symbols and transitions, embedded in a larger universe that also carries the tape positions and the junk. Its predicates are the images of the abstract ones, and derivations of the halting word correspond exactly.

def DescriptiveComplexity.HaltPcp.TapeLetter.map {A B : Type} (f : A → B) : TapeLetter A → TapeLetter B

Mapping the machine elements of a tape letter.

Equations

• DescriptiveComplexity.HaltPcp.TapeLetter.map f DescriptiveComplexity.HaltPcp.TapeLetter.lft = DescriptiveComplexity.HaltPcp.TapeLetter.lft
• DescriptiveComplexity.HaltPcp.TapeLetter.map f DescriptiveComplexity.HaltPcp.TapeLetter.rgt = DescriptiveComplexity.HaltPcp.TapeLetter.rgt
• DescriptiveComplexity.HaltPcp.TapeLetter.map f DescriptiveComplexity.HaltPcp.TapeLetter.boot = DescriptiveComplexity.HaltPcp.TapeLetter.boot
• DescriptiveComplexity.HaltPcp.TapeLetter.map f DescriptiveComplexity.HaltPcp.TapeLetter.halt = DescriptiveComplexity.HaltPcp.TapeLetter.halt
• DescriptiveComplexity.HaltPcp.TapeLetter.map f (DescriptiveComplexity.HaltPcp.TapeLetter.sym a) = DescriptiveComplexity.HaltPcp.TapeLetter.sym (f a)
• DescriptiveComplexity.HaltPcp.TapeLetter.map f (DescriptiveComplexity.HaltPcp.TapeLetter.state a) = DescriptiveComplexity.HaltPcp.TapeLetter.state (f a)

structure DescriptiveComplexity.HaltHard.TMEmbed {A B : Type} (f : A → B) (M : TMData A) (N : TMData B) : Prop

A machine embedded in a larger universe: an injection under which every predicate of the target is the image of the corresponding predicate of the source.

• inj : Function.Injective f

  The embedding is injective.

• tr (b : B) : N.Tr b ↔ ∃ (a : A), b = f a ∧ M.Tr a

  Transitions correspond.

• start (b : B) : N.Start b ↔ ∃ (a : A), b = f a ∧ M.Start a

  Start states correspond.

• acc (b : B) : N.Acc b ↔ ∃ (a : A), b = f a ∧ M.Acc a

  Accepting states correspond.

• blank (b : B) : N.Blank b ↔ ∃ (a : A), b = f a ∧ M.Blank a

  Blanks correspond.

• right (b : B) : N.Right b ↔ ∃ (a : A), b = f a ∧ M.Right a

  Directions correspond.

• src (b b' : B) : N.Src b b' ↔ ∃ (a : A) (a' : A), b = f a ∧ b' = f a' ∧ M.Src a a'

  Source states correspond.

• read (b b' : B) : N.Read b b' ↔ ∃ (a : A) (a' : A), b = f a ∧ b' = f a' ∧ M.Read a a'

  Read symbols correspond.

• dst (b b' : B) : N.Dst b b' ↔ ∃ (a : A) (a' : A), b = f a ∧ b' = f a' ∧ M.Dst a a'

  Destination states correspond.

• write (b b' : B) : N.Write b b' ↔ ∃ (a : A) (a' : A), b = f a ∧ b' = f a' ∧ M.Write a a'

  Written symbols correspond.

theorem DescriptiveComplexity.HaltPcp.startWord_map {A B : Type} (f : A → B) (inp : List A) : List.map (TapeLetter.map f) (startWord inp) = startWord (List.map f inp)

The start word is mapped letterwise.

theorem DescriptiveComplexity.HaltHard.TMEmbed.mRule_map {A B : Type} {f : A → B} {M : TMData A} {N : TMData B} (h : TMEmbed f M N) {l r : List (HaltPcp.TapeLetter A)} (hrule : HaltPcp.MRule M l r) : HaltPcp.MRule N (List.map (HaltPcp.TapeLetter.map f) l) (List.map (HaltPcp.TapeLetter.map f) r)

Forward transport of a rule.

Decomposing image words

theorem DescriptiveComplexity.HaltHard.TMEmbed.cons_eq_map {α β : Type} {f : α → β} {x : β} {xs : List β} {l : List α} (h : x :: xs = List.map f l) : ∃ (a : α) (l₀ : List α), l = a :: l₀ ∧ x = f a ∧ xs = List.map f l₀

theorem DescriptiveComplexity.HaltHard.TMEmbed.nil_eq_map {α β : Type} {f : α → β} {l : List α} (h : [] = List.map f l) : l = []

theorem DescriptiveComplexity.HaltHard.TMEmbed.append_eq_map {α β : Type} {f : α → β} {x y : List β} {l : List α} : x ++ y = List.map f l → ∃ (lx : List α) (ly : List α), l = lx ++ ly ∧ x = List.map f lx ∧ y = List.map f ly

theorem DescriptiveComplexity.HaltHard.TMEmbed.eq_map_state {A B : Type} {f : A → B} {a : HaltPcp.TapeLetter A} {q : B} (h : HaltPcp.TapeLetter.state q = HaltPcp.TapeLetter.map f a) : ∃ (q₀ : A), a = HaltPcp.TapeLetter.state q₀ ∧ q = f q₀

theorem DescriptiveComplexity.HaltHard.TMEmbed.eq_map_sym {A B : Type} {f : A → B} {a : HaltPcp.TapeLetter A} {q : B} (h : HaltPcp.TapeLetter.sym q = HaltPcp.TapeLetter.map f a) : ∃ (q₀ : A), a = HaltPcp.TapeLetter.sym q₀ ∧ q = f q₀

theorem DescriptiveComplexity.HaltHard.TMEmbed.eq_map_lft {A B : Type} {f : A → B} {a : HaltPcp.TapeLetter A} (h : HaltPcp.TapeLetter.lft = HaltPcp.TapeLetter.map f a) : a = HaltPcp.TapeLetter.lft

theorem DescriptiveComplexity.HaltHard.TMEmbed.eq_map_rgt {A B : Type} {f : A → B} {a : HaltPcp.TapeLetter A} (h : HaltPcp.TapeLetter.rgt = HaltPcp.TapeLetter.map f a) : a = HaltPcp.TapeLetter.rgt

theorem DescriptiveComplexity.HaltHard.TMEmbed.eq_map_boot {A B : Type} {f : A → B} {a : HaltPcp.TapeLetter A} (h : HaltPcp.TapeLetter.boot = HaltPcp.TapeLetter.map f a) : a = HaltPcp.TapeLetter.boot

theorem DescriptiveComplexity.HaltHard.TMEmbed.eq_map_halt {A B : Type} {f : A → B} {a : HaltPcp.TapeLetter A} (h : HaltPcp.TapeLetter.halt = HaltPcp.TapeLetter.map f a) : a = HaltPcp.TapeLetter.halt

theorem DescriptiveComplexity.HaltHard.TMEmbed.mRule_inv {A B : Type} {f : A → B} {M : TMData A} {N : TMData B} (h : TMEmbed f M N) {l' r' : List (HaltPcp.TapeLetter B)} (hrule : HaltPcp.MRule N l' r') {l : List (HaltPcp.TapeLetter A)} (hl : l' = List.map (HaltPcp.TapeLetter.map f) l) : ∃ (r : List (HaltPcp.TapeLetter A)), r' = List.map (HaltPcp.TapeLetter.map f) r ∧ HaltPcp.MRule M l r

Backward transport of a rule: a target rule whose left side is an image has an image right side, and comes from a source rule.

theorem DescriptiveComplexity.HaltHard.TMEmbed.step_map {A B : Type} {f : A → B} {M : TMData A} {N : TMData B} (h : TMEmbed f M N) {u v : List (HaltPcp.TapeLetter A)} (hs : Pcp.History.Step (HaltPcp.MRule M) u v) : Pcp.History.Step (HaltPcp.MRule N) (List.map (HaltPcp.TapeLetter.map f) u) (List.map (HaltPcp.TapeLetter.map f) v)

Forward transport of a rewriting step.

theorem DescriptiveComplexity.HaltHard.TMEmbed.step_inv {A B : Type} {f : A → B} {M : TMData A} {N : TMData B} (h : TMEmbed f M N) {W : List (HaltPcp.TapeLetter A)} {w' : List (HaltPcp.TapeLetter B)} (hs : Pcp.History.Step (HaltPcp.MRule N) (List.map (HaltPcp.TapeLetter.map f) W) w') : ∃ (V : List (HaltPcp.TapeLetter A)), w' = List.map (HaltPcp.TapeLetter.map f) V ∧ Pcp.History.Step (HaltPcp.MRule M) W V

Backward transport of a rewriting step: from an image word, every step lands on an image word, by the image step.

theorem DescriptiveComplexity.HaltHard.TMEmbed.derives_map {A B : Type} {f : A → B} {M : TMData A} {N : TMData B} (h : TMEmbed f M N) {u v : List (HaltPcp.TapeLetter A)} (hd : Pcp.History.Derives (HaltPcp.MRule M) u v) : Pcp.History.Derives (HaltPcp.MRule N) (List.map (HaltPcp.TapeLetter.map f) u) (List.map (HaltPcp.TapeLetter.map f) v)

Forward transport of a derivation.

theorem DescriptiveComplexity.HaltHard.TMEmbed.derives_halt_of_map {A B : Type} {f : A → B} {M : TMData A} {N : TMData B} (h : TMEmbed f M N) {w' : List (HaltPcp.TapeLetter B)} : Pcp.History.Derives (HaltPcp.MRule N) w' [HaltPcp.TapeLetter.halt] → ∀ {w : List (HaltPcp.TapeLetter A)}, w' = List.map (HaltPcp.TapeLetter.map f) w → Pcp.History.Derives (HaltPcp.MRule M) w [HaltPcp.TapeLetter.halt]

Backward transport of a derivation of the halting word.

theorem DescriptiveComplexity.HaltHard.TMEmbed.derives_halt_iff {A B : Type} {f : A → B} {M : TMData A} {N : TMData B} (h : TMEmbed f M N) {w : List (HaltPcp.TapeLetter A)} : Pcp.History.Derives (HaltPcp.MRule N) (List.map (HaltPcp.TapeLetter.map f) w) [HaltPcp.TapeLetter.halt] ↔ Pcp.History.Derives (HaltPcp.MRule M) w [HaltPcp.TapeLetter.halt]

Derivations of the halting word transport along an embedding.

theorem DescriptiveComplexity.HaltHard.TMEmbed.derives_iff_evalDom {c : Turing.ToPartrec.Code} {B : Type} {f : SimU c → B} {N : TMData B} (h : TMEmbed f (simTM c) N) {k : PCont c} {fr : List (SimSym c)} (hfr : FrameSeg k fr) (v : List ℕ) (j t : ℕ) : Pcp.History.Derives (HaltPcp.MRule N) (HaltPcp.startWord (List.map f (List.map sts (SimSym.endL :: (fr ++ SimSym.mid :: valR v j t))))) [HaltPcp.TapeLetter.halt] ↔ (k.toCont.eval v).Dom

The whole bridge, for a drawn machine: a machine whose predicates are the images of simTM's derives the halting word from the image of the spelled resting configuration exactly when the abstract evaluation terminates.