Finite observations of space-bounded transducer configurations

This file defines the finite snapshots used to turn an auxiliary-space bound for a deterministic transducer into a time bound. A work tape whose head stays within space is observed only through that bounded head position and the cells through space. The input is read-only, so its head position suffices. For the one-way output tape, only whether the head is at the left marker and the symbol currently under the head can affect future execution.

Main definitions

• Tape.BoundedObs — the finite observable part of a space-bounded tape
• Tape.boundedObs — observe a tape whose head satisfies the space bound
• TM.TransducerSnapshot — the finite observable part of a transducer configuration
• TM.transducerSnapshot — observe a configuration within auxiliary space
• TM.transducerConfigBound — the number of possible transducer snapshots

@[simp]

theorem Complexity.Γ.card : Fintype.card Γ = 4

The fixed tape alphabet has four symbols.

@[reducible, inline]

abbrev Complexity.Tape.BoundedObs (space : ℕ) : Type

The observable part of a tape whose head never travels beyond space. It records the bounded head position and every cell the head can visit.

Equations

• Complexity.Tape.BoundedObs space = (Fin (space + 1) × (Fin (space + 1) → Complexity.Γ))

def Complexity.Tape.boundedObs (t : Tape) (space : ℕ) (h : t.head ≤ space) : BoundedObs space

Restrict a tape to the cells visible under a given head-space bound.

Equations

• t.boundedObs space h = (⟨t.head, ⋯⟩, fun (i : Fin (space + 1)) => t.cells ↑i)

theorem Complexity.Tape.card_boundedObs (space : ℕ) : Fintype.card (BoundedObs space) = (space + 1) * 4 ^ (space + 1)

The exact number of bounded observations of one work tape.

@[reducible, inline]

abbrev Complexity.TM.TransducerSnapshot {k : ℕ} (tm : TM k) (inputLength space : ℕ) : Type

The finite observable part of a space-bounded transducer configuration.

The output position and written prefix are deliberately absent: for a one-way output tape, future execution can inspect only whether the head is still on the exceptional left-marker cell and the symbol under its current head.

Equations

• tm.TransducerSnapshot inputLength space = (tm.Q × Fin (inputLength + space + 2) × (Fin k → Complexity.Tape.BoundedObs space) × Bool × Complexity.Γ)

def Complexity.TM.transducerSnapshot {k : ℕ} (tm : TM k) (c : Cfg k tm.Q) (inputLength space : ℕ) (hspace : c.WithinAuxSpace inputLength space) : tm.TransducerSnapshot inputLength space

Observe the finite part of a configuration satisfying an auxiliary-space bound. The output-head zero flag distinguishes the immutable left-marker cell from ordinary output cells.

Equations

• tm.transducerSnapshot c inputLength space hspace = (c.state, ⟨c.input.head, ⋯⟩, fun (i : Fin k) => (c.work i).boundedObs space ⋯, decide (c.output.head = 0), c.output.read)

def Complexity.TM.transducerConfigBound {k : ℕ} (tm : TM k) (inputLength space : ℕ) : ℕ

A concrete upper bound on the number of finite snapshots of a k-work-tape transducer using auxiliary space space on inputs of length inputLength.

Equations

• tm.transducerConfigBound inputLength space = 8 * Fintype.card tm.Q * (inputLength + space + 2) * ((space + 1) * 4 ^ (space + 1)) ^ k

theorem Complexity.TM.card_transducerSnapshot {k : ℕ} (tm : TM k) (inputLength space : ℕ) : Fintype.card (tm.TransducerSnapshot inputLength space) = tm.transducerConfigBound inputLength space

transducerConfigBound is the exact cardinality of the snapshot type.