lengthDivBy k: length-divisibility language family

Strings whose length is divisible by k (for k ≥ 1). Decided by a (k + 2)-state scannerTM instance: the scan state is the current length taken mod k, incremented by 1 on each bit.

This generalizes evenLength (which is lengthDivBy 2).

Main definitions

• Language.lengthDivBy k.
• TM.lengthDivByTM k — scannerTM specialized to ZMod k counter.

Main results

• lengthDivBy_in_DTIME — lengthDivBy k ∈ DTIME(n + 2).
• lengthDivBy_mem_P.

def Complexity.TM.lengthDivByTM (k : ℕ) [NeZero k] : TM 0

Scanner for "input length is divisible by k". Scan state: the current length mod k (a ZMod k).

Equations

• Complexity.TM.lengthDivByTM k = Complexity.TM.scannerTM 0 (fun (s : ZMod k) (x : Bool) => s + 1) fun (s : ZMod k) => if decide (s = 0) = true then Complexity.Γw.one else Complexity.Γw.zero

def Complexity.Language.lengthDivBy (k : ℕ) : Language

Strings whose length is divisible by k.

Equations

• Complexity.Language.lengthDivBy k = {x : List Bool | k ∣ x.length}

theorem Complexity.lengthDivBy_in_DTIME (k : ℕ) [NeZero k] : Language.lengthDivBy k ∈ DTIME fun (n : ℕ) => n + 2

lengthDivBy k ∈ DTIME(n + 2).

theorem Complexity.lengthDivBy_mem_P (k : ℕ) [NeZero k] : Language.lengthDivBy k ∈ P

lengthDivBy k ∈ P.