Writing out a list of encoded entries

The encoding of a list is its entries' encodings run together inside one pair of brackets. So a machine that can produce each entry's encoding can produce the list's, by accumulating them in a loop.

The loop is iterate_mem_FP, and the state carries the accumulated bits, the counter, and the input the entries are read from.

Main definitions

• Complexity.listStep — append the next entry's encoding

Main results

• Complexity.listStep_iterate — what the loop accumulates
• Complexity.bitstringEncode_of_entries — the accumulation is the encoding
• Complexity.listEncFn_mem_FP, Complexity.listEncFn_eq — the loop is polynomial time and writes the encoding

def Complexity.listStep (E : List Bool → List Bool) (st : List Bool) : List Bool

One step: append the next entry's encoding and advance the counter. The state is pair (pair accumulated counter) input.

Equations

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

theorem Complexity.listStep_mem_FP {E : List Bool → List Bool} (hE : E ∈ FP) : listStep E ∈ FP

def Complexity.entryCat (E : List Bool → List Bool) (x : List Bool) (n : ℕ) : List Bool

The bits the loop has accumulated after n steps.

Equations

• Complexity.entryCat E x n = List.flatMap (fun (i : ℕ) => E (Complexity.pair x (List.replicate i true))) (List.range n)

@[simp]

theorem Complexity.entryCat_zero (E : List Bool → List Bool) (x : List Bool) : entryCat E x 0 = []

theorem Complexity.entryCat_succ (E : List Bool → List Bool) (x : List Bool) (n : ℕ) : entryCat E x (n + 1) = entryCat E x n ++ E (pair x (List.replicate n true))

theorem Complexity.listStep_iterate (E : List Bool → List Bool) (x : List Bool) (n : ℕ) : (listStep E)^[n] (pair (pair [] []) x) = pair (pair (entryCat E x n) (List.replicate n true)) x

What the loop accumulates.

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

The accumulation is the encoding. If each step writes the encoding of the corresponding entry, the loop writes the inner part of the list's own encoding.

theorem Complexity.length_entryCat_le (E : List Bool → List Bool) (x : List Bool) (b n : ℕ) : (∀ i < n, (E (pair x (List.replicate i true))).length ≤ b) → (entryCat E x n).length ≤ n * b

The loop as one function

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

The list encoder, on pair (unary count) input.

Equations

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

theorem Complexity.listEncFn_mem_FP {E : List Bool → List Bool} (hE : E ∈ FP) (p : Polynomial ℕ) (hbound : ∀ (z : List Bool), ∀ k ≤ (pairFst z).length, ((listStep E)^[k] (pair (pair [] []) (pairSnd z))).length ≤ Polynomial.eval z.length p) : listEncFn E ∈ FP

theorem Complexity.listEncFn_eq (E : List Bool → List Bool) (z : List Bool) : listEncFn E z = false :: entryCat E (pairSnd z) (pairFst z).length ++ [true]

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 loop writes the list's encoding.