Descriptions as bit strings: the postorder serialization of data

Blueprint rem:compression-abstract, item 1: the strings of the compressibility criterion are descriptions, pairs (λ, decider) of a parameter and a decider program. This file fixes how such a pair travels as a bit string.

A pair is data (cons (encode λ) (encode decider)), and data is serialized in postorder: nil ↦ 0, cons a b ↦ a · b · 1 (Data.toBitsPost). Postorder, rather than the preorder Data.toBits, because it is read back by a stack machine (Data.stackStep): a 0 pushes nil, a 1 pops two entries and pushes their pair. A loop of the ambient model can run a stack machine on a bit string, whereas a recursive-descent reader would need recursion; the ambient program is in Halting/Lists.lean, this file has the mathematics and the primitive recursive versions.

• Data.toBitsPost, Data.stackRun, Data.parse: the serialization, the stack machine and the total reader (the top of the final stack, nil for an empty stack), with the round trip Data.parse_toBitsPost.
• Data.normBin: a total normalization of the parameter, the identity on canonical binary numerals (encode n for n : ℕ) and nil (encode 0) elsewhere; Data.natOf reads it. Every string thereby names a parameter and a decider (descLam, descDecD), and the wrapper decider of Halting/Wrapper.lean interprets the raw data the same way, so that no validity condition on strings is needed anywhere.

Each of these is also given in primitive recursive form, Data.parse and Data.natOf among them, together with Data.primrec_size: the level at which the halting reduction runs is 2 ^ (K + 1 + esize e), so the size of an encoding has to be computable.

Postorder serialization

def MIPRE.Cost.Data.toBitsPost : Data → BitStr

Postorder serialization of data: nil ↦ 0, cons a b ↦ a · b · 1.

Equations

• MIPRE.Cost.Data.nil.toBitsPost = [false]
• (a.cons b).toBitsPost = a.toBitsPost ++ b.toBitsPost ++ [true]

@[simp]

theorem MIPRE.Cost.Data.length_toBitsPost (d : Data) : List.length d.toBitsPost = d.size

def MIPRE.Cost.Data.stackStep (s : List Data) (bit : Bool) : List Data

One step of the stack machine: a 0 pushes nil; a 1 pops b then a and pushes cons a b, and does nothing on a stack with fewer than two entries.

Equations

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

@[simp]

theorem MIPRE.Cost.Data.stackStep_false (s : List Data) : stackStep s false = nil :: s

@[simp]

theorem MIPRE.Cost.Data.stackStep_true_cons_cons (b a : Data) (s : List Data) : stackStep (b :: a :: s) true = a.cons b :: s

def MIPRE.Cost.Data.stackRun (x : BitStr) (s : List Data) : List Data

Running the stack machine over a bit string from a stack.

Equations

• MIPRE.Cost.Data.stackRun x s = List.foldl MIPRE.Cost.Data.stackStep s x

@[simp]

theorem MIPRE.Cost.Data.stackRun_nil (s : List Data) : stackRun [] s = s

@[simp]

theorem MIPRE.Cost.Data.stackRun_cons (bit : Bool) (x : BitStr) (s : List Data) : stackRun (bit :: x) s = stackRun x (stackStep s bit)

theorem MIPRE.Cost.Data.stackRun_toBitsPost (d : Data) (rest : BitStr) (s : List Data) : stackRun (d.toBitsPost ++ rest) s = stackRun rest (d :: s)

The stack machine reads a serialization by pushing the datum.

def MIPRE.Cost.Data.parse (x : BitStr) : Data

The total reader: the top of the final stack, nil for an empty stack.

Equations

• MIPRE.Cost.Data.parse x = (MIPRE.Cost.Data.stackRun x []).headD MIPRE.Cost.Data.nil

@[simp]

theorem MIPRE.Cost.Data.parse_toBitsPost (d : Data) : parse d.toBitsPost = d

Primitive recursiveness

theorem MIPRE.Cost.Data.primrec_stackStep : Primrec₂ stackStep

theorem MIPRE.Cost.Data.primrec_parse : Primrec parse

The parameter: canonical binary numerals

def MIPRE.Cost.Data.isBit : Data → Bool

A datum is a bit: nil or cons nil nil.

Equations

• MIPRE.Cost.Data.nil.isBit = true
• (MIPRE.Cost.Data.nil.cons MIPRE.Cost.Data.nil).isBit = true
• x✝.isBit = false

@[simp]

theorem MIPRE.Cost.Data.isBit_ofBool (b : Bool) : (ofBool b).isBit = true

theorem MIPRE.Cost.Data.isBit_iff (d : Data) : d.isBit = true ↔ ∃ (b : Bool), d = ofBool b

def MIPRE.Cost.Data.isCanonBin (d : Data) : Bool

A datum is a canonical binary numeral: a list of bits, empty or ending in true.

Equations

• d.isCanonBin = match MIPRE.Cost.decode d with | some l => decide (l = [] ∨ List.getLast? l = some true) | none => false

theorem MIPRE.Cost.Data.encode_of_decode_bitStr {d : Data} {l : BitStr} (h : decode d = some l) : encode l = d

Decoding a bit string succeeds only on its encoding.

theorem MIPRE.Cost.Data.bits_getLast (n : ℕ) : n.bits = [] ∨ n.bits.getLast? = some true

Nat.bits is canonical: empty or ending in true.

theorem MIPRE.Cost.Data.isCanonBin_encode (n : ℕ) : (encode n).isCanonBin = true

theorem MIPRE.Cost.Data.bits_foldr_of_canon (l : BitStr) (hl : l = [] ∨ List.getLast? l = some true) : (List.foldr Nat.bit 0 l).bits = l

A canonical bit string is the binary expansion of the number it denotes.

def MIPRE.Cost.Data.normBin (d : Data) : Data

Total normalization of a parameter: canonical binary numerals are kept, everything else reads as 0.

Equations

• d.normBin = if d.isCanonBin = true then d else MIPRE.Cost.Data.nil

def MIPRE.Cost.Data.natOf (d : Data) : ℕ

The parameter a datum denotes, after normalization.

Equations

• d.natOf = (MIPRE.Cost.decode d.normBin).getD 0

@[simp]

theorem MIPRE.Cost.Data.normBin_encode (n : ℕ) : (encode n).normBin = encode n

@[simp]

theorem MIPRE.Cost.Data.natOf_encode (n : ℕ) : (encode n).natOf = n

theorem MIPRE.Cost.Data.encode_natOf (d : Data) : encode d.natOf = d.normBin

The normalized parameter is the encoding of the number it denotes.

How large a parameter a short string can denote

The bound a string of length L places on the number it denotes. Obligation O4 of the halting reduction needs it: the answer budget the classes are read with at level n grows with the described string's own compression parameter (MIPRE.Halting.ansBound), while the compression theorem's completeness clause supplies strategies at a budget fixed by the compressor's output, so the two can only be related through a bound on that parameter.

theorem MIPRE.Cost.Data.size_normBin_le (d : Data) : d.normBin.size ≤ d.size

Normalization does not grow a datum: it is either the datum or nil.

theorem MIPRE.Cost.Data.natOf_lt (d : Data) : d.natOf < 2 ^ d.size

A datum denotes a number smaller than 2 to its size. Through encode_natOf, the normalized datum is the binary encoding of the number it denotes, so the number has at most d.size binary digits.

theorem MIPRE.Cost.Data.size_sum_stackStep_le (s : List Data) (bit : Bool) : (List.map size (stackStep s bit)).sum ≤ (List.map size s).sum + 1

One step of the stack machine adds at most one to the total size on the stack: a 0 pushes nil, and a 1 replaces two entries by one node above them.

theorem MIPRE.Cost.Data.size_sum_stackRun_le (x : BitStr) (s : List Data) : (List.map size (stackRun x s)).sum ≤ (List.map size s).sum + List.length x

So the whole run adds at most the length of the string.

theorem MIPRE.Cost.Data.size_parse_le (x : BitStr) : (parse x).size ≤ max 1 (List.length x)

What a string of length L can parse to: a datum of size at most L, or nil when the run leaves the stack empty.

theorem MIPRE.Cost.Data.primrec_isCanonBin : Primrec isCanonBin

theorem MIPRE.Cost.Data.primrec_normBin : Primrec normBin

theorem MIPRE.Cost.Data.primrec_decode_nat : Primrec fun (d : Data) => decode d

theorem MIPRE.Cost.Data.primrec_natOf : Primrec natOf

The size of data

theorem MIPRE.Cost.Data.size_eq_recD (d : Data) : d.size = recD 1 (fun (x x_1 : Data) (ra rb : ℕ) => ra + rb + 1) d

The size of data is a tree recursion.

theorem MIPRE.Cost.Data.primrec_size : Primrec size

The size of data is primitive recursive, hence so is esize of anything whose encoding is: Cost.esize a = (encode a).size. The halting reduction needs it for the level 2 ^ (K + 1 + esize e) at which the recursion runs.