Reading a table of unary numbers

An algorithm that materializes a graph writes a list of records and reads them back. PosScan reads an entry of an encoded list, and DataEncode writes the entries; what is missing is getting a number back out, in the unary form the loops of the toolkit consume.

Storing the number in unary makes that a length computation: the encoding of a unary string of w marks is 4 * w + 2 bits long — two brackets, and four bits a mark — so dividing the length by four recovers the marks. No parsing of the encoding is needed, and no binary arithmetic.

The same scan reads the two halves of an encoded pair, since a pair is encoded as the two-element list of its halves.

Main definitions

• Complexity.unaryOf — the marks an encoded unary string stands for
• Complexity.fstEnc, Complexity.sndEnc — the halves of an encoded pair

Main results

• Complexity.unaryOf_encode, Complexity.unaryOf_mem_FP
• Complexity.fstEnc_eq, Complexity.sndEnc_eq, and their FP versions
• Complexity.tableFst_eq, Complexity.tableSnd_eq — an entry of a table of pairs of unary numbers, read back in unary
• Complexity.recFst_eq, Complexity.recSnd_eq, Complexity.recThd_eq — the same for records of three numbers
• Complexity.encPair_eq — and written out

Numbers

theorem Complexity.size_encode_replicate (w : ℕ) : (DataEncode.encode (List.replicate w true)).size = 4 * w + 2

The size of an encoded unary string: two brackets and four bits a mark.

theorem Complexity.length_bitstringEncode_replicate (w : ℕ) : (DataEncode.bitstringEncode (List.replicate w true)).length = 4 * w + 2

noncomputable def Complexity.unaryOf (e : List Bool) : List Bool

The unary number an encoded unary string stands for.

Equations

• Complexity.unaryOf e = Complexity.divFn [false, false, false, false] (Complexity.dropOne (Complexity.dropOne e))

theorem Complexity.unaryOf_encode (w : ℕ) : unaryOf (DataEncode.bitstringEncode (List.replicate w true)) = List.replicate w true

theorem Complexity.unaryOf_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => unaryOf (a z)) ∈ FP

Pairs

noncomputable def Complexity.fstEnc (e : List Bool) : List Bool

The first half of an encoded pair.

Equations

• Complexity.fstEnc e = Complexity.posAt e 0

noncomputable def Complexity.sndEnc (e : List Bool) : List Bool

The second half of an encoded pair.

Equations

• Complexity.sndEnc e = Complexity.posAt e 1

theorem Complexity.bitstringEncode_prod {α β : Type} [DataEncode α] [DataEncode β] (a : α) (b : β) : DataEncode.bitstringEncode (a, b) = DataEncode.bitstringEncode [DataEncode.encode a, DataEncode.encode b]

theorem Complexity.fstEnc_eq {α β : Type} [DataEncode α] [DataEncode β] (a : α) (b : β) : fstEnc (DataEncode.bitstringEncode (a, b)) = DataEncode.bitstringEncode a

theorem Complexity.sndEnc_eq {α β : Type} [DataEncode α] [DataEncode β] (a : α) (b : β) : sndEnc (DataEncode.bitstringEncode (a, b)) = DataEncode.bitstringEncode b

theorem Complexity.fstEnc_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => fstEnc (a z)) ∈ FP

theorem Complexity.sndEnc_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => sndEnc (a z)) ∈ FP

Unary arithmetic with constants

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

Any string, as that many marks.

Equations

• Complexity.marks s = Complexity.divFn [false] s

theorem Complexity.marks_eq (s : List Bool) : marks s = List.replicate s.length true

theorem Complexity.marks_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => marks (a z)) ∈ FP

noncomputable def Complexity.divC (c : ℕ) (s : List Bool) : List Bool

Division by a constant.

Equations

• Complexity.divC c s = Complexity.divFn (List.replicate c false) s

theorem Complexity.divC_eq {c : ℕ} (hc : 0 < c) (s : List Bool) : divC c s = List.replicate (s.length / c) true

theorem Complexity.divC_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) (c : ℕ) : (fun (z : List Bool) => divC c (a z)) ∈ FP

noncomputable def Complexity.modC (c : ℕ) (s : List Bool) : List Bool

Remainder by a constant.

Equations

• Complexity.modC c s = Complexity.modFn (List.replicate c false) s

theorem Complexity.modC_eq {c : ℕ} (hc : 0 < c) (s : List Bool) : modC c s = List.replicate (s.length % c) true

theorem Complexity.modC_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) (c : ℕ) : (fun (z : List Bool) => modC c (a z)) ∈ FP

def Complexity.mulLen (a b : List Bool) : List Bool

The product of two lengths.

Equations

• Complexity.mulLen a b = List.replicate (a.length * b.length) false

@[simp]

theorem Complexity.length_mulLen (a b : List Bool) : (mulLen a b).length = a.length * b.length

theorem Complexity.mulLen_mem_FP {f g : List Bool → List Bool} (hf : f ∈ FP) (hg : g ∈ FP) : (fun (z : List Bool) => mulLen (f z) (g z)) ∈ FP

def Complexity.mulC (c : ℕ) (s : List Bool) : List Bool

Multiplication by a constant, as a length.

Equations

• Complexity.mulC c s = List.replicate (s.length * c) false

@[simp]

theorem Complexity.length_mulC (c : ℕ) (s : List Bool) : (mulC c s).length = s.length * c

theorem Complexity.mulC_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) (c : ℕ) : (fun (z : List Bool) => mulC c (a z)) ∈ FP

Writing records

def Complexity.encUnary (s : List Bool) : List Bool

The encoding of a unary string.

Equations

• Complexity.encUnary s = false :: List.flatMap Complexity.boolBits s ++ [true]

theorem Complexity.encUnary_eq (s : List Bool) : encUnary s = DataEncode.bitstringEncode s

theorem Complexity.encUnary_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => encUnary (a z)) ∈ FP

def Complexity.encPair (a b : List Bool) : List Bool

The encoding of a pair of unary strings.

Equations

• Complexity.encPair a b = false :: (Complexity.encUnary a ++ Complexity.encUnary b) ++ [true]

theorem Complexity.bitstringEncode_prod_eq {α β : Type} [DataEncode α] [DataEncode β] (a : α) (b : β) : DataEncode.bitstringEncode (a, b) = false :: (DataEncode.bitstringEncode a ++ DataEncode.bitstringEncode b) ++ [true]

theorem Complexity.encPair_eq (a b : List Bool) : encPair a b = DataEncode.bitstringEncode (a, b)

theorem Complexity.encPair_mem_FP {a b : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) : (fun (z : List Bool) => encPair (a z) (b z)) ∈ FP

theorem Complexity.unaryOf_fstEnc_encPair (w c : ℕ) : unaryOf (fstEnc (encPair (List.replicate w true) (List.replicate c true))) = List.replicate w true

theorem Complexity.unaryOf_sndEnc_encPair (w c : ℕ) : unaryOf (sndEnc (encPair (List.replicate w true) (List.replicate c true))) = List.replicate c true

@[simp]

theorem Complexity.marks_append_mulC (w m c : ℕ) : marks (List.replicate w true ++ mulC c (List.replicate m true)) = List.replicate (w + m * c) true

theorem Complexity.length_mulC_append (m c w : ℕ) : (mulC c (List.replicate m true) ++ List.replicate w true).length = m * c + w

theorem Complexity.length_bitstringEncode_list {α : Type} [DataEncode α] (l : List α) : (DataEncode.bitstringEncode l).length = 2 + (List.map (fun (a : α) => (DataEncode.bitstringEncode a).length) l).sum

The encoding of a list is two brackets and its entries' encodings.

@[simp]

theorem Complexity.length_encPair (w c : ℕ) : (encPair (List.replicate w true) (List.replicate c true)).length = 4 * w + 4 * c + 6

Tables of pairs of numbers

noncomputable def Complexity.tableFst (T : List Bool) (j : ℕ) : List Bool

The first number of the j-th record of a table, in unary.

Equations

• Complexity.tableFst T j = Complexity.unaryOf (Complexity.fstEnc (Complexity.posAt T j))

noncomputable def Complexity.tableSnd (T : List Bool) (j : ℕ) : List Bool

The second number of the j-th record of a table, in unary.

Equations

• Complexity.tableSnd T j = Complexity.unaryOf (Complexity.sndEnc (Complexity.posAt T j))

theorem Complexity.tableFst_def (T : List Bool) (j : ℕ) : tableFst T j = unaryOf (fstEnc (posAt T j))

theorem Complexity.tableSnd_def (T : List Bool) (j : ℕ) : tableSnd T j = unaryOf (sndEnc (posAt T j))

theorem Complexity.tableFst_eq {l : List (List Bool × List Bool)} {j w c : ℕ} (hj : j < l.length) (h : l[j] = (List.replicate w true, List.replicate c true)) : tableFst (DataEncode.bitstringEncode l) j = List.replicate w true

theorem Complexity.tableSnd_eq {l : List (List Bool × List Bool)} {j w c : ℕ} (hj : j < l.length) (h : l[j] = (List.replicate w true, List.replicate c true)) : tableSnd (DataEncode.bitstringEncode l) j = List.replicate c true

theorem Complexity.tableFst_mem_FP {a b : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) : (fun (z : List Bool) => tableFst (b z) (a z).length) ∈ FP

theorem Complexity.tableSnd_mem_FP {a b : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) : (fun (z : List Bool) => tableSnd (b z) (a z).length) ∈ FP

Records of three numbers

def Complexity.encTriple (a b c : List Bool) : List Bool

The encoding of three unary strings.

Equations

• Complexity.encTriple a b c = false :: (Complexity.encUnary a ++ Complexity.encPair b c) ++ [true]

theorem Complexity.encTriple_eq (a b c : List Bool) : encTriple a b c = DataEncode.bitstringEncode (a, b, c)

@[simp]

theorem Complexity.length_encTriple (a b c : ℕ) : (encTriple (List.replicate a true) (List.replicate b true) (List.replicate c true)).length = 4 * a + 4 * b + 4 * c + 10

theorem Complexity.encTriple_mem_FP {a b c : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) (hc : c ∈ FP) : (fun (z : List Bool) => encTriple (a z) (b z) (c z)) ∈ FP

noncomputable def Complexity.recFst (T : List Bool) (j : ℕ) : List Bool

The first number of the j-th record of a table of triples.

Equations

• Complexity.recFst T j = Complexity.unaryOf (Complexity.fstEnc (Complexity.posAt T j))

noncomputable def Complexity.recSnd (T : List Bool) (j : ℕ) : List Bool

The second.

Equations

• Complexity.recSnd T j = Complexity.unaryOf (Complexity.fstEnc (Complexity.sndEnc (Complexity.posAt T j)))

noncomputable def Complexity.recThd (T : List Bool) (j : ℕ) : List Bool

The third.

Equations

• Complexity.recThd T j = Complexity.unaryOf (Complexity.sndEnc (Complexity.sndEnc (Complexity.posAt T j)))

theorem Complexity.recFst_eq {j : ℕ} {l3 : List (List Bool × List Bool × List Bool)} {a b c : ℕ} (hj : j < l3.length) (h : l3[j] = (List.replicate a true, List.replicate b true, List.replicate c true)) : recFst (DataEncode.bitstringEncode l3) j = List.replicate a true

theorem Complexity.recSnd_eq {j : ℕ} {l3 : List (List Bool × List Bool × List Bool)} {a b c : ℕ} (hj : j < l3.length) (h : l3[j] = (List.replicate a true, List.replicate b true, List.replicate c true)) : recSnd (DataEncode.bitstringEncode l3) j = List.replicate b true

theorem Complexity.recThd_eq {j : ℕ} {l3 : List (List Bool × List Bool × List Bool)} {a b c : ℕ} (hj : j < l3.length) (h : l3[j] = (List.replicate a true, List.replicate b true, List.replicate c true)) : recThd (DataEncode.bitstringEncode l3) j = List.replicate c true

theorem Complexity.recFst_mem_FP {f g : List Bool → List Bool} (hf : f ∈ FP) (hg : g ∈ FP) : (fun (z : List Bool) => recFst (g z) (f z).length) ∈ FP

theorem Complexity.recSnd_mem_FP {f g : List Bool → List Bool} (hf : f ∈ FP) (hg : g ∈ FP) : (fun (z : List Bool) => recSnd (g z) (f z).length) ∈ FP

theorem Complexity.recThd_mem_FP {f g : List Bool → List Bool} (hf : f ∈ FP) (hg : g ∈ FP) : (fun (z : List Bool) => recThd (g z) (f z).length) ∈ FP

Digit sums

noncomputable def Complexity.digitSum (radix : ℕ) (digit : ℕ → List Bool → List Bool) : ℕ → List Bool → List Bool

A number from its digits: ∑ j < n, digit j · radix ^ j, written in marks. The digits are read from the input, so this is how an algorithm assembles a mixed-radix number out of constantly many pieces.

Equations

• Complexity.digitSum radix digit 0 x✝ = []
• Complexity.digitSum radix digit n.succ x✝ = Complexity.digitSum radix digit n x✝ ++ Complexity.mulC (radix ^ n) (digit n x✝)

theorem Complexity.digitSum_mem_FP {radix : ℕ} {digit : ℕ → List Bool → List Bool} (hd : ∀ (i : ℕ), digit i ∈ FP) (n : ℕ) : digitSum radix digit n ∈ FP

@[simp]

theorem Complexity.length_digitSum (radix : ℕ) (digit : ℕ → List Bool → List Bool) (w : List Bool) (n : ℕ) : (digitSum radix digit n w).length = ∑ j ∈ Finset.range n, (digit j w).length * radix ^ j

theorem Complexity.length_digitSum_le {radix : ℕ} (hr : 0 < radix) {digit : ℕ → List Bool → List Bool} {d : ℕ} (hd : ∀ (j : ℕ) (w : List Bool), (digit j w).length ≤ d) (n : ℕ) (w : List Bool) : (digitSum radix digit n w).length ≤ n * (d * radix ^ n)