Reductions that edit the word of an instance–word pair

Quantifier and certificate arguments work with problems on pairs (a, w) of an instance and a bit string, encoded by encPair enc encBits. Cutting the word to a prefix or suffix whose length is computed from a, or appending a second word to it, is polynomial-time, so each operation reduces the edited problem to the original one.

Main results

• Cslib.Complexity.polyTimeReducible_take, Cslib.Complexity.polyTimeReducible_drop: keeping or dropping the first N a bits of the word, for N computable in polynomial time in unary.
• Cslib.Complexity.polyTimeReducible_append: appending a second word to the word.

theorem Cslib.Complexity.polyTimeReducible_take {α : Type} {enc : α ↪ List Bool} {N : α → ℕ} (hN : Turing.MultiTapeTM.ComputableInPolyTime N enc Turing.MultiTapeTM.encUnary) (C : Set (α × List Bool)) : PolyTimeReducible (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) {x : α × List Bool | (x.1, List.take (N x.1) x.2) ∈ C} C

Keeping the first N a bits of the word of (a, w) is a polynomial-time reduction, for N computable in polynomial time in unary.

theorem Cslib.Complexity.polyTimeReducible_drop {α : Type} {enc : α ↪ List Bool} {N : α → ℕ} (hN : Turing.MultiTapeTM.ComputableInPolyTime N enc Turing.MultiTapeTM.encUnary) (C : Set (α × List Bool)) : PolyTimeReducible (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) {x : α × List Bool | (x.1, List.drop (N x.1) x.2) ∈ C} C

Dropping the first N a bits of the word of (a, w) is a polynomial-time reduction, for N computable in polynomial time in unary.

theorem Cslib.Complexity.polyTimeReducible_append {α : Type} {enc : α ↪ List Bool} (C : Set (α × List Bool)) : PolyTimeReducible (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) {((a, s), u) : (α × List Bool) × List Bool | (a, s ++ u) ∈ C} C

Appending a word u to the word of (a, s) is a polynomial-time reduction.