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. ListEncode runs the loop that does it, but asks for a bound on the loop's own state; this module discharges that bound from the rule alone, since a polynomial-time rule has polynomially bounded output and the loop runs no more often than its argument is long.

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.countOver, Complexity.length_countOver — the same loop used to add up a rule's outputs, which is how a bounded count is taken
• Complexity.findFirst, Complexity.length_findFirst — and, run twice, how a bounded search is made
• Complexity.ifEqLen, Complexity.ifLtLen — comparing two unary numbers, and branching on the answer
• Complexity.length_findFirst_eq — the search returns the least index the rule answers at

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: a polynomial-time rule already has polynomially bounded output, and the loop runs only as many times as its own argument is long.

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.

Adding up

theorem Complexity.length_entryCat (E : List Bool → List Bool) (x : List Bool) (n : ℕ) : (entryCat E x n).length = ∑ i ∈ Finset.range n, (E (pair x (List.replicate i true))).length

noncomputable def Complexity.countOver (E : List Bool → List Bool) (z : List Bool) : List Bool

The total length of a rule's outputs over a range, in unary. Running the rule for its length alone is how a loop counts: a rule that answers [true] or [] counts the indices where it says yes.

Equations

• Complexity.countOver E z = Complexity.marks (Complexity.dropOne (Complexity.dropOne (Complexity.listEncFn E z)))

theorem Complexity.countOver_mem_FP {E : List Bool → List Bool} (hE : E ∈ FP) : countOver E ∈ FP

theorem Complexity.length_countOver (E : List Bool → List Bool) (x : List Bool) (n : ℕ) : (countOver E (pair (List.replicate n true) x)).length = ∑ i ∈ Finset.range n, (E (pair x (List.replicate i true))).length

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

theorem Complexity.countOver_eq_replicate (E : List Bool → List Bool) (z : List Bool) : countOver E z = List.replicate (countOver E z).length true

The count is written in marks.

Searching

noncomputable def Complexity.isEmptyMark (s : List Bool) : List Bool

One mark when the string is empty, none otherwise.

Equations

• Complexity.isEmptyMark s = Complexity.Cobham.selectHead (Complexity.Cobham.emptyFlag s) [true] []

@[simp]

theorem Complexity.isEmptyMark_nil : isEmptyMark [] = [true]

@[simp]

theorem Complexity.isEmptyMark_cons (b : Bool) (t : List Bool) : isEmptyMark (b :: t) = []

theorem Complexity.length_isEmptyMark (s : List Bool) : (isEmptyMark s).length = if s = [] then 1 else 0

theorem Complexity.isEmptyMark_mem_FP {f : List Bool → List Bool} (hf : f ∈ FP) : (fun (z : List Bool) => isEmptyMark (f z)) ∈ FP

noncomputable def Complexity.findFirst (E : List Bool → List Bool) (z : List Bool) : List Bool

The least index below the bound at which the rule answers something, or the bound itself when it never does: count the indices no answer has been seen up to.

Equations

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

theorem Complexity.findFirst_mem_FP {E : List Bool → List Bool} (hE : E ∈ FP) : findFirst E ∈ FP

theorem Complexity.findFirst_eq_replicate (E : List Bool → List Bool) (z : List Bool) : findFirst E z = List.replicate (findFirst E z).length true

The search's answer is written in marks.

theorem Complexity.length_findFirst (E : List Bool → List Bool) (x : List Bool) (n : ℕ) : (findFirst E (pair (List.replicate n true) x)).length = ∑ j ∈ Finset.range n, if ∑ k ∈ Finset.range (j + 1), (E (pair x (List.replicate k true))).length = 0 then 1 else 0

theorem Complexity.length_findFirst_eq {E : List Bool → List Bool} {x : List Bool} {n c : ℕ} (hc : c < n) (hhit : (E (pair x (List.replicate c true))).length ≠ 0) (hmin : ∀ k < c, (E (pair x (List.replicate k true))).length = 0) : (findFirst E (pair (List.replicate n true) x)).length = c

The search returns the least index the rule answers at.