The dispatch phase of the simulation

The first half of the simulation of Turing.ToPartrec.step by the machine of Table.lean: from the dispatch of a code at the separator mid, the machine reaches the resting configuration of the Turing.ToPartrec.Cfg that Turing.ToPartrec.stepNormal computes – in the positioned form DescriptiveComplexity.HaltHard.pStepNormal, whose projection to the library semantics is DescriptiveComplexity.HaltHard.pStepNormal_toCont.

The tape regions are described by DescriptiveComplexity.HaltHard.valR/midL/restCfg/atMid, and the frame region by the relation DescriptiveComplexity.HaltHard.FrameSeg, which spells a continuation as frames separated by arbitrary blank gaps. One lemma per code shape moves the machine from the dispatch at mid to the next dispatch (for the four node shapes, having pushed the frame) or back to rest (for the three leaves, having transformed the value); DescriptiveComplexity.HaltHard.sim_norm chains them by induction on the size of the dispatched code.

The tape regions

@[reducible, inline]

abbrev DescriptiveComplexity.HaltHard.valR {c : Turing.ToPartrec.Code} (v : List ℕ) (j t : ℕ) : List (SimSym c)

The value-region strip right of mid: the inner gap – never empty, so a separator can always be closed next to an empty value – the mirrored value, the right marker and the trailing blanks.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.HaltHard.midL {c : Turing.ToPartrec.Code} (g : ℕ) (fr : List (SimSym c)) : List (SimSym c)

The left context of a head sitting on mid: the frame region, the left marker, the left blanks.

Equations

• DescriptiveComplexity.HaltHard.midL g fr = fr.reverse ++ DescriptiveComplexity.HaltHard.SimSym.endL :: List.replicate g DescriptiveComplexity.HaltHard.SimSym.bk

@[reducible, inline]

abbrev DescriptiveComplexity.HaltHard.atMid {c : Turing.ToPartrec.Code} (Q : SimQ c) (g : ℕ) (fr : List (SimSym c)) (v : List ℕ) (j t : ℕ) : LCfg c

The configuration at the dispatch point: head on mid.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.HaltHard.restCfg {c : Turing.ToPartrec.Code} (g : ℕ) (fr : List (SimSym c)) (v : List ℕ) (j t : ℕ) : LCfg c

The resting configuration between abstract steps: head on endL in the seek state.

Equations

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

inductive DescriptiveComplexity.HaltHard.FrameSeg {c : Turing.ToPartrec.Code} : PCont c → List (SimSym c) → Prop

The frame region of a continuation: the frames in order, top first, separated by arbitrary blank gaps. A cons₁ frame stores its value straight, a cons₂ frame mirrored.

• halt {c : Turing.ToPartrec.Code} : FrameSeg PCont.halt []

  The empty continuation has an empty frame region.

• gap {c : Turing.ToPartrec.Code} {k : PCont c} {w : List (SimSym c)} : FrameSeg k w → FrameSeg k (SimSym.bk :: w)

  A blank gap may precede the frames.

• cons₁ {c : Turing.ToPartrec.Code} {p : CPos c} {as : List ℕ} {k : PCont c} {w : List (SimSym c)} : FrameSeg k w → FrameSeg (PCont.cons₁ p as k) (SimSym.hCons₁ p :: (encVal as ++ w))

  A cons₁ frame: header, then the stored value, straight.

• cons₂ {c : Turing.ToPartrec.Code} {ns : List ℕ} {k : PCont c} {w : List (SimSym c)} : FrameSeg k w → FrameSeg (PCont.cons₂ ns k) (SimSym.hCons₂ :: ((encVal ns).reverse ++ w))

  A cons₂ frame: header, then the stored value, mirrored.

• comp {c : Turing.ToPartrec.Code} {p : CPos c} {k : PCont c} {w : List (SimSym c)} : FrameSeg k w → FrameSeg (PCont.comp p k) (SimSym.hComp p :: w)

  A comp frame: a bare header.

• fix {c : Turing.ToPartrec.Code} {p : CPos c} {k : PCont c} {w : List (SimSym c)} : FrameSeg k w → FrameSeg (PCont.fix p k) (SimSym.hFix p :: w)

  A fix frame: a bare header.

def DescriptiveComplexity.HaltHard.FrameSym {c : Turing.ToPartrec.Code} (σ : SimSym c) : Prop

The letters a frame region can hold.

Equations

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

theorem DescriptiveComplexity.HaltHard.mem_encVal {c : Turing.ToPartrec.Code} {v : List ℕ} {σ : SimSym c} (h : σ ∈ encVal v) : σ = SimSym.one ∨ σ = SimSym.com

theorem DescriptiveComplexity.HaltHard.FrameSeg.mem_frameSym {c : Turing.ToPartrec.Code} {k : PCont c} {fr : List (SimSym c)} (h : FrameSeg k fr) (σ : SimSym c) : σ ∈ fr → FrameSym σ

theorem DescriptiveComplexity.HaltHard.FrameSym.ne {c : Turing.ToPartrec.Code} {σ : SimSym c} (h : FrameSym σ) : σ ≠ SimSym.endL ∧ σ ≠ SimSym.mid ∧ σ ≠ SimSym.endR ∧ σ ≠ SimSym.one' ∧ σ ≠ SimSym.com'

What a frame letter is not: none of the markers, none of the primes.

Pass lemmas

Each walk state passes every letter but its stop letter; the catch-all rows of the table make these case bashes.

theorem DescriptiveComplexity.HaltHard.pass_retL {c : Turing.ToPartrec.Code} {σ : SimSym c} (h : σ ≠ SimSym.endL) : simStep SimQ.retL σ = some (σ, SimQ.retL, false)

theorem DescriptiveComplexity.HaltHard.pass_nSeekL {c : Turing.ToPartrec.Code} {σ : SimSym c} {p : CPos c} (h : σ ≠ SimSym.mid) : simStep (SimQ.nSeekL p) σ = some (σ, SimQ.nSeekL p, false)

theorem DescriptiveComplexity.HaltHard.pass_nSeekR {c : Turing.ToPartrec.Code} {σ : SimSym c} {p : CPos c} (h : σ ≠ SimSym.mid) : simStep (SimQ.nSeekR p) σ = some (σ, SimQ.nSeekR p, true)

theorem DescriptiveComplexity.HaltHard.pass_zGo {c : Turing.ToPartrec.Code} {σ : SimSym c} (h : σ ≠ SimSym.endR) : simStep SimQ.zGo σ = some (σ, SimQ.zGo, true)

theorem DescriptiveComplexity.HaltHard.pass_suGo {c : Turing.ToPartrec.Code} {σ : SimSym c} (h : σ ≠ SimSym.endR) : simStep SimQ.suGo σ = some (σ, SimQ.suGo, true)

theorem DescriptiveComplexity.HaltHard.pass_tlGo {c : Turing.ToPartrec.Code} {σ : SimSym c} (h : σ ≠ SimSym.endR) : simStep SimQ.tlGo σ = some (σ, SimQ.tlGo, true)

theorem DescriptiveComplexity.HaltHard.pass_caGo {c : Turing.ToPartrec.Code} {σ : SimSym c} {p : CPos c} (h : σ ≠ SimSym.endR) : simStep (SimQ.caGo p) σ = some (σ, SimQ.caGo p, true)

theorem DescriptiveComplexity.HaltHard.pass_coHdr {c : Turing.ToPartrec.Code} {σ : SimSym c} {p : CPos c} (h : σ ≠ SimSym.endL) : simStep (SimQ.coHdr p) σ = some (σ, SimQ.coHdr p, false)

theorem DescriptiveComplexity.HaltHard.pass_fiHdr {c : Turing.ToPartrec.Code} {σ : SimSym c} {p : CPos c} (h : σ ≠ SimSym.endL) : simStep (SimQ.fiHdr p) σ = some (σ, SimQ.fiHdr p, false)

theorem DescriptiveComplexity.HaltHard.pass_suKill {c : Turing.ToPartrec.Code} {σ : SimSym c} (h : σ = SimSym.one ∨ σ = SimSym.com ∨ σ = SimSym.bk) : simStep SimQ.suKill σ = some (SimSym.bk, SimQ.suKill, false)

theorem DescriptiveComplexity.HaltHard.Reach.cast {c : Turing.ToPartrec.Code} {x x' y y' : LCfg c} (hx : x = x') (hy : y = y') (h : Reach x' y') : Reach x y

Reachability transported along equalities of the two configurations.

theorem DescriptiveComplexity.HaltHard.replicate_glue {c : Turing.ToPartrec.Code} (a : SimSym c) (n : ℕ) (R : List (SimSym c)) : List.replicate n a ++ a :: R = List.replicate (n + 1) a ++ R

Gluing the letter behind the head back onto a run of its own kind – the shape the region equalities take after a walk re-crosses a run it wrote.

Hand-over walks

Each phase of a dispatch is one step that hands over to a walk state, followed by the walk itself: the combinators below package the two, so that an empty walked run – the hand-over landing directly on the stop letter – needs no case split at the use sites.

theorem DescriptiveComplexity.HaltHard.reach_step_walkR {c : Turing.ToPartrec.Code} {q q' : SimQ c} {P : SimSym c → Prop} {s σ' : SimSym c} (hs : simStep q s = some (σ', q', true)) (hq : ∀ (σ : SimSym c), P σ → simStep q' σ = some (σ, q', true)) (w : List (SimSym c)) (hw : ∀ σ ∈ w, P σ) (L : List (SimSym c)) (t : SimSym c) (R : List (SimSym c)) : Reach { q := q, L := L, s := s, R := w ++ t :: R } { q := q', L := w.reverse ++ σ' :: L, s := t, R := R }

A rightward hand-over step, then a rightward walk to the stop letter.

theorem DescriptiveComplexity.HaltHard.reach_step_walkL_map {c : Turing.ToPartrec.Code} {q q' : SimQ c} {P : SimSym c → Prop} {f : SimSym c → SimSym c} {s σ' : SimSym c} (hs : simStep q s = some (σ', q', false)) (hq : ∀ (σ : SimSym c), P σ → simStep q' σ = some (f σ, q', false)) (w : List (SimSym c)) (hw : ∀ σ ∈ w, P σ) (t : SimSym c) (L R : List (SimSym c)) : Reach { q := q, L := w ++ t :: L, s := s, R := R } { q := q', L := L, s := t, R := (List.map f w).reverse ++ σ' :: R }

A leftward hand-over step, then a leftward walk to the stop letter, rewriting each crossed letter by f.

theorem DescriptiveComplexity.HaltHard.reach_step_walkL {c : Turing.ToPartrec.Code} {q q' : SimQ c} {P : SimSym c → Prop} {s σ' : SimSym c} (hs : simStep q s = some (σ', q', false)) (hq : ∀ (σ : SimSym c), P σ → simStep q' σ = some (σ, q', false)) (w : List (SimSym c)) (hw : ∀ σ ∈ w, P σ) (t : SimSym c) (L R : List (SimSym c)) : Reach { q := q, L := w ++ t :: L, s := s, R := R } { q := q', L := L, s := t, R := w.reverse ++ σ' :: R }

A leftward hand-over step, then a leftward walk to the stop letter.

The positioned stepNormal

@[irreducible]

def DescriptiveComplexity.HaltHard.pStepNormal {c : Turing.ToPartrec.Code} (p : CPos c) (k : PCont c) (v : List ℕ) : PCont c × List ℕ

Turing.ToPartrec.stepNormal, over positions: the continuation and value of the configuration the dispatched code immediately becomes – stepNormal always returns a Cfg.ret, so a pair suffices.

Equations

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

theorem DescriptiveComplexity.HaltHard.pStepNormal_toCont {c : Turing.ToPartrec.Code} (p : CPos c) (k : PCont c) (v : List ℕ) : Turing.ToPartrec.stepNormal (codeAt p) k.toCont v = Turing.ToPartrec.Cfg.ret (pStepNormal p k v).1.toCont (pStepNormal p k v).2

The positioned stepNormal projects onto the library's.

The leaf dispatches

theorem DescriptiveComplexity.HaltHard.norm_zero' {c : Turing.ToPartrec.Code} {p : CPos c} (h : codeAt p = Turing.ToPartrec.Code.zero') {Q : SimQ c} (hQ : simStep Q SimSym.mid = some (dispatch p)) (g : ℕ) {fr : List (SimSym c)} (hfr : ∀ σ ∈ fr, FrameSym σ) (v : List ℕ) (j t : ℕ) : Reach (atMid Q g fr v j t) (restCfg g fr (0 :: v) j (t - 1))

zero': walk to endR, append a separator, return to rest. The value gains a 0 in front – a separator at the right end of the mirrored region.

theorem DescriptiveComplexity.HaltHard.norm_comp {c : Turing.ToPartrec.Code} {p : CPos c} {f g₂ : Turing.ToPartrec.Code} (h : codeAt p = f.comp g₂) {Q : SimQ c} (hQ : simStep Q SimSym.mid = some (dispatch p)) (g : ℕ) {fr : List (SimSym c)} (hfr : ∀ σ ∈ fr, FrameSym σ) (v : List ℕ) (j t : ℕ) : Reach (atMid Q g fr v j t) (atMid (SimQ.nSeekR (c₂ p)) (g - 1) (SimSym.hComp (c₁ p) :: fr) v j t)

comp push: walk left over the frames to endL, write the comp header over it, re-write endL one cell into the left blanks, and walk back to mid to dispatch the second child: the frame region gains a bare header, the left blanks lose a cell.

theorem DescriptiveComplexity.HaltHard.norm_succ {c : Turing.ToPartrec.Code} {p : CPos c} (h : codeAt p = Turing.ToPartrec.Code.succ) {Q : SimQ c} (hQ : simStep Q SimSym.mid = some (dispatch p)) (g : ℕ) {fr : List (SimSym c)} (hfr : ∀ σ ∈ fr, FrameSym σ) (v : List ℕ) (j t : ℕ) : ∃ (j' : ℕ) (t' : ℕ), Reach (atMid Q g fr v j t) (restCfg g fr [v.headI.succ] j' t')

succ: append a digit at endR – a fresh separator and a digit, if the value was empty – then walk back over the head block and erase every letter between it and mid: the value becomes the singleton successor of its head, the erased blocks joining the inner gap.

theorem DescriptiveComplexity.HaltHard.norm_tail {c : Turing.ToPartrec.Code} {p : CPos c} (h : codeAt p = Turing.ToPartrec.Code.tail) {Q : SimQ c} (hQ : simStep Q SimSym.mid = some (dispatch p)) (g : ℕ) {fr : List (SimSym c)} (hfr : ∀ σ ∈ fr, FrameSym σ) (v : List ℕ) (j t : ℕ) : ∃ (t' : ℕ), Reach (atMid Q g fr v j t) (restCfg g fr v.tail j t')

tail: walk to endR, erase it, and look at the last letter of the value – a blank for an empty value, restored after a probe step to its right; a lone separator, consumed; a digit, starting an erasure of the head block down to its separator – then re-write endR and return to rest.

theorem DescriptiveComplexity.HaltHard.norm_case_zero {c : Turing.ToPartrec.Code} {p : CPos c} {f g₂ : Turing.ToPartrec.Code} (h : codeAt p = f.case g₂) {Q : SimQ c} (hQ : simStep Q SimSym.mid = some (dispatch p)) (g : ℕ) {fr : List (SimSym c)} (_hfr : ∀ σ ∈ fr, FrameSym σ) {v : List ℕ} (hv : v.headI = 0) (j t : ℕ) : ∃ (t' : ℕ), Reach (atMid Q g fr v j t) (atMid (SimQ.nSeekL (c₁ p)) g fr v.tail j t')

case, zero or empty head: walk to endR, look left of it – a blank for an empty value, restored after a probe step to its right, or the head block's separator, consumed – re-write endR and walk back to mid to dispatch the first child on the tail of the value.

theorem DescriptiveComplexity.HaltHard.norm_case_succ {c : Turing.ToPartrec.Code} {p : CPos c} {f g₂ : Turing.ToPartrec.Code} (h : codeAt p = f.case g₂) {Q : SimQ c} (hQ : simStep Q SimSym.mid = some (dispatch p)) (g : ℕ) {fr : List (SimSym c)} (_hfr : ∀ σ ∈ fr, FrameSym σ) {v : List ℕ} {y : ℕ} (hv : v.headI = y + 1) (j t : ℕ) : ∃ (t' : ℕ), Reach (atMid Q g fr v j t) (atMid (SimQ.nSeekL (c₂ p)) g fr (y :: v.tail) j t')

case, positive head: walk to endR, find a digit left of it – the head block is nonempty – consume it as endR and walk back to mid to dispatch the second child on the decremented head.

theorem DescriptiveComplexity.HaltHard.norm_fix {c : Turing.ToPartrec.Code} {p : CPos c} {f : Turing.ToPartrec.Code} (h : codeAt p = f.fix) {Q : SimQ c} (hQ : simStep Q SimSym.mid = some (dispatch p)) (g : ℕ) {fr : List (SimSym c)} (hfr : ∀ σ ∈ fr, FrameSym σ) (v : List ℕ) (j t : ℕ) : Reach (atMid Q g fr v j t) (atMid (SimQ.nSeekR (c₁ p)) (g - 1) (SimSym.hFix (c₁ p) :: fr) v j t)

fix push: walk left over the frames to endL, write the fix header over it, re-write endL one cell into the left blanks, and walk back to mid to dispatch the body: the frame region gains a bare header, the left blanks lose a cell.