Languages determined by the parity of the input length

The first genuinely linear-time examples: scan the input, toggling a bit each step, and write the answer once we hit a blank. Demonstrates a textbook scan-style TM with an O(n) time bound, proved by induction on the input.

Main definitions

• TM.evenLengthTM — 4-state scanning TM (start, even, odd, done).
• Language.evenLength — strings of even length.
• Language.oddLength — strings of odd length.

Main results

• evenLengthTM_reachesIn — halts in |x| + 2 steps with 1 iff |x| is even.
• evenLength_in_DTIME, oddLength_in_DTIME — both in DTIME(n + 2).
• evenLength_mem_P, oddLength_mem_P — derived via DTIME_mono / P_compl.
• oddLength_eq_compl_evenLength — explicit Boolean identity.

inductive Complexity.TM.LengthParityPhase : Type

Control states of evenLengthTM.

• start : LengthParityPhase
• even : LengthParityPhase
• odd : LengthParityPhase
• done : LengthParityPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqLengthParityPhase : DecidableEq LengthParityPhase

Equations

• Complexity.TM.instDecidableEqLengthParityPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.TM.instFintypeLengthParityPhase : Fintype LengthParityPhase

Equations

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

def Complexity.TM.evenLengthTM {n : ℕ} : TM n

Scanning TM that writes 1 if the input length is even, 0 otherwise. Uses exactly 4 control states and halts in |x| + 2 steps on every input.

Equations

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

theorem Complexity.TM.evenLengthTM_reachesIn {n : ℕ} (x : List Bool) : ∃ (c' : Cfg n evenLengthTM.Q), evenLengthTM.reachesIn (x.length + 2) (evenLengthTM.initCfg x) c' ∧ evenLengthTM.halted c' ∧ c'.output.cells 1 = if x.length % 2 = 0 then Γ.one else Γ.zero

evenLengthTM halts in |x| + 2 steps on every input, writing Γ.one to output cell 1 iff |x| is even.

def Complexity.Language.evenLength : Language

Strings of even length (including the empty string).

Equations

• Complexity.Language.evenLength = {x : List Bool | x.length % 2 = 0}

def Complexity.Language.oddLength : Language

Strings of odd length.

Equations

• Complexity.Language.oddLength = {x : List Bool | x.length % 2 = 1}

theorem Complexity.oddLength_eq_compl_evenLength : Language.oddLength = Language.evenLengthᶜ

theorem Complexity.evenLengthTM_decidesInTime : TM.evenLengthTM.DecidesInTime Language.evenLength fun (n : ℕ) => n + 2

evenLengthTM decides evenLength in time n + 2.

theorem Complexity.evenLength_in_DTIME : Language.evenLength ∈ DTIME fun (n : ℕ) => n + 2

evenLength ∈ DTIME(n + 2).

theorem Complexity.evenLength_mem_P : Language.evenLength ∈ P

evenLength ∈ P.

theorem Complexity.oddLength_mem_P : Language.oddLength ∈ P

oddLength ∈ P via P_compl.