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 #

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

SimSym c → SimSym c

Marking a letter as copied.

Equations

Instances For

Dependency graph

def DescriptiveComplexity.HaltHard.unprime {c : Turing.ToPartrec.Code} :

SimSym c → SimSym c

Unmarking a letter.

Equations

Instances For

Dependency graph

theorem DescriptiveComplexity.HaltHard.unprime_prime {c : Turing.ToPartrec.Code} {σ : SimSym c} (h : σ = SimSym.one ∨ σ = SimSym.com) :

unprime (prime σ) = σ

Dependency graph

theorem DescriptiveComplexity.HaltHard.prime_ne {c : Turing.ToPartrec.Code} {σ : SimSym c} (h : σ = SimSym.one ∨ σ = SimSym.com) :

prime σ ≠ SimSym.endL ∧ prime σ ≠ SimSym.mid ∧ prime σ ≠ SimSym.endR

Dependency graph

Fused step-and-walk combinators #

theorem DescriptiveComplexity.HaltHard.reach_step_then_walkL {c : Turing.ToPartrec.Code} {q q₂ : SimQ c} {σ σ' : SimSym c} {P : SimSym c → Prop} (hstep : simStep q σ = some (σ', q₂, false )) (hpass : ∀ (τ : SimSym c), P τ → simStep q₂ τ = some (τ, q₂, false )) (w : List (SimSym c)) (hw : ∀ τ ∈ w, P τ) (x : SimSym c) (L R : List (SimSym c)) :

Reach { q := q, L := w ++ x :: L, s := σ, R := R } { q := q₂, L := L, s := x, R := w.reverse ++ σ' :: R }

One left move, then a leftward walk over passed letters: the fused form every carry uses, sound whether or not the walked span is empty.

Dependency graph

theorem DescriptiveComplexity.HaltHard.reach_step_then_walkR {c : Turing.ToPartrec.Code} {q q₂ : SimQ c} {σ σ' : SimSym c} {P : SimSym c → Prop} (hstep : simStep q σ = some (σ', q₂, true )) (hpass : ∀ (τ : SimSym c), P τ → simStep q₂ τ = some (τ, q₂, true )) (w : List (SimSym c)) (hw : ∀ τ ∈ w, P τ) (x : SimSym c) (L R : List (SimSym c)) :

Reach { q := q, L := L, s := σ, R := w ++ x :: R } { q := q₂, L := w.reverse ++ σ' :: L, s := x, R := R }

One right move, then a rightward walk over passed letters.

Dependency graph

theorem DescriptiveComplexity.HaltHard.reach_step_then_walkR_map {c : Turing.ToPartrec.Code} {q q₂ : SimQ c} {σ σ' : SimSym c} {P : SimSym c → Prop} {f : SimSym c → SimSym c} (hstep : simStep q σ = some (σ', q₂, true )) (hpass : ∀ (τ : SimSym c), P τ → simStep q₂ τ = some (f τ, q₂, true )) (w : List (SimSym c)) (hw : ∀ τ ∈ w, P τ) (x : SimSym c) (L R : List (SimSym c)) :

Reach { q := q, L := L, s := σ, R := w ++ x :: R } { q := q₂, L := (List.map f w).reverse ++ σ' :: L, s := x, R := R }

One right move, then a rightward transducing walk.

Dependency graph

Pass lemmas for the copy #

theorem DescriptiveComplexity.HaltHard.pass_cpCar₁ {c : Turing.ToPartrec.Code} {σ : SimSym c} {p : CPos c} (h : σ ≠ SimSym.endL) :

simStep (SimQ.cpCar₁ p) σ = some (σ, SimQ.cpCar₁ p, false )

Dependency graph

theorem DescriptiveComplexity.HaltHard.pass_cpCarC {c : Turing.ToPartrec.Code} {σ : SimSym c} {p : CPos c} (h : σ ≠ SimSym.endL) :

simStep (SimQ.cpCarC p) σ = some (σ, SimQ.cpCarC p, false )

Dependency graph

theorem DescriptiveComplexity.HaltHard.pass_cpBack {c : Turing.ToPartrec.Code} {σ : SimSym c} {p : CPos c} (h : σ ≠ SimSym.mid) :

simStep (SimQ.cpBack p) σ = some (σ, SimQ.cpBack p, true )

Dependency graph

theorem DescriptiveComplexity.HaltHard.pass_cpHdr {c : Turing.ToPartrec.Code} {σ : SimSym c} {p : CPos c} (h : σ ≠ SimSym.endL) :

simStep (SimQ.cpHdr p) σ = some (σ, SimQ.cpHdr p, false )

Dependency graph

theorem DescriptiveComplexity.HaltHard.pass_cpUnp {c : Turing.ToPartrec.Code} {σ : SimSym c} {p : CPos c} (h : σ ≠ SimSym.mid) :

simStep (SimQ.cpUnp p) σ = some (σ, SimQ.cpUnp p, true )

Dependency graph

theorem DescriptiveComplexity.HaltHard.pass_cpFetch {c : Turing.ToPartrec.Code} {σ : SimSym c} {p : CPos c} (h : σ = SimSym.bk ∨ σ = SimSym.one' ∨ σ = SimSym.com') :

simStep (SimQ.cpFetch p) σ = some (σ, SimQ.cpFetch p, true )

The scan passes blanks and primed letters.

Dependency graph

theorem DescriptiveComplexity.HaltHard.pass_cpUnp₂ {c : Turing.ToPartrec.Code} {σ : SimSym c} {p : CPos c} (h : σ = SimSym.bk ∨ σ = SimSym.one' ∨ σ = SimSym.com') :

simStep (SimQ.cpUnp₂ p) σ = some (unprime σ, SimQ.cpUnp₂ p, true )

The unpriming sweep, as a transducing pass.

Dependency graph

The copy loop #

theorem DescriptiveComplexity.HaltHard.cp_iter {c : Turing.ToPartrec.Code} (p : CPos c) {u : SimSym c} {Qcar : SimQ c} (hu : u = SimSym.one ∨ u = SimSym.com) (h1 : simStep (SimQ.cpFetch p) u = some (prime u, Qcar, false )) (h2 : ∀ (τ : SimSym c), τ ≠ SimSym.endL → simStep Qcar τ = some (τ, Qcar, false )) (h3 : simStep Qcar SimSym.endL = some (u, SimQ.cpEndS p, false )) (P : List (SimSym c)) (hP : ∀ σ ∈ P, σ = SimSym.one ∨ σ = SimSym.com) (g : ℕ) {fr : List (SimSym c)} (hfr : ∀ σ ∈ fr, FrameSym σ) (j : ℕ) (Y : List (SimSym c)) :

Reach { q := SimQ.cpFetch p, L := (List.replicate j SimSym.bk ++ List.map prime P).reverse ++ SimSym.bk :: SimSym.mid :: (fr.reverse ++ (P ++ SimSym.endL :: List.replicate g SimSym.bk)), s := u, R := Y } { q := SimQ.cpFetch p, L := SimSym.mid :: (fr.reverse ++ (P ++ [u] ++ SimSym.endL :: List.replicate (g - 1) SimSym.bk)), s := SimSym.bk, R := List.replicate j SimSym.bk ++ (List.map prime (P ++ [u]) ++ Y) }

One iteration of the copy: with the scan on the next unprimed letter, prime it, carry it home to endL, write it by the endL-shift and walk back onto the gap – the loop entry one letter further. Stated over an abstract carry state so the digit and separator instances share the proof.

Dependency graph

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

theorem DescriptiveComplexity.HaltHard.unprime_map_prime {c : Turing.ToPartrec.Code} {l : List (SimSym c)} (hl : ∀ σ ∈ l, σ = SimSym.one ∨ σ = SimSym.com) :

List.map unprime (List.map prime l) = l

Unpriming undoes priming, letterwise on a value word.

Dependency graph

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 #

theorem DescriptiveComplexity.HaltHard.pStepNormal_zero' {c : Turing.ToPartrec.Code} {p : CPos c} {k : PCont c} {v : List ℕ} (h : codeAt p = Turing.ToPartrec.Code.zero') :

pStepNormal p k v = (k, 0 :: v)

Dependency graph

theorem DescriptiveComplexity.HaltHard.pStepNormal_succ {c : Turing.ToPartrec.Code} {p : CPos c} {k : PCont c} {v : List ℕ} (h : codeAt p = Turing.ToPartrec.Code.succ) :

pStepNormal p k v = (k, [v.headI.succ])

Dependency graph

theorem DescriptiveComplexity.HaltHard.pStepNormal_tail {c : Turing.ToPartrec.Code} {p : CPos c} {k : PCont c} {v : List ℕ} (h : codeAt p = Turing.ToPartrec.Code.tail) :

pStepNormal p k v = (k, v.tail)

Dependency graph

theorem DescriptiveComplexity.HaltHard.pStepNormal_cons {c : Turing.ToPartrec.Code} {p : CPos c} {k : PCont c} {v : List ℕ} {f fs : Turing.ToPartrec.Code} (h : codeAt p = f.cons fs) :

pStepNormal p k v = pStepNormal (c₁ p) (PCont.cons₁ (c₂ p) v k) v

Dependency graph

theorem DescriptiveComplexity.HaltHard.pStepNormal_comp {c : Turing.ToPartrec.Code} {p : CPos c} {k : PCont c} {v : List ℕ} {f g₂ : Turing.ToPartrec.Code} (h : codeAt p = f.comp g₂) :

pStepNormal p k v = pStepNormal (c₂ p) (PCont.comp (c₁ p) k) v

Dependency graph

theorem DescriptiveComplexity.HaltHard.pStepNormal_case_zero {c : Turing.ToPartrec.Code} {p : CPos c} {k : PCont c} {v : List ℕ} {f g₂ : Turing.ToPartrec.Code} (h : codeAt p = f.case g₂) (hv : v.headI = 0) :

pStepNormal p k v = pStepNormal (c₁ p) k v.tail

Dependency graph

theorem DescriptiveComplexity.HaltHard.pStepNormal_case_succ {c : Turing.ToPartrec.Code} {p : CPos c} {k : PCont c} {v : List ℕ} {f g₂ : Turing.ToPartrec.Code} {y : ℕ} (h : codeAt p = f.case g₂) (hv : v.headI = y + 1) :

pStepNormal p k v = pStepNormal (c₂ p) k (y :: v.tail)

Dependency graph

theorem DescriptiveComplexity.HaltHard.pStepNormal_fix {c : Turing.ToPartrec.Code} {p : CPos c} {k : PCont c} {v : List ℕ} {f : Turing.ToPartrec.Code} (h : codeAt p = f.fix) :

pStepNormal p k v = pStepNormal (c₁ p) (PCont.fix (c₁ p) k) v

Dependency graph

The assembled dispatch phase #

theorem DescriptiveComplexity.HaltHard.one_le_sizeOf_code (c' : Turing.ToPartrec.Code) :

1 ≤ sizeOf c'

Every code has size at least one.

Dependency graph

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