Log-space transducer classes

This file defines the log-space complexity classes L, NL, coNL, FL, and the search problem classes FNL, TFNL.

These classes use the library's honest auxiliary-space convention: work-tape travel is bounded, excess input-head travel is charged, and language deciders also charge two-way output-tape travel beyond the verdict cell. They additionally use the transducer discipline (IsTransducer), under which the output head never moves left. TM.ComputesInSpace includes this discipline internally so function output may have unbounded length without becoming read-write workspace.

def Complexity.L : Set Language

L (LOGSPACE) is the class of languages decidable by a deterministic log-space transducer: a DTM with O(log n) auxiliary space whose output tape head never moves left. The transducer constraint prevents the output tape from being used as extra workspace beyond the space bound.

Equations

• Complexity.L = {Lang : Complexity.Language | ∃ (k : ℕ) (tm : Complexity.TM k) (f : ℕ → ℕ), tm.IsTransducer ∧ tm.DecidesInSpace Lang f ∧ Complexity.BigO f fun (n : ℕ) => Nat.log 2 n}

def Complexity.NL : Set Language

NL is the class of languages decidable by a nondeterministic log-space transducer: an NTM with O(log n) auxiliary space whose output tape head never moves left.

Equations

• Complexity.NL = {Lang : Complexity.Language | ∃ (k : ℕ) (tm : Complexity.NTM k) (f : ℕ → ℕ), tm.IsTransducer ∧ tm.DecidesInSpace Lang f ∧ Complexity.BigO f fun (n : ℕ) => Nat.log 2 n}

def Complexity.coNL : Set Language

coNL is the class of languages whose complements are in NL. By the Immerman-Szelepcsényi theorem coNL = NL, but this is nontrivial.

Equations

• Complexity.coNL = Complexity.complClass Complexity.NL

def Complexity.FL : Set (List Bool → List Bool)

FL is the class of functions computable by a deterministic log-space transducer: a DTM with O(log n) auxiliary space whose output tape head never moves left.

Equations

• Complexity.FL = {f : List Bool → List Bool | ∃ (k : ℕ) (tm : Complexity.TM k) (S : ℕ → ℕ), tm.ComputesInSpace f S ∧ Complexity.BigO S fun (n : ℕ) => Nat.log 2 n}

def Complexity.FNL : Set (List Bool → List Bool → Prop)

FNL is the class of search problems with log-space verifiable relations: binary relations that are polynomially balanced (witnesses have poly-bounded length) and whose pair language is decidable in L (deterministic log space).

This parallels FNP, which uses P (deterministic poly time) for verification.

Equations

• Complexity.FNL = {R : List Bool → List Bool → Prop | Complexity.PolyBalanced R ∧ Complexity.pairLang R ∈ Complexity.L}

def Complexity.TFNL : Set (List Bool → List Bool → Prop)

TFNL is the class of total FNL search problems: every instance has at least one witness.

Equations

• Complexity.TFNL = {R : List Bool → List Bool → Prop | R ∈ Complexity.FNL ∧ ∀ (x : List Bool), ∃ (y : List Bool), R x y}