Lax51.BinaryWordEncoding
Binary encoding of finite words
concepts/Lax51/BinaryWordEncoding.lean · lax-51
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
Definition
A finite list of natural numbers is encoded over a three-symbol alphabet. Each number begins with a separator and is followed by its canonical least-significant-bit-first binary expansion. Thus zero is represented by a separator with no following bits, and the next separator begins the next number. The empty list is represented by the empty string.
This encoding is self-delimiting at the level of numbers: separators cannot occur as binary digits. Its length is the common input-size measure used by the Turing-machine and word-RAM polynomial-time definitions in this submission.
Lean source view on GitHub
| 1 | import Mathlib.Data.Nat.Bits |
| 2 | import Mathlib.Data.Fintype.Basic |
| 3 | import Mathlib.Tactic.DeriveFintype |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Binary encoding of finite words |
| 8 | type: definition |
| 9 | --- |
| 10 | A finite list of natural numbers is encoded over a three-symbol alphabet. |
| 11 | Each number begins with a separator and is followed by its canonical |
| 12 | least-significant-bit-first binary expansion. Thus zero is represented by a |
| 13 | separator with no following bits, and the next separator begins the next |
| 14 | number. The empty list is represented by the empty string. |
| 15 | |
| 16 | This encoding is self-delimiting at the level of numbers: separators cannot |
| 17 | occur as binary digits. Its length is the common input-size measure used by |
| 18 | the Turing-machine and word-RAM polynomial-time definitions in this |
| 19 | submission. |
| 20 | -/ |
| 21 | |
| 22 | namespace Lax51.BinaryWordEncoding |
| 23 | |
| 24 | /-- The finite alphabet used to encode lists of natural numbers. -/ |
| 25 | inductive Symbol |
| 26 | | separator |
| 27 | | zero |
| 28 | | one |
| 29 | deriving DecidableEq, Fintype, Inhabited |
| 30 | |
| 31 | /-- Encode one natural number, including the separator which begins it. -/ |
| 32 | def encodeNat (n : ℕ) : List Symbol := |
| 33 | .separator :: n.bits.map (fun b => if b then .one else .zero) |
| 34 | |
| 35 | /-- The canonical binary encoding of a finite list of natural numbers. -/ |
| 36 | def encode (x : List ℕ) : List Symbol := |
| 37 | x.flatMap encodeNat |
| 38 | |
| 39 | /-- The bit-size of a finite list of natural numbers. -/ |
| 40 | def bitSize (x : List ℕ) : ℕ := |
| 41 | (encode x).length |
| 42 | |
| 43 | end Lax51.BinaryWordEncoding |
| 44 |
Community review
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.
0 comments