The simulating machine on a zipper tape

The simulation of Turing.ToPartrec.step by DescriptiveComplexity.HaltHard.simStep is proved against a concrete sequential semantics first: a configuration is a zipper (DescriptiveComplexity.HaltHard.LCfg) – the state, the letters left of the head (nearest first), the letter under the head, and the letters right of the head (nearest first) – and one step (DescriptiveComplexity.HaltHard.lstep) applies the table and moves, materialising a blank when the head leaves the recorded region. This keeps every walk argument a plain list induction; the sibling Bridge file identifies runs of lstep with derivations of the rewriting system DescriptiveComplexity.HaltPcp.MRule of the drawn machine, so nothing here mentions words or rules.

Beside the step and its reachability (DescriptiveComplexity.HaltHard.Reach, and the step-counted DescriptiveComplexity.HaltHard.stepsTo the deterministic backward reading needs), the file provides the two walk combinators: a state that passes a set of letters unchanged in one direction crosses any run of them (DescriptiveComplexity.HaltHard.reach_walkR/reach_walkL). Every phase of the simulation is a chain of these.

structure DescriptiveComplexity.HaltHard.LCfg (c : Turing.ToPartrec.Code) : Type

A configuration of the simulating machine, as a zipper: the letters left of the head are listed nearest-first, the letters right of the head nearest-first. Cells outside the recorded region are blank; a move beyond it materialises the blank.

• q : SimQ c

  The current state.

• L : List (SimSym c)

  The letters left of the head, nearest first.

• s : SimSym c

  The letter under the head.

• R : List (SimSym c)

  The letters right of the head, nearest first.

def DescriptiveComplexity.HaltHard.lstep {c : Turing.ToPartrec.Code} (x : LCfg c) : Option (LCfg c)

One step of the machine on the zipper tape: apply the table, write, move; a move beyond the recorded region reads a fresh blank.

Equations

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

def DescriptiveComplexity.HaltHard.Reach {c : Turing.ToPartrec.Code} : LCfg c → LCfg c → Prop

Reachability in any number of machine steps.

Equations

• DescriptiveComplexity.HaltHard.Reach = Relation.ReflTransGen fun (x y : DescriptiveComplexity.HaltHard.LCfg c) => DescriptiveComplexity.HaltHard.lstep x = some y

def DescriptiveComplexity.HaltHard.stepsTo {c : Turing.ToPartrec.Code} : ℕ → LCfg c → LCfg c → Prop

Reaching one configuration from another in exactly n steps.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HaltHard.stepsTo 0 x✝¹ x✝ = (x✝¹ = x✝)

The four single steps

theorem DescriptiveComplexity.HaltHard.lstep_right {c : Turing.ToPartrec.Code} {q q' : SimQ c} {σ σ' : SimSym c} (h : simStep q σ = some (σ', q', true)) (L : List (SimSym c)) (t : SimSym c) (R : List (SimSym c)) : lstep { q := q, L := L, s := σ, R := t :: R } = some { q := q', L := σ' :: L, s := t, R := R }

A right move with a recorded cell to enter.

theorem DescriptiveComplexity.HaltHard.lstep_right_end {c : Turing.ToPartrec.Code} {q q' : SimQ c} {σ σ' : SimSym c} (h : simStep q σ = some (σ', q', true)) (L : List (SimSym c)) : lstep { q := q, L := L, s := σ, R := [] } = some { q := q', L := σ' :: L, s := SimSym.bk, R := [] }

A right move off the recorded region: the entered cell is blank.

theorem DescriptiveComplexity.HaltHard.lstep_left {c : Turing.ToPartrec.Code} {q q' : SimQ c} {σ σ' : SimSym c} (h : simStep q σ = some (σ', q', false)) (t : SimSym c) (L R : List (SimSym c)) : lstep { q := q, L := t :: L, s := σ, R := R } = some { q := q', L := L, s := t, R := σ' :: R }

A left move with a recorded cell to enter.

theorem DescriptiveComplexity.HaltHard.lstep_left_end {c : Turing.ToPartrec.Code} {q q' : SimQ c} {σ σ' : SimSym c} (h : simStep q σ = some (σ', q', false)) (R : List (SimSym c)) : lstep { q := q, L := [], s := σ, R := R } = some { q := q', L := [], s := SimSym.bk, R := σ' :: R }

A left move off the recorded region: the entered cell is blank.

theorem DescriptiveComplexity.HaltHard.lstep_right_pad {c : Turing.ToPartrec.Code} {q q' : SimQ c} {σ σ' : SimSym c} (h : simStep q σ = some (σ', q', true)) (L : List (SimSym c)) (t : ℕ) : lstep { q := q, L := L, s := σ, R := List.replicate t SimSym.bk } = some { q := q', L := σ' :: L, s := SimSym.bk, R := List.replicate (t - 1) SimSym.bk }

A right move into a run of blanks – recorded or materialised, the entered cell is blank either way.

theorem DescriptiveComplexity.HaltHard.lstep_left_pad {c : Turing.ToPartrec.Code} {q q' : SimQ c} {σ σ' : SimSym c} (h : simStep q σ = some (σ', q', false)) (g : ℕ) (R : List (SimSym c)) : lstep { q := q, L := List.replicate g SimSym.bk, s := σ, R := R } = some { q := q', L := List.replicate (g - 1) SimSym.bk, s := SimSym.bk, R := σ' :: R }

A left move into a run of blanks – recorded or materialised, the entered cell is blank either way.

Reachability

theorem DescriptiveComplexity.HaltHard.Reach.refl {c : Turing.ToPartrec.Code} (x : LCfg c) : Reach x x

theorem DescriptiveComplexity.HaltHard.Reach.single {c : Turing.ToPartrec.Code} {x y : LCfg c} (h : lstep x = some y) : Reach x y

theorem DescriptiveComplexity.HaltHard.Reach.head {c : Turing.ToPartrec.Code} {x y z : LCfg c} (h : lstep x = some y) (hr : Reach y z) : Reach x z

theorem DescriptiveComplexity.HaltHard.Reach.trans {c : Turing.ToPartrec.Code} {x y z : LCfg c} (h : Reach x y) (h' : Reach y z) : Reach x z

Counted steps, and determinism

theorem DescriptiveComplexity.HaltHard.stepsTo.trans_step {c : Turing.ToPartrec.Code} {n : ℕ} {x y z : LCfg c} : stepsTo n x y → lstep y = some z → stepsTo (n + 1) x z

A counted run, extended by one step at its end.

theorem DescriptiveComplexity.HaltHard.stepsTo.trans {c : Turing.ToPartrec.Code} {n m : ℕ} {x y z : LCfg c} : stepsTo n x y → stepsTo m y z → stepsTo (n + m) x z

Counted runs compose.

theorem DescriptiveComplexity.HaltHard.reach_iff_stepsTo {c : Turing.ToPartrec.Code} {x y : LCfg c} : Reach x y ↔ ∃ (n : ℕ), stepsTo n x y

Reachability is a counted run of some length.

theorem DescriptiveComplexity.HaltHard.stepsTo_det {c : Turing.ToPartrec.Code} {m n : ℕ} {x y z : LCfg c} : stepsTo m x y → stepsTo n x z → m ≤ n → stepsTo (n - m) y z

The machine is deterministic: a counted run to anywhere follows the run to a terminal configuration, step for step.

theorem DescriptiveComplexity.HaltHard.le_of_stepsTo_terminal {c : Turing.ToPartrec.Code} {n m : ℕ} {x y z : LCfg c} : stepsTo n x y → lstep y = none → stepsTo m x z → m ≤ n

A run cannot leave a terminal configuration, so it is at least as long as any run from the same start.

The walk combinators

A state that passes a set of letters unchanged in one direction crosses any run of them. The head starts on the first letter of the run and ends on the first letter beyond it; the crossed letters pile up behind the head in reverse.

theorem DescriptiveComplexity.HaltHard.reach_walkR_map {c : Turing.ToPartrec.Code} {q : SimQ c} {P : SimSym c → Prop} {f : SimSym c → SimSym c} (hq : ∀ (σ : SimSym c), P σ → simStep q σ = some (f σ, q, true)) (w : List (SimSym c)) : (∀ σ ∈ w, P σ) → ∀ {s : SimSym c}, P s → ∀ (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 := (List.map f w).reverse ++ f s :: L, s := t, R := R }

Walking right over a run of passed letters, rewriting each by f – the transducing form: erasure sweeps take f := fun _ => .bk, unpriming takes the unpriming map.

theorem DescriptiveComplexity.HaltHard.reach_walkL_map {c : Turing.ToPartrec.Code} {q : SimQ c} {P : SimSym c → Prop} {f : SimSym c → SimSym c} (hq : ∀ (σ : SimSym c), P σ → simStep q σ = some (f σ, q, false)) (w : List (SimSym c)) : (∀ σ ∈ w, P σ) → ∀ {s : SimSym c}, P s → ∀ (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 ++ f s :: R }

Walking left over a run of passed letters, rewriting each by f.

theorem DescriptiveComplexity.HaltHard.reach_walkR {c : Turing.ToPartrec.Code} {q : SimQ c} {P : SimSym c → Prop} (hq : ∀ (σ : SimSym c), P σ → simStep q σ = some (σ, q, true)) (w : List (SimSym c)) : (∀ σ ∈ w, P σ) → ∀ {s : SimSym c}, P s → ∀ (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 ++ s :: L, s := t, R := R }

Walking right over a run of passed letters, unchanged.

theorem DescriptiveComplexity.HaltHard.reach_walkL {c : Turing.ToPartrec.Code} {q : SimQ c} {P : SimSym c → Prop} (hq : ∀ (σ : SimSym c), P σ → simStep q σ = some (σ, q, false)) (w : List (SimSym c)) : (∀ σ ∈ w, P σ) → ∀ {s : SimSym c}, P s → ∀ (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 ++ s :: R }

Walking left over a run of passed letters, unchanged.