The transition table of the simulating machine

The control of the machine M(c) of PCP-HARDNESS.md §2.8, as one deterministic step function DescriptiveComplexity.HaltHard.simStep : SimQ c → SimSym c → Option (SimSym c × SimQ c × Bool) (the Boolean is “move right”). Determinism is what makes the backward direction of the simulation a case analysis rather than an invariant hunt, and the drawn machine's transition relations are read off the graph of this function.

The tape layout is the one of Tags.lean: frames left of the fixed separator mid, bounded by the movable endL; the value mirrored right of mid, its head block ending at the movable endR, so that every operation on the head of the value works at endR and grows into the blank half-tape – no marker ever crosses a letter. The states fall into walk families between the unique letters endL/mid/endR/headers:

• retL/retR – seek the top frame (or accept on mid); retL doubles as the start state, the head starting on endL;
• nSeekL p/nSeekR p – walk to mid and dispatch on the shape of codeAt p;
• zGo/zEnd – zero': append a separator at endR;
• suScan/suE₁/suE₂/suGo/suEnd/suBack/suKill – succ: append a digit (a separator and a digit, if the value was empty), then erase every block but the head one;
• tlGo/tlLook/tlOnes/tlRest – tail: erase the head block at endR;
• caGo p/caLook p/caRest p – case: inspect and consume the head at endR, then dispatch a child;
• cpFetch p/cpCar₁ p/cpCarC p/cpEndS p/cpBack p/cpHdr p/ cpHdrS p/cpUnp p/cpUnp₂ p – the one non-destructive copy (the cons push), priming letters and writing at endL by the endL-shift;
• coHdr p/coHdrS p, fiHdr p/fiHdrS p – the bare header pushes;
• fxGo p/fxLook p/fxOnes p/fxRest p/fxDropL/fxDropR – the fix pop: inspect the flag at endR, then keep or drop the frame;
• swGo/swPeek/swCar₁/swCarC/swEndS/swRest/swHdr/swHdrS/ swOut/swScan/swLast/swApp₁/swAppC/swAppS/swBack – the cons₁ pop: move the value into a fresh cons₂ frame (consuming it at endR, so the frame stores it mirrored), then move the stored value out (consuming the frame at its right end, so the value region gets it mirrored);
• ppGo/ppShift/ppBack/ppFind/ppScan/ppLast/ppCar/ppCarS/ ppKill – the cons₂ pop: append a separator, transfer the digits of the frame's head block (sitting at the frame's right end, since the frame is mirrored), and discard the rest.

inductive DescriptiveComplexity.HaltHard.SimQ (c : Turing.ToPartrec.Code) : Type

The states of the simulating machine; see the module docstring for the role of each family.

• retL {c : Turing.ToPartrec.Code} : SimQ c

  Walk left to endL, then look for the top frame.

• retR {c : Turing.ToPartrec.Code} : SimQ c

  Walk right over the gap to the top frame; accept on mid.

• acc {c : Turing.ToPartrec.Code} : SimQ c

  The accepting state.

• nSeekL {c : Turing.ToPartrec.Code} : CPos c → SimQ c

  Walk left to mid and dispatch stepNormal (codeAt p).

• nSeekR {c : Turing.ToPartrec.Code} : CPos c → SimQ c

  Walk right to mid and dispatch stepNormal (codeAt p).

• zGo {c : Turing.ToPartrec.Code} : SimQ c

  zero': walk right to endR.

• zEnd {c : Turing.ToPartrec.Code} : SimQ c

  zero': re-write endR one cell right of the appended separator.

• suScan {c : Turing.ToPartrec.Code} : SimQ c

  succ: from mid, look whether the value is empty.

• suE₁ {c : Turing.ToPartrec.Code} : SimQ c

  succ on an empty value: a separator is appended; write the digit.

• suE₂ {c : Turing.ToPartrec.Code} : SimQ c

  succ on an empty value: re-write endR.

• suGo {c : Turing.ToPartrec.Code} : SimQ c

  succ: walk right to endR.

• suEnd {c : Turing.ToPartrec.Code} : SimQ c

  succ: re-write endR one cell right of the appended digit.

• suBack {c : Turing.ToPartrec.Code} : SimQ c

  succ: walk left over the head block's digits.

• suKill {c : Turing.ToPartrec.Code} : SimQ c

  succ: erase everything between the head block and mid.

• tlGo {c : Turing.ToPartrec.Code} : SimQ c

  tail: walk right to endR.

• tlLook {c : Turing.ToPartrec.Code} : SimQ c

  tail: look at the last letter of the value.

• tlOnes {c : Turing.ToPartrec.Code} : SimQ c

  tail: erase the head block's digits, then land endR on its separator.

• tlRest {c : Turing.ToPartrec.Code} : SimQ c

  tail on an empty value: re-write the erased endR.

• caGo {c : Turing.ToPartrec.Code} : CPos c → SimQ c

  case: walk right to endR.

• caLook {c : Turing.ToPartrec.Code} : CPos c → SimQ c

  case: look at the last letter of the value.

• caRest {c : Turing.ToPartrec.Code} : CPos c → SimQ c

  case on an empty value: re-write the erased endR.

• cpFetch {c : Turing.ToPartrec.Code} : CPos c → SimQ c

  cons push: find the next unprimed letter of the value.

• cpCar₁ {c : Turing.ToPartrec.Code} : CPos c → SimQ c

  cons push: carry a digit to endL.

• cpCarC {c : Turing.ToPartrec.Code} : CPos c → SimQ c

  cons push: carry a separator to endL.

• cpEndS {c : Turing.ToPartrec.Code} : CPos c → SimQ c

  cons push: re-write endL one cell left.

• cpBack {c : Turing.ToPartrec.Code} : CPos c → SimQ c

  cons push: walk right back to mid before resuming the scan.

• cpHdr {c : Turing.ToPartrec.Code} : CPos c → SimQ c

  cons push: walk left to endL to write the frame header.

• cpHdrS {c : Turing.ToPartrec.Code} : CPos c → SimQ c

  cons push: re-write endL left of the header.

• cpUnp {c : Turing.ToPartrec.Code} : CPos c → SimQ c

  cons push: walk right to mid before unpriming.

• cpUnp₂ {c : Turing.ToPartrec.Code} : CPos c → SimQ c

  cons push: unprime the copied value.

• coHdr {c : Turing.ToPartrec.Code} : CPos c → SimQ c

  comp push: walk left to endL.

• coHdrS {c : Turing.ToPartrec.Code} : CPos c → SimQ c

  comp push: re-write endL left of the header.

• fiHdr {c : Turing.ToPartrec.Code} : CPos c → SimQ c

  fix push: walk left to endL.

• fiHdrS {c : Turing.ToPartrec.Code} : CPos c → SimQ c

  fix push: re-write endL left of the header.

• fxGo {c : Turing.ToPartrec.Code} : CPos c → SimQ c

  fix pop: walk right to endR.

• fxLook {c : Turing.ToPartrec.Code} : CPos c → SimQ c

  fix pop: look at the last letter of the value.

• fxOnes {c : Turing.ToPartrec.Code} : CPos c → SimQ c

  fix pop, nonzero flag: erase the head block's digits.

• fxRest {c : Turing.ToPartrec.Code} : CPos c → SimQ c

  fix pop on an empty value: re-write the erased endR.

• fxDropL {c : Turing.ToPartrec.Code} : SimQ c

  fix pop, zero flag: walk left to endL to drop the frame.

• fxDropR {c : Turing.ToPartrec.Code} : SimQ c

  fix pop, zero flag: walk right to the frame header and erase it.

• swGo {c : Turing.ToPartrec.Code} : SimQ c

  cons₁ pop: walk right to endR.

• swPeek {c : Turing.ToPartrec.Code} : SimQ c

  cons₁ pop: look at the last letter of the value.

• swCar₁ {c : Turing.ToPartrec.Code} : SimQ c

  cons₁ pop: carry a digit to endL.

• swCarC {c : Turing.ToPartrec.Code} : SimQ c

  cons₁ pop: carry a separator to endL.

• swEndS {c : Turing.ToPartrec.Code} : SimQ c

  cons₁ pop: re-write endL one cell left.

• swRest {c : Turing.ToPartrec.Code} : SimQ c

  cons₁ pop: the value is spent; re-write the erased endR.

• swHdr {c : Turing.ToPartrec.Code} : SimQ c

  cons₁ pop: walk left to endL to write the cons₂ header.

• swHdrS {c : Turing.ToPartrec.Code} : SimQ c

  cons₁ pop: re-write endL left of the header.

• swOut {c : Turing.ToPartrec.Code} : SimQ c

  cons₁ pop: walk right to the old frame's header.

• swScan {c : Turing.ToPartrec.Code} : SimQ c

  cons₁ pop: walk right over the old frame's content.

• swLast {c : Turing.ToPartrec.Code} : SimQ c

  cons₁ pop: consume the old frame's last letter.

• swApp₁ {c : Turing.ToPartrec.Code} : SimQ c

  cons₁ pop: carry a digit to endR.

• swAppC {c : Turing.ToPartrec.Code} : SimQ c

  cons₁ pop: carry a separator to endR.

• swAppS {c : Turing.ToPartrec.Code} : SimQ c

  cons₁ pop: re-write endR one cell right.

• swBack {c : Turing.ToPartrec.Code} : SimQ c

  cons₁ pop: walk left to endL before re-entering the frame.

• ppGo {c : Turing.ToPartrec.Code} : SimQ c

  cons₂ pop: walk right to endR to append the separator.

• ppShift {c : Turing.ToPartrec.Code} : SimQ c

  cons₂ pop: re-write endR one cell right.

• ppBack {c : Turing.ToPartrec.Code} : SimQ c

  cons₂ pop: walk left to endL.

• ppFind {c : Turing.ToPartrec.Code} : SimQ c

  cons₂ pop: walk right over the gap to the frame.

• ppScan {c : Turing.ToPartrec.Code} : SimQ c

  cons₂ pop: walk right over the frame's content.

• ppLast {c : Turing.ToPartrec.Code} : SimQ c

  cons₂ pop: consume the frame's last letter.

• ppCar {c : Turing.ToPartrec.Code} : SimQ c

  cons₂ pop: carry a digit to endR.

• ppCarS {c : Turing.ToPartrec.Code} : SimQ c

  cons₂ pop: re-write endR one cell right.

• ppKill {c : Turing.ToPartrec.Code} : SimQ c

  cons₂ pop: erase the spent frame.

instance DescriptiveComplexity.HaltHard.instNonemptySimQ {c : Turing.ToPartrec.Code} : Nonempty (SimQ c)

instance DescriptiveComplexity.HaltHard.instFiniteSimQ {c : Turing.ToPartrec.Code} : Finite (SimQ c)

The states are finitely many: CPos c is finite and every family is indexed by at most one position.

def DescriptiveComplexity.HaltHard.dispatch {c : Turing.ToPartrec.Code} (p : CPos c) : SimSym c × SimQ c × Bool

The dispatch of stepNormal (codeAt p), with the head reading mid: the first action of each shape's handler.

Equations

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

def DescriptiveComplexity.HaltHard.simStep {c : Turing.ToPartrec.Code} : SimQ c → SimSym c → Option (SimSym c × SimQ c × Bool)

The deterministic step table (none = no move; the Boolean is “move right”). The docstring of the file names each family; within a family the letter-specific actions come first and the walk catch-alls after.