A self-delimiting code for binary strings

A program for x followed by a program for y can only be split back into the two programs if the end of the first one is marked. The self-delimiting code selfDelimitingCode p of a binary string p is 1^{|ℓ|} 0 ℓ p, where ℓ is the binary representation of the length of p (Nat.bits, least significant digit first): the unary prefix gives the length of ℓ, and ℓ gives the length of p. It costs 2 size |p| + 1 bits, that is 2 log₂ |p| + O(1) Li and Vitányi, Chapter 1. The decoder decodeSelfDelimiting splits a self-delimiting code followed by any string back into the two (decodeSelfDelimiting_selfDelimitingCode_append). It splits every string, so it is a total function, and it only uses operations that are primitive recursive in Mathlib's sense (List.idxOf, List.take, List.drop, List.foldr).

Main definitions

• Cslib.Kolmogorov.selfDelimitingCode: a binary string prefixed by its length.
• Cslib.Kolmogorov.decodeSelfDelimiting: the decoder.

Main results

• Cslib.Kolmogorov.decodeSelfDelimiting_selfDelimitingCode_append: the decoder inverts the code.
• Cslib.Kolmogorov.selfDelimitingCode_append_inj: a self-delimiting code followed by any string determines both.
• Cslib.Kolmogorov.length_selfDelimitingCode: the code of p has length |p| + 2 size |p| + 1.

References

• M. Li, P. Vitányi, An Introduction to Kolmogorov Complexity and Its Applications

def Cslib.Kolmogorov.selfDelimitingCode (p : List Bool) : List Bool

The self-delimiting code 1^{|ℓ|} 0 ℓ p of a binary string p, where ℓ = Nat.bits |p| is the binary representation of the length of p Li and Vitányi, Chapter 1.

def Cslib.Kolmogorov.decodeSelfDelimiting (q : List Bool) : List Bool × List Bool

The decoder of the self-delimiting code: decodeSelfDelimiting (selfDelimitingCode p ++ q) is (p, q). It reads the number k of leading trues, the number n whose binary representation follows the first false in k bits, and then splits off the next n bits.

@[simp]

theorem Cslib.Kolmogorov.decodeSelfDelimiting_selfDelimitingCode_append (p q : List Bool) : decodeSelfDelimiting (selfDelimitingCode p ++ q) = (p, q)

The decoder inverts the code: it splits selfDelimitingCode p ++ q back into p and q.

theorem Cslib.Kolmogorov.selfDelimitingCode_append_inj {p p' q q' : List Bool} (h : selfDelimitingCode p ++ q = selfDelimitingCode p' ++ q') : p = p' ∧ q = q'

A self-delimiting code followed by any string determines both.

theorem Cslib.Kolmogorov.selfDelimitingCode_injective : Function.Injective selfDelimitingCode

theorem Cslib.Kolmogorov.length_selfDelimitingCode (p : List Bool) : (selfDelimitingCode p).length = p.length + (2 * p.length.size + 1)

The self-delimiting code of p costs 2 size |p| + 1 bits.