Counting the configurations inside a space bound

⚠️ Unreviewed by Bolton

Cfg.WithinDecisionSpace bounds head positions, but counting configurations also needs to know the tape contents are pinned down. A head that never leaves its window can never write outside it, so every cell beyond still holds what it started with — that is Windowed, and it is what makes the configuration space finite.

Nothing here mentions a machine: the counting is the same for deterministic and nondeterministic configurations, and both PSPACE ⊆ EXP and the log-space graph arguments use it.

Main definitions

• Windowed — the tapes agree with their initial contents outside the window
• cfgCode — a total code for configurations, injective inside the space bound
• instDecidableEqCode — codes have decidable equality

Main results

• Windowed.mono, Cfg.WithinDecisionSpace.mono — enlarging the window is harmless
• cfgCode_inj — two windowed configurations inside the bound with the same code are equal
• card_Code — the number of codes
• card_Code_le_two_pow — the count is at most 2 to a linear-in-S exponent

structure Complexity.Windowed {k : ℕ} {Q : Type} (x : List Bool) (S : ℕ) (c : Cfg k Q) : Prop

Outside the space window every tape still holds what it started with: the input tape is read-only, and the work and output tapes are blank beyond the reach of their heads.

• input : c.input.cells = (Tape.init (List.map Γ.ofBool x)).cells

  The input tape is never written.

• work (i : Fin k) (p : ℕ) : S < p → (c.work i).cells p = Γ.blank

  Work cells beyond the window are blank.

• output (p : ℕ) : S + 1 < p → c.output.cells p = Γ.blank

  Output cells beyond the window are blank.

theorem Complexity.windowed_init {k : ℕ} {Q : Type} (q : Q) (x : List Bool) (S : ℕ) : Windowed x S (Cfg.init q x)

The initial configuration is windowed.

theorem Complexity.Windowed.mono {k : ℕ} {Q : Type} {x : List Bool} {S S' : ℕ} {c : Cfg k Q} (h : Windowed x S c) (hS : S ≤ S') : Windowed x S' c

Enlarging the window preserves the invariant: what is blank beyond S is blank beyond any larger S' too.

theorem Complexity.Cfg.WithinDecisionSpace.mono {k : ℕ} {Q : Type} {n S S' : ℕ} {c : Cfg k Q} (h : c.WithinDecisionSpace n S) (hS : S ≤ S') : c.WithinDecisionSpace n S'

Enlarging the space budget preserves a decision-space bound.

theorem Complexity.cells_writeAndMove_of_ne (t : Tape) (s : Γ) (d : Dir3) {p : ℕ} (hp : p ≠ t.head) : (t.writeAndMove s d).cells p = t.cells p

Writing at the head leaves every other cell alone.

@[reducible, inline]

abbrev Complexity.Code (Q : Type) (k nn S : ℕ) : Type

A finite code for configurations inside the space window: the state, the three head positions clamped into range, and the tape contents restricted to the window.

Equations

• Complexity.Code Q k nn S = (Q × Fin (nn + S + 2) × (Fin k → Fin (S + 1) × (Fin (S + 1) → Complexity.Γ)) × Fin (S + 2) × (Fin (S + 2) → Complexity.Γ))

@[instance_reducible]

instance Complexity.instDecidableEqCode (Q : Type) [DecidableEq Q] (k nn S : ℕ) : DecidableEq (Code Q k nn S)

Codes have decidable equality: the search of Complexitylib.Classes.Containments.Internal.CodeSearch stores them in a Finset. The instance is spelled out because the default synthesis size limit stops short of this nesting depth.

Equations

• Complexity.instDecidableEqCode Q k nn S = inferInstance

def Complexity.cfgCode {k : ℕ} {Q : Type} (nn S : ℕ) (c : Cfg k Q) : Code Q k nn S

The code of a configuration. Clamping keeps this total; on configurations that respect the space bound the clamps are inert.

Equations

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

theorem Complexity.cfgCode_inj {k : ℕ} {Q : Type} {x : List Bool} {S : ℕ} {c₁ c₂ : Cfg k Q} (h₁ : Windowed x S c₁) (hs₁ : c₁.WithinDecisionSpace x.length S) (h₂ : Windowed x S c₂) (hs₂ : c₂.WithinDecisionSpace x.length S) (h : cfgCode x.length S c₁ = cfgCode x.length S c₂) : c₁ = c₂

Two windowed configurations inside the space bound with the same code are equal.

theorem Complexity.card_Code (Q : Type) [Fintype Q] (k nn S : ℕ) : Fintype.card (Code Q k nn S) = Fintype.card Q * ((nn + S + 2) * (((S + 1) * 4 ^ (S + 1)) ^ k * ((S + 2) * 4 ^ (S + 2))))

The number of codes.

theorem Complexity.card_Code_le_two_pow (Q : Type) [Fintype Q] (k nn S : ℕ) : Fintype.card (Code Q k nn S) ≤ 2 ^ (Fintype.card Q + (nn + S + 2) + 3 * k * (S + 1) + 3 * (S + 2))

The configuration count is at most exponential in the space bound. Both PSPACE ⊆ EXP and Savitch's theorem read the count this way: as 2 to something linear in the space bound.