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.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.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.

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.

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