Documentation

DescriptiveComplexity.Problems.Machine.HaltHard.SimCons

The cons push, and the assembled dispatch simulation #

The one non-destructive copy of the machine: dispatching a cons copies the value into a fresh cons₁ frame at endL, priming each letter on the way so the scan finds the next one, then unprimes the value and dispatches the first child. DescriptiveComplexity.HaltHard.cp_loop is the copy loop – one iteration primes one letter, carries it home and returns – and DescriptiveComplexity.HaltHard.norm_cons wraps it with the header write and the unpriming sweep.

With every code shape handled, DescriptiveComplexity.HaltHard.sim_norm assembles the whole dispatch phase: from the dispatch of the code at p, the machine reaches the resting configuration of DescriptiveComplexity.HaltHard.pStepNormal p k v, by induction on the size of the dispatched code.

Priming #

source
def DescriptiveComplexity.HaltHard.prime {c : Turing.ToPartrec.Code} :
SimSym c → SimSym c

Marking a letter as copied.

Equations
Instances For
    Dependency graph

    Fused step-and-walk combinators #

    Pass lemmas for the copy #

    The copy loop #

    source
    theorem DescriptiveComplexity.HaltHard.cp_loop {c : Turing.ToPartrec.Code} (p : CPos c) (U P : List (SimSym c)) :
    (∀ σ ∈ U, σ = SimSym.one ∨ σ = SimSym.com) → (∀ σ ∈ P, σ = SimSym.one ∨ σ = SimSym.com) → ∀ (g : ℕ) {fr : List (SimSym c)}, (∀ σ ∈ fr, FrameSym σ) → ∀ (j t : ℕ), Reach { q := SimQ.cpFetch p, L := SimSym.mid :: (fr.reverse ++ (P ++ SimSym.endL :: List.replicate g SimSym.bk)), s := SimSym.bk, R := List.replicate j SimSym.bk ++ (List.map prime P ++ (U ++ SimSym.endR :: List.replicate t SimSym.bk)) } { q := SimQ.cpFetch p, L := (List.replicate j SimSym.bk ++ List.map prime (P ++ U)).reverse ++ SimSym.bk :: SimSym.mid :: (fr.reverse ++ (P ++ U ++ SimSym.endL :: List.replicate (g - U.length) SimSym.bk)), s := SimSym.endR, R := List.replicate t SimSym.bk }

    One pass of the copy loop, iterated to the end of the value: with the prefix P already primed and copied and U still to do, the scan fetches each letter of U in turn, carries it to endL, writes it by the endL-shift and returns; the loop ends with the scan on endR. The copied content sits between endL and the old frame region, spatially reversed – which is what makes it encVal v when the value region held (encVal v).reverse.

    Dependency graph
    source
    theorem DescriptiveComplexity.HaltHard.norm_cons {c : Turing.ToPartrec.Code} {p : CPos c} {f fs : Turing.ToPartrec.Code} (h : codeAt p = f.cons fs) {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.nSeekL (c₁ p)) (g - ((encVal v).length + 1)) (SimSym.hCons₁ (c₂ p) :: (encVal v ++ fr)) v j t)

    The cons dispatch: copy the value into a fresh cons₁ frame at endL – mirrored back to straight by the endL-shifts – write the header, unprime the value, and dispatch the first child.

    Dependency graph

    Reading pStepNormal off the code shape #

    The assembled dispatch phase #

    source
    theorem DescriptiveComplexity.HaltHard.sim_norm {c : Turing.ToPartrec.Code} (n : ℕ) (p : CPos c) :
    sizeOf (codeAt p) ≤ n → ∀ (k : PCont c) (v : List ℕ) {Q : SimQ c}, simStep Q SimSym.mid = some (dispatch p) → ∀ (g : ℕ) {fr : List (SimSym c)}, FrameSeg k fr → ∀ (j t : ℕ), ∃ (g' : ℕ) (fr' : List (SimSym c)) (j' : ℕ) (t' : ℕ), FrameSeg (pStepNormal p k v).1 fr' ∧ Reach (atMid Q g fr v j t) (restCfg g' fr' (pStepNormal p k v).2 j' t')

    The dispatch phase of the simulation: from the dispatch of the code at p – any state that hands over to dispatch p on mid – the machine reaches the resting configuration of pStepNormal p k v, by induction on the size of the dispatched code.

    Dependency graph