inductive SpaceComplexity.LadderTapeSymbol (α : Type) : Type

Tape alphabet used by the linear-space NTM deciding LADDER_DFA. It consists of the input symbols of the DFA (ofAlpha), a separator used to encode the pair ⟨u, v⟩, and a blank symbol.

• ofAlpha {α : Type} : α → LadderTapeSymbol α
• separator {α : Type} : LadderTapeSymbol α
• blank {α : Type} : LadderTapeSymbol α

@[implicit_reducible]

instance SpaceComplexity.instDecidableEqLadderTapeSymbol {α✝ : Type} [DecidableEq α✝] : DecidableEq (LadderTapeSymbol α✝)

def SpaceComplexity.instDecidableEqLadderTapeSymbol.decEq {α✝ : Type} [DecidableEq α✝] (x✝ x✝¹ : LadderTapeSymbol α✝) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance SpaceComplexity.instInhabitedLadderTapeSymbol {α : Type} : Inhabited (LadderTapeSymbol α)

The default tape symbol is blank.

def SpaceComplexity.encodePair {α : Type} (u v : List α) : List (LadderTapeSymbol α)

Encoding of a pair of strings (u, v) on the tape as u ++ [separator] ++ v, where each symbol of u and v is lifted via ofAlpha.

def SpaceComplexity.LADDER_DFA_Lang {α σ : Type} [Fintype σ] [Fintype α] (B : DFA α σ) : Set (List (LadderTapeSymbol α))

The on-tape language version of LADDER_DFA: tape words w that encode some pair (u, v) of strings such that there is a ladder y₁, …, y_k ∈ L(B) of common-length strings (consecutive ones differing in a single symbol) with y₁ = u and y_k = v.

inductive SpaceComplexity.LadderPhase : Type

The phases of the linear-space NTM that decides LADDER_DFA.

• readInput: reading and buffering the input pair ⟨u, v⟩ from the tape.
• searchFwd: nondeterministically guessing the next rung of the ladder.
• searchBack: moving the head back to the working area between rungs.
• accepted / rejected: terminal states.

• readInput : LadderPhase
• searchFwd : LadderPhase
• searchBack : LadderPhase
• accepted : LadderPhase
• rejected : LadderPhase

@[implicit_reducible]

instance SpaceComplexity.instDecidableEqLadderPhase : DecidableEq LadderPhase

@[implicit_reducible]

instance SpaceComplexity.instFintypeLadderPhase : Fintype LadderPhase

structure SpaceComplexity.LadderState (α : Type) : Type

Internal control state of the LADDER_DFA NTM.

• phase is the current phase.
• buf is the buffered tape input being parsed in readInput.
• y is the current rung of the ladder (a string in L(B) of the common length).
• v is the target endpoint of the ladder.
• counter bounds the number of remaining rungs to try (so the machine halts).

Note: the components buf, y, v are stored inside the state for convenience but represent information that fits in O(n) tape cells in the simulating linear-space NTM.

• phase : LadderPhase
• buf : List (LadderTapeSymbol α)
• y : List α
• v : List α
• counter : ℕ

def SpaceComplexity.instDecidableEqLadderState.decEq {α✝ : Type} [DecidableEq α✝] (x✝ x✝¹ : LadderState α✝) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance SpaceComplexity.instDecidableEqLadderState {α✝ : Type} [DecidableEq α✝] : DecidableEq (LadderState α✝)

noncomputable def SpaceComplexity.ladderNTMδ {α σ : Type} [Fintype α] [DecidableEq α] [Fintype σ] [DecidableEq σ] (B : DFA α σ) (q : LadderState α) (sym : LadderTapeSymbol α) : Set (LadderState α × LadderTapeSymbol α × TuringMachine.Direction)

Transition relation of the linear-space NTM deciding LADDER_DFA. At the end of readInput it parses the buffer into a pair (u, v) of equal-length strings with u ∈ L(B), and either accepts immediately (if u = v) or enters searchFwd with y := u and counter := |α|^|u| (the maximum possible number of rungs without repetition). In searchFwd it nondeterministically guesses a position i and symbol a, sets y[i] := a, checks that the new rung is in L(B), and either accepts (if it equals v) or continues. searchBack simply moves the head left between rungs.

noncomputable def SpaceComplexity.ladderNTM {α σ : Type} [Fintype α] [DecidableEq α] [Fintype σ] [DecidableEq σ] (B : DFA α σ) : NTM (LadderState α) (LadderTapeSymbol α)

The linear-space NTM deciding LADDER_DFA for the DFA B. The state space is LadderState α, the tape alphabet is LadderTapeSymbol α, and the transition relation is ladderNTMδ B. The input alphabet consists of the lifted DFA symbols and the separator.

theorem SpaceComplexity.ladderNTM_language {α σ : Type} [Fintype α] [DecidableEq α] [Fintype σ] [DecidableEq σ] (B : DFA α σ) : (ladderNTM B).language = LADDER_DFA_Lang B

Correctness of the NTM: ladderNTM B accepts exactly the encoded ladder pairs of B.

theorem SpaceComplexity.ladderNTM_runs_in_linear_space {α σ : Type} [Fintype α] [DecidableEq α] [Fintype σ] [DecidableEq σ] (B : DFA α σ) : ∃ (g : ℕ → ℕ), IsAsympBoundedBy g id ∧ (ladderNTM B).RunsInSpace g

The NTM ladderNTM B runs in linear space: there is a space-bound function g that is asymptotically bounded by id, and ladderNTM B runs within space g.

theorem SpaceComplexity.LADDER_DFA_in_NSPACE_n {α σ : Type} [Fintype α] [DecidableEq α] [Fintype σ] [DecidableEq σ] (B : DFA α σ) : InNSPACE id (LADDER_DFA_Lang B)

Theorem (Lecture 17). LADDER_DFA ∈ NSPACE(n). Combining the correctness lemma ladderNTM_language with the linear-space bound ladderNTM_runs_in_linear_space, the language LADDER_DFA_Lang B is decided by an NTM in O(n) tape cells.

theorem SpaceComplexity.LADDER_DFA_in_NPSPACE {α σ : Type} [Fintype α] [DecidableEq α] [Fintype σ] [DecidableEq σ] (B : DFA α σ) : InNPSPACE (LADDER_DFA_Lang B)

Theorem (Lecture 17). LADDER_DFA ∈ NPSPACE. Since NSPACE(n) ⊆ NSPACE(n^1) ⊆ NPSPACE, the result follows from LADDER_DFA_in_NSPACE_n.

structure SpaceComplexity.DFAEncoding : Type 1

A uniform encoding scheme for triples ⟨B, u, v⟩ over a single fixed tape alphabet Γ, suitable for stating LADDER_DFA as a single language. It packages:

• a tape alphabet Γ;
• an encoding function encode for any DFA B and strings u, v;
• a decidable validity predicate isValidEncoding characterising the image of encode;
• and a lower bound |u| + |v| ≤ |encode B u v| ensuring that the encoded input is at least as long as the data it represents (so a linear-space bound on the encoding translates back to a linear bound on the underlying strings).

• Γ : Type
• encode {α σ : Type} [Fintype α] [Fintype σ] (B : DFA α σ) (u v : List α) : List self.Γ
• isValidEncoding : List self.Γ → Prop
• isValidEncoding_iff (w : List self.Γ) : self.isValidEncoding w ↔ ∃ (α : Type) (σ : Type) (x : Fintype α) (x_1 : Fintype σ) (B : DFA α σ) (u : List α) (v : List α), w = self.encode B u v
• encode_length_lower_bound {α σ : Type} [Fintype α] [Fintype σ] (B : DFA α σ) (u v : List α) : u.length + v.length ≤ (self.encode B u v).length

def SpaceComplexity.LADDER_DFA_Uniform (enc : DFAEncoding) : Set (List enc.Γ)

The uniform formulation LADDER_DFA = {⟨B, u, v⟩ | B is a DFA and there is a ladder in L(B)fromutov} over a fixed tape alphabet, using a DFAEncoding.

theorem SpaceComplexity.LADDER_DFA_Uniform_in_NSPACE_n (enc : DFAEncoding) : InNSPACE id (LADDER_DFA_Uniform enc)

Theorem (Lecture 17). Under any reasonable uniform encoding enc, the language LADDER_DFA_Uniform enc lies in NSPACE(n).