Bounds on the number of reachable configurations in bounded space

A multi-tape Turing machine that uses at most s cells of work-tape space can only reach a number of configurations that differ in their storage content (state and work tapes) that is bounded exponentially in s. Together with the n + 2 possible positions of the input head this bounds the number of configurations the machine can be in, disregarding the write-only output tape.

Important Definitions

The results are layered, from the purely combinatorial to the machine-specific:

• MultiTapeTM.encard_fitsIn_le is a counting statement about the type Storage alone and does not mention Turing machines: a memory whose non-blank cells and heads stay within per-tape windows of total size s can hold at most storageBound Symbol State k s different values.
• MultiTapeTM.storage_fitsIn is the geometric input: the storage reached after t steps stays within the windows given by the space used up to step t.
• MultiTapeTM.encard_storages_le combines the two: a machine bounded by space s passes through at most storageBound Symbol State k s storages during its whole run, no matter how long it runs and how long its input is. This is the form needed for arguments below logarithmic space, where the number of storages is much smaller than the number of input head positions.
• MultiTapeTM.encard_cores_le adds the input head position, giving the bound (n + 2) * storageBound Symbol State k s on the number of reachable cores (Cfg.core, a configuration without its output tape) for an input of length n.
• MultiTapeTM.storageBound_le_base_mul_pow restates storageBound Symbol State k s as storageBoundBase Symbol State k * 2 ^ (storageBoundExp Symbol k * s), so that the bounds can be used to time-bound space-bounded machines.

Design

The write-only output tape is never read by step, so it can be dropped: what a machine can still react to is its Cfg.core, the pair of the input head position and the Storage. The input head position, in contrast, is read, so it cannot be dropped and has to be counted, which is where the factor n + 2 comes from (the input head may move one step off the input in either direction).

Starting from the all-blank tapes with every head at 0 and moving by at most one cell per step, a computation in which tape i has visited at most sᵢ cells keeps that tape's head position and every non-blank cell within the per-tape window [-sᵢ, sᵢ].

Hence a storage is determined by finite data over these windows, and counting it gives the per-tape product ∏ᵢ (2 sᵢ + 1) · (|Symbol| + 1)^(2 sᵢ + 1). Since the tapes share the total space budget (∑ᵢ sᵢ ≤ s), this collapses to an expression with the total space (2s + k) as the alphabet exponent.

We lose a factor of 2 * k by simplifying the windows to [-sᵢ, sᵢ] instead of the actually used area, but this is absorbed by the O(s) exponent in the final bound.

The windows for a whole run are available because a machine that is space-bounded at every point in time attains its per-tape space usage at a single step (MultiTapeTM.exists_spaceUsedByTape_max).

Storage

Defines the core data structure for this file, Storage, which contains the state and the work tapes of a multi-tape Turing machine, with the work tape cells indexed over all of ℤ. It is thus equivalent to a projection of Cfg.

Then BoundedStorage is introduced, which restricts the cells and the head position of each tape to a window [-s, s] (with a different s for each tape) and is therefore a finite type. It is proven that the restriction map is injective on those Storages whose non-blank cells and head positions all lie inside the [-s, s] windows, so that counting BoundedStorage bounds the number of such Storages.

structure Turing.Storage (Symbol : Type u_3) (State : Type u_4) (k : ℕ) : Type (max u_3 u_4)

The state and work-tape data of a machine.

• state : Option State

  the state of the TM (cf. Cfg.state)

• workTapes (i : Fin k) : ℤ → Option Symbol

  the contents of work tape i (cf. Cfg.workTapes)

• workTapePos (i : Fin k) : ℤ

  the position of the head on work tape i (cf. Cfg.workTapePos)

theorem Turing.Storage.ext_iff {Symbol : Type u_3} {State : Type u_4} {k : ℕ} {x y : Storage Symbol State k} : x = y ↔ x.state = y.state ∧ x.workTapes = y.workTapes ∧ x.workTapePos = y.workTapePos

theorem Turing.Storage.ext {Symbol : Type u_3} {State : Type u_4} {k : ℕ} {x y : Storage Symbol State k} (state : x.state = y.state) (workTapes : x.workTapes = y.workTapes) (workTapePos : x.workTapePos = y.workTapePos) : x = y

def Turing.window (s : ℕ) : Finset ℤ

The window [-s, s] of tape positions allotted to a tape that uses s cells.

Equations

• Turing.window s = Finset.Icc (-↑s) ↑s

theorem Turing.mem_window {s : ℕ} {z : ℤ} : z ∈ window s ↔ z.natAbs ≤ s

@[simp]

theorem Turing.card_window (s : ℕ) : (window s).card = 2 * s + 1

@[reducible, inline]

abbrev Turing.BoundedStorage (Symbol : Type u_3) (State : Type u_4) {k : ℕ} (w : Fin k → ℕ) : Type (max u_4 u_3)

A bounded storage: the state and work-tape data of a machine, but with the cells and the head position of tape i restricted to the finite window [-(w i), w i].

Equations

• Turing.BoundedStorage Symbol State w = (Option State × ((i : Fin k) → ↥(Turing.window (w i)) → Option Symbol) × ((i : Fin k) → ↥(Turing.window (w i))))

structure Turing.Storage.FitsIn {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (x : Storage Symbol State k) (w : Fin k → ℕ) : Prop

A storage fits in the per-tape windows w: on each tape j, the head position and every non-blank cell have absolute value ≤ w j.

• pos_le (j : Fin k) : (x.workTapePos j).natAbs ≤ w j

  the head position on every tape lies within its window

• cell_le (j : Fin k) (z : ℤ) : x.workTapes j z ≠ none → z.natAbs ≤ w j

  every non-blank cell on every tape lies within its window

theorem Turing.Storage.FitsIn_mono {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {x : Storage Symbol State k} : Monotone x.FitsIn

If a Storage fits in a smaller window, it also fits in the larger window.

def Turing.Storage.toBounded {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (x : Storage Symbol State k) (w : Fin k → ℕ) : BoundedStorage Symbol State w

Restriction of a storage to the finite windows w (with heads outside their window clamped to 0).

Equations

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

theorem Turing.Storage.toBounded_injOn {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (w : Fin k → ℕ) : Set.InjOn (fun (x : Storage Symbol State k) => x.toBounded w) {x : Storage Symbol State k | x.FitsIn w}

The restriction is injective on storages that fit in the windows.

Counting storages

This section is purely combinatorial: it counts how many values a Storage restricted to given windows can take, without reference to a machine or a run.

def Turing.storageBound (Symbol : Type u_3) (State : Type u_4) [Fintype Symbol] [Fintype State] (k s : ℕ) : ℕ

An upper bound on the number of storages a k-tape machine can be in while using at most s cells of total work-tape space, over the given alphabet and state set. The (2s + 1)^k factor counts the possible head positions; the dominant factor (|Symbol| + 1)^(2s + k) uses the total space s in the exponent (the k tapes share the space budget).

Equations

• Turing.storageBound Symbol State k s = (Fintype.card State + 1) * ((2 * s + 1) ^ k * (Fintype.card Symbol + 1) ^ (2 * s + k))

theorem Turing.card_boundedStorage_le {k : ℕ} {State : Type u_1} {Symbol : Type u_2} [Fintype Symbol] [Fintype State] {w : Fin k → ℕ} {s : ℕ} (hsum : ∑ i : Fin k, w i ≤ s) : Fintype.card (BoundedStorage Symbol State w) ≤ storageBound Symbol State k s

The number of bounded storages is at most storageBound. Counting the tapes separately gives the per-tape product ∏ᵢ (2 wᵢ + 1) · (|Symbol| + 1) ^ (2 wᵢ + 1); each tape uses at most the total space s, and the tapes together use at most s, which collapses the alphabet exponent to 2s + k.

theorem Turing.encard_fitsIn_le {k : ℕ} {State : Type u_1} {Symbol : Type u_2} [Fintype Symbol] [Fintype State] {w : Fin k → ℕ} {s : ℕ} (hsum : ∑ i : Fin k, w i ≤ s) : {x : Storage Symbol State k | x.FitsIn w}.encard ≤ ↑(storageBound Symbol State k s)

The counting result at the heart of this file: a Storage whose non-blank cells and head positions stay within per-tape windows of total size at most s can take at most storageBound Symbol State k s different values.

The exponential form of storageBound

This proves that storageBound is exponential in the space s.

def Turing.storageBoundBase (Symbol : Type u_3) (State : Type u_4) [Fintype Symbol] [Fintype State] (k : ℕ) : ℕ

The base factor in the resulting exponential form of storageBound.

Equations

• Turing.storageBoundBase Symbol State k = (Fintype.card State + 1) * 2 ^ ((Fintype.card Symbol + 1) * k + k)

def Turing.storageBoundExp (Symbol : Type u_3) [Fintype Symbol] (k : ℕ) : ℕ

The factor in the exponent of the exponential form of storageBound.

Equations

• Turing.storageBoundExp Symbol k = 2 * (Fintype.card Symbol + 1) + k

theorem Turing.storageBound_le_base_mul_pow {k : ℕ} {State : Type u_1} {Symbol : Type u_2} [Fintype Symbol] [Fintype State] (s : ℕ) : storageBound Symbol State k s ≤ storageBoundBase Symbol State k * 2 ^ (storageBoundExp Symbol k * s)

storageBound grows at most exponentially in the space s, with a constant factor and a factor in the exponent that only depend on the machine's alphabet, state set and tape count.

theorem Turing.storageBound_le_pow {k : ℕ} {State : Type u_1} {Symbol : Type u_2} [Fintype Symbol] [Fintype State] : ∃ (a : ℕ) (c : ℕ), ∀ (s : ℕ), storageBound Symbol State k s ≤ a * 2 ^ (c * s)

storageBound grows at most exponentially in the space s: there exist constants a and c (depending on the machine's alphabet, state set and tape count) with storageBound Symbol State k s ≤ a * 2 ^ (c * s) for all s.

The storage and the core of a configuration

Now we relate Cfg and Storage by giving the projection.

def Turing.Cfg.storage {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (c : Cfg k Symbol State input) : Storage Symbol State k

This function maps a Cfg to Storage, forgetting the input head position and the write-only output tape.

Equations

• c.storage = { state := c.state, workTapes := c.workTapes, workTapePos := c.workTapePos }

def Turing.Cfg.core {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (c : Cfg k Symbol State input) : Fin (input.length + 2) × Storage Symbol State k

The part of a configuration that the machine can still read: the input head position together with the Storage, i.e. the configuration without the write-only output tape.

Equations

• c.core = (c.inputPos, c.storage)

theorem Turing.core_step_eq_of_core_eq {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} {c₁ c₂ : Cfg k Symbol State input} (h : c₁.core = c₂.core) : (MultiTapeTM.step c₁).core = (MultiTapeTM.step c₂).core

step never reads the output tape, so the core of the next configuration is determined by the core of the current one.

The storages and cores of a space-bounded run

These are the main results giving upper bounds on the number of storages and configuration cores reachable in bounded space.

theorem Turing.MultiTapeTM.storage_fitsIn {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} (t : ℕ) : (runFrom (initCfg input) t).storage.FitsIn (spaceUsedByTape (initCfg input) t)

The storage reached after t steps fits in the windows given by the per-tape space usage up to step t.

theorem Turing.MultiTapeTM.encard_storages_le {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} [Fintype Symbol] [Fintype State] {s : ℕ} (hs : ∀ (t : ℕ), spaceUsed (initCfg input) t ≤ s) : (Set.range fun (t : ℕ) => (runFrom (initCfg input) t).storage).encard ≤ ↑(storageBound Symbol State k s)

A machine that uses at most s cells of work-tape space at every point in time passes through at most storageBound Symbol State k s different storages during its whole run — independently of the length of the input and of how long it runs.

theorem Turing.MultiTapeTM.encard_cores_le {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} [Fintype Symbol] [Fintype State] {s : ℕ} (hs : ∀ (t : ℕ), spaceUsed (initCfg input) t ≤ s) : (Set.range fun (t : ℕ) => (runFrom (initCfg input) t).core).encard ≤ (↑input.length + 2) * ↑(storageBound Symbol State k s)

The number of configuration cores that a machine bounded by space s can reach is at most (n + 2) * storageBound Symbol State k s, where n is the length of the input.

theorem Turing.MultiTapeTM.encard_storages_le_pow {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} [Finite Symbol] [Finite State] : ∃ (a : ℕ) (c : ℕ), ∀ (input : List Symbol) (s : ℕ), (∀ (t : ℕ), spaceUsed (initCfg input) t ≤ s) → (Set.range fun (t : ℕ) => (runFrom (initCfg input) t).storage).encard ≤ ↑a * 2 ^ (c * s)

The storage bound in exponential form: the number of storages a space-s-bounded machine passes through is at most 2 ^ (O(s)), with constants depending only on the machine.

theorem Turing.MultiTapeTM.encard_cores_le_pow {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} [Finite Symbol] [Finite State] : ∃ (a : ℕ) (c : ℕ), ∀ (input : List Symbol) (s : ℕ), (∀ (t : ℕ), spaceUsed (initCfg input) t ≤ s) → (Set.range fun (t : ℕ) => (runFrom (initCfg input) t).core).encard ≤ (↑input.length + 2) * ↑a * 2 ^ (c * s)

The core bound in exponential form: the number of cores a space-s-bounded machine can reach is at most (n + 2) * 2 ^ (O(s)), with constants depending only on the machine and not on the input.