Writing out a table

Every stage of an algorithmic reduction writes a list: the edges of a graph, the entries of a rotation table, the records of a gadget. The list encoder listEncFn of Complexitylib.Classes.P.Range writes it from a polynomial-time rule for its entries, with no bound on the loop to supply; this module names that fact the way the reductions use it, and adds the unary comparisons they branch on. The counting and searching loops that used to live here (countOver, findFirst and their lemmas) moved to Complexitylib.Classes.P.Range under the same names.

Main results

• Complexity.materialize_mem_FP — a record rule makes the list encoder polynomial time
• Complexity.materialize_eq — and it writes the list it is meant to
• Complexity.ifEqLen, Complexity.ifLtLen — comparing two unary numbers, and branching on the answer

theorem Complexity.materialize_mem_FP {E : List Bool → List Bool} (hE : E ∈ FP) : listEncFn E ∈ FP

A record rule materializes a list in polynomial time. No bound need be supplied: this is listEncFn_mem_FP.

theorem Complexity.materialize_eq {α : Type} [DataEncode α] {E : List Bool → List Bool} (l : List α) (x : List Bool) (h : ∀ (i : ℕ) (hi : i < l.length), E (pair x (List.replicate i true)) = DataEncode.bitstringEncode l[i]) : listEncFn E (pair (List.replicate l.length true) x) = DataEncode.bitstringEncode l

The list encoder writes the list.

Comparing

noncomputable def Complexity.ifEqLen (a b x y : List Bool) : List Bool

x when the two strings have the same length, y otherwise.

Equations

• Complexity.ifEqLen a b x y = Complexity.Cobham.selectHead (Complexity.Cobham.emptyFlag (List.drop a.length b ++ List.drop b.length a)) x y

theorem Complexity.ifEqLen_pos {a b : List Bool} (h : a.length = b.length) (x y : List Bool) : ifEqLen a b x y = x

theorem Complexity.ifEqLen_neg {a b : List Bool} (h : a.length ≠ b.length) (x y : List Bool) : ifEqLen a b x y = y

theorem Complexity.ifEqLen_mem_FP {a b x y : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) (hx : x ∈ FP) (hy : y ∈ FP) : (fun (z : List Bool) => ifEqLen (a z) (b z) (x z) (y z)) ∈ FP

noncomputable def Complexity.ifLtLen (a b x y : List Bool) : List Bool

x when the first string is shorter than the second, y otherwise.

Equations

• Complexity.ifLtLen a b x y = Complexity.Cobham.selectHead (Complexity.Cobham.emptyFlag (List.drop a.length b)) y x

theorem Complexity.ifLtLen_pos {a b : List Bool} (h : a.length < b.length) (x y : List Bool) : ifLtLen a b x y = x

theorem Complexity.ifLtLen_neg {a b : List Bool} (h : ¬a.length < b.length) (x y : List Bool) : ifLtLen a b x y = y

theorem Complexity.ifLtLen_mem_FP {a b x y : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) (hx : x ∈ FP) (hy : y ∈ FP) : (fun (z : List Bool) => ifLtLen (a z) (b z) (x z) (y z)) ∈ FP