Polynomial-time loops over a range of indices

Many polynomial-time functions are easiest to describe one index at a time: the encodings of these entries, one after another; the number of indices at which a test passes; the least such index; the largest of these values. A loop over the indices 0, 1, …, n - 1 is given by a rule E, which reads pair z (1^i) (the loop's input z and the index i in unary) and outputs what the loop contributes at index i. The loops read the count and the input from one string pair (1^n) z. Counts, indices and values are written in unary, as strings of trues whose length is the number.

The one construction is concatenation over a range (catRange_mem_FP): if the rule is polynomial-time, then so is running it on every index below the count and concatenating the outputs. No bound on the loop's state has to be supplied, because a polynomial-time rule has polynomially long outputs and the loop runs at most as often as its argument is long. The rest are corollaries: the count may be any polynomial-time function of the input (flatMap_range_mem_FP), and the encoding of a list (listEncFn_mem_FP), a count (countOver_mem_FP), a bounded search (findFirst_mem_FP), a maximum (maxFn_mem_FP) and a function given one output bit at a time (bitwise_mem_FP) are all polynomial-time.

Main results

• catRange_mem_FP — concatenation over a range is polynomial-time
• flatMap_range_mem_FP — the same, over a range given by a polynomial-time count
• listEncFn_mem_FP, listEncFn_eq_bitstringEncode — writing the encoding of a list from a rule for its entries
• countOver_mem_FP, length_countOver — the total output length, in unary
• findFirst_mem_FP, length_findFirst_eq — the least index at which the rule outputs anything
• maxFn_mem_FP, maxFn_eq — the greatest output length
• bitwise_mem_FP — a function given by its length and a rule for each bit

Concatenation

@[simp]

theorem Complexity.catRange_pair (E : List Bool → List Bool) (x : List Bool) (n : ℕ) : catRange E (pair (List.replicate n true) x) = List.flatMap (fun (i : ℕ) => E (pair x (List.replicate i true))) (List.range n)

On pair (1^n) x, concatenation over a range runs the rule on pair x (1^i) for each i < n.

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

The length of a concatenation over a range is the sum of the output lengths.

theorem Complexity.catRange_mem_FP {E : List Bool → List Bool} (hE : E ∈ FP) : catRange E ∈ FP

Concatenation over a range is polynomial-time. If the rule E is polynomial-time, then so is the map from pair u z to the outputs of E on pair z (1^i) for i < |u|, concatenated.

theorem Complexity.flatMap_range_mem_FP {E m : List Bool → List Bool} (hE : E ∈ FP) (hm : m ∈ FP) : (fun (z : List Bool) => List.flatMap (fun (i : ℕ) => E (pair z (List.replicate i true))) (List.range (m z).length)) ∈ FP

Concatenation over a polynomial-time range. If E and m are polynomial-time, then so is z ↦ E ⟨z, 1^0⟩ E ⟨z, 1^1⟩ ⋯ E ⟨z, 1^(|m z| - 1)⟩.

Encoding a list

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

The list encoder is polynomial-time whenever its rule is.

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

The list encoder writes the list. If the count is the length of l and the rule writes the encoding of each entry of l, then the encoder writes the encoding of l.

Counting

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

Counting over a range is polynomial-time.

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

The count is the sum of the output lengths.

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

@[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

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

Searching over a range is polynomial-time.

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

The search counts the indices j at which the rule has output nothing on the indices up to j.

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.

The maximum

theorem Complexity.le_maxOver {f : List Bool → List Bool} {z : List Bool} (n i : ℕ) : i < n → (f (pair z (List.replicate i true))).length ≤ maxOver f z n

Every value is at most the maximum.

theorem Complexity.maxOver_attained {f : List Bool → List Bool} {z : List Bool} (n : ℕ) : 0 < n → ∃ i < n, (f (pair z (List.replicate i true))).length = maxOver f z n

The maximum is attained, when there is anything to maximise over.

theorem Complexity.maxOver_le {f : List Bool → List Bool} {z : List Bool} {B : ℕ} (n : ℕ) : (∀ i < n, (f (pair z (List.replicate i true))).length ≤ B) → maxOver f z n ≤ B

The maximum is at most any common bound on the values.

theorem Complexity.maxFn_mem_FP {f : List Bool → List Bool} (hf : f ∈ FP) : maxFn f ∈ FP

Taking a maximum over a range is polynomial-time.

theorem Complexity.maxFn_eq (f : List Bool → List Bool) {n : ℕ} {z : List Bool} : (maxFn f (pair (List.replicate n true) z)).length = maxOver f z n

maxFn computes the maximum, in unary.

One bit at a time

theorem Complexity.bitwise_mem_FP {len : List Bool → ℕ} {b : List Bool → ℕ → Bool} (hlen : (fun (x : List Bool) => List.replicate (len x) true) ∈ FP) {G : List Bool → List Bool} (hG : G ∈ FP) (hGspec : ∀ (x : List Bool) (i : ℕ), G (pair x (List.replicate i true)) = [b x i]) : (fun (x : List Bool) => List.map (b x) (List.range (len x))) ∈ FP

A function described bit by bit is polynomial-time. If the output length is computable in unary and each output bit is computable from the input and the position in unary, the function itself is in FP.