Counting an input's length modulo four

A single polynomial-time language, built because the analysis of the PCP statement needs one concrete verdict that depends on the length of its input: the strings whose length is divisible by four.

The construction is the obvious one, assembled from the existing toolkit rather than from a machine. A counter with four states is a finite function, so ite_mem_finset_mem_FP puts one step of it in FP; unaryLength_mem_FP supplies one tick per input bit; and iterate_mem_FP runs the ticks.

Main definitions

• Complexity.ctrStep — one step of a counter modulo four
• Complexity.lenMod4 — the language of lengths divisible by four

Main results

• Complexity.lenMod4_mem_P — it is polynomial-time decidable

def Complexity.ctrVals : Finset (List Bool)

The four states of the counter, as unary strings.

Equations

• Complexity.ctrVals = {[], [true], [true, true], [true, true, true]}

def Complexity.ctrStep (s : List Bool) : List Bool

One step of a counter modulo four. Outside the four states it resets, which keeps the function total without leaving the finite table.

Equations

• Complexity.ctrStep s = if s ∈ Complexity.ctrVals then if s.length = 3 then [] else s ++ [true] else []

theorem Complexity.ctrStep_mem_FP : ctrStep ∈ FP

theorem Complexity.replicate_mem_ctrVals {k : ℕ} (hk : k < 4) : List.replicate k true ∈ ctrVals

theorem Complexity.ctrStep_iterate (n : ℕ) : ctrStep^[n] [] = List.replicate (n % 4) true

The counter counts.

theorem Complexity.length_ctrStep_iterate_le (n : ℕ) : (ctrStep^[n] []).length ≤ 3

def Complexity.lenCtr (z : List Bool) : List Bool

The counter, run once per input bit.

Equations

• Complexity.lenCtr z = Complexity.ctrStep^[z.length] []

theorem Complexity.lenCtr_mem_FP : lenCtr ∈ FP

def Complexity.ctrIsZero (s : List Bool) : List Bool

Reading the counter: it is zero exactly on the multiples of four.

Equations

• Complexity.ctrIsZero s = if s ∈ Complexity.ctrVals then if s = [] then [true] else [false] else []

theorem Complexity.ctrIsZero_mem_FP : ctrIsZero ∈ FP

def Complexity.lenMod4 : Language

The language of lengths divisible by four.

Equations

• Complexity.lenMod4 = {z : List Bool | z.length % 4 = 0}

theorem Complexity.lenMod4_mem_P : lenMod4 ∈ P