What the encoded step does to a reachable configuration

⚠️ Unreviewed by Bolton

Cobham.stepFn tracks a machine's step only on configurations that respect the encoding's window: every head inside it, every tape carrying its left-end marker. This file collects those side conditions into Complexity.CodeInv, shows that every configuration of a space-bounded machine's configuration graph satisfies it, and reads off what Complexity.nstepFn computes there.

Main definitions

• Complexity.CodeInv — the encoding's side conditions on a configuration

Main results

• Complexity.cfgCode_length — a code is exactly 2(k+2)+1 blocks wide
• Complexity.nstepFn_code, Complexity.nstepFn_code_halted — the encoded successor is the code of the successor
• Complexity.codeInv_of_reachesCfg — the graph stays inside the window

The width of a code

def Complexity.codeBlocks (k : ℕ) : ℕ

The number of blocks in a code: one for the state and two per tape.

Equations

• Complexity.codeBlocks k = 2 * (k + 2) + 1

@[simp]

theorem Complexity.cfgCode_length {k : ℕ} {Q : Type} [Fintype Q] [DecidableEq Q] (W : ℕ) (c : Cfg k Q) : (Cobham.cfgCode W c).length = codeBlocks k * (Cobham.blockRuler W).length

A code is exactly 2(k+2)+1 blocks wide.

theorem Complexity.fitCode_cfgCode {k : ℕ} {Q : Type} [Fintype Q] [DecidableEq Q] (W : ℕ) (c : Cfg k Q) : fitCode (codeBlocks k) (Cobham.blockRuler W) (Cobham.cfgCode W c) = Cobham.cfgCode W c

A code is unchanged by the width normalisation.

The window conditions

structure Complexity.CodeInv {k : ℕ} {Q : Type} (W : ℕ) (c : Cfg k Q) : Prop

The side conditions under which the encoded step tracks the real one.

• start (t : Tape) : t ∈ Cobham.cfgTapes c → t.StartInvariant

  Every tape carries its left-end marker.

• head (t : Tape) : t ∈ Cobham.cfgTapes c → t.head ≤ W

  Every head is inside the encoded window.

theorem Complexity.nstepFn_code {k : ℕ} (tm : NTM k) (b : Bool) (W : ℕ) (c : Cfg k tm.Q) (hq : Fintype.card tm.Q ≤ Cobham.blockWidth W) (hinv : CodeInv W c) (hne : c.state ≠ tm.qhalt) : nstepFn tm b (Cobham.blockRuler W) (Cobham.cfgCode W c) = Cobham.cfgCode W (tm.stepCfg b c)

The encoded successor is the code of the successor.

theorem Complexity.nstepFn_code_halted {k : ℕ} (tm : NTM k) (b : Bool) (W : ℕ) (c : Cfg k tm.Q) (hq : Fintype.card tm.Q ≤ Cobham.blockWidth W) (hinv : CodeInv W c) (hhalt : c.state = tm.qhalt) : nstepFn tm b (Cobham.blockRuler W) (Cobham.cfgCode W c) = Cobham.cfgCode W c

A halted configuration is a fixed point of the encoded step.

The graph stays inside the window

theorem Complexity.startInvariant_of_reachesCfg {k : ℕ} (tm : NTM k) (x : List Bool) {c : Cfg k tm.Q} (h : tm.ReachesCfg (tm.initCfg x) c) : c.input.StartInvariant ∧ (∀ (i : Fin k), (c.work i).StartInvariant) ∧ c.output.StartInvariant

Every configuration of the graph carries its left-end markers.

theorem Complexity.codeInv_of_reachesCfg {k : ℕ} (tm : NTM k) {L : Language} {S : ℕ → ℕ} (hdec : tm.DecidesInSpace L S) (x : List Bool) {c : Cfg k tm.Q} (h : tm.ReachesCfg (tm.initCfg x) c) (W : ℕ) (hW : x.length + S x.length + 1 ≤ W) : CodeInv W c

The graph stays inside the encoded window.