Literal Atomic Prefix Parser

Abstract

The literal two-letter tree code has an executable recursive parser with exact suffix boundaries, injective code, prefix-free image, and complete decoding.

Source is the existing FreeMagma Bool of finite nonempty ordered binary trees. The true leaf is alpha and the false leaf is beta. A leaf b is encoded as [true,b], while a branch is encoded as false followed by the concatenation of the left and right codes. The parser uses predecessor fuel for both recursive children and passes the actual remainder returned by the left parse to the right parse. Its public fuel is the input length, and decode accepts only an empty final remainder.

Definition 1.1 (Literal Tree Code).

$$(\forall (b:Bool),(\mathrm{code}\left(\mathrm{of}\left(b\right)\right)=[true,b]))\wedge (\forall (s:Source)(t:Source),(\mathrm{code}\left(\mathrm{mul}\left(s,t\right)\right)=false::(\mathrm{code}\left(s\right)++\mathrm{code}\left(t\right))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/AtomicPrefixParser.code (✓ std3).

Source. Repository-derived.

Commentary.

$$code:Source\to ListBool$$

The two Boolean letters are used directly. Internal nodes begin with false, so the two child codes are parsed without a delimiter or integer encoding.

Definition 1.2 (Fuelled Suffix Parser).

$$\forall (w:ListBool),(\mathrm{parse}\left(w\right)=\mathrm{parseFuel}\left(\mathrm{length}\left(w\right),w\right))$$

Formalization. D5/S3/Arith/FibonacciAtomic/AtomicPrefixParser.parse (✓ std3).

Source. Repository-derived.

Commentary.

$$parse:ListBool\to \mathrm{Option}\left(Source\times ListBool\right)$$

Parsing returns either failure or a source tree together with the exact unconsumed suffix. The local recurrence below uses recursion-depth fuel: both child calls receive n, and the right child receives the actual left remainder r. The clauses exhaust the input shapes and recursive outcomes. The public parser derives its fuel from the input length.

$$parseFuel:Nat\to ListBool\to \mathrm{Option}\left(Source\times ListBool\right)$$

$$\forall (w:ListBool),(\mathrm{parseFuel}\left(0,w\right)=none)$$

$$\forall (n:Nat)(b:Bool)(r:ListBool),(\mathrm{parseFuel}\left(n+1,true::b::r\right)=\mathrm{some}\left((\mathrm{of}\left(b\right),r)\right))$$

$$\forall (n:Nat)(w:ListBool)(s:Source)(r:ListBool)(t:Source)(q:ListBool),(((\mathrm{parseFuel}\left(n,w\right)=\mathrm{some}\left((s,r)\right))\wedge (\mathrm{parseFuel}\left(n,r\right)=\mathrm{some}\left((t,q)\right)))\Rightarrow \mathrm{parseFuel}\left(n+1,false::w\right)=\mathrm{some}\left((\mathrm{mul}\left(s,t\right),q)\right))$$

$$\forall (n:Nat)(w:ListBool),((\mathrm{parseFuel}\left(n,w\right)=none)\Rightarrow \mathrm{parseFuel}\left(n+1,false::w\right)=none)$$

$$\forall (n:Nat)(w:ListBool)(s:Source)(r:ListBool),(((\mathrm{parseFuel}\left(n,w\right)=\mathrm{some}\left((s,r)\right))\wedge (\mathrm{parseFuel}\left(n,r\right)=none))\Rightarrow \mathrm{parseFuel}\left(n+1,false::w\right)=none)$$

$$\forall (n:Nat),((\mathrm{parseFuel}\left(n+1,[]\right)=none)\wedge (\mathrm{parseFuel}\left(n+1,[true]\right)=none))$$

Definition 1.3 (Complete Decoder).

$$\forall (w:ListBool),(\mathrm{decode}\left(w\right)=\mathrm{emptyRemainder}\left(\mathrm{parse}\left(w\right)\right))$$

Formalization. D5/S3/Arith/FibonacciAtomic/AtomicPrefixParser.decode (✓ std3).

Source. Repository-derived.

Commentary.

$$decode:ListBool\to OptionSource$$

Here emptyRemainder denotes the mathematical operation defined by the following three cases. Decoding succeeds exactly when the parser consumes the whole input, and then returns the parsed source.

$$emptyRemainder:\mathrm{Option}\left(Source\times ListBool\right)\to OptionSource$$

$$(\mathrm{emptyRemainder}\left(none\right)=none)\wedge (\forall (t:Source),(\mathrm{emptyRemainder}\left(\mathrm{some}\left((t,[])\right)\right)=\mathrm{some}\left(t\right)))\wedge (\forall (t:Source)(b:Bool)(r:ListBool),(\mathrm{emptyRemainder}\left(\mathrm{some}\left((t,b::r)\right)\right)=none))$$

Theorem 1.4 (Exact Parsing and Prefix-Free Coding).

$$(\forall (w:ListBool)(t:Source)(r:ListBool),(\mathrm{parse}\left(w\right)=\mathrm{some}\left((t,r)\right)\iff w=\mathrm{append}\left(\mathrm{code}\left(t\right),r\right)))\wedge (\mathrm{Injective}\left(code\right))\wedge (\mathrm{IsPrefixFree}\left(\mathrm{range}\left(code\right)\right))\wedge (\forall (w:ListBool)(t:Source),(\mathrm{decode}\left(w\right)=\mathrm{some}\left(t\right)\iff w=\mathrm{code}\left(t\right)))$$

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/AtomicPrefixParser.result (✓ std3). ∎

Source. Repository-derived.

Commentary.

The first conjunct is the successful-consumption equivalence for every input, tree, and suffix. Its proof keeps the stronger local induction invariant that any successful fuelled parse consumes exactly one codeword, and the uniform sufficient-fuel invariant that every codeword followed by an arbitrary suffix parses with that suffix unchanged.

The same parser law gives injectivity by applying a local Encoding roundtrip, and gives prefix freedom by parsing one complete codeword in two ways. Full decoding is equivalent to being exactly a codeword; malformed inputs and nonempty suffixes are rejected.

References

• Truth anchor: D5/S3/Arith/FibonacciAtomic/AtomicPrefixParser.code
• Truth anchor: D5/S3/Arith/FibonacciAtomic/AtomicPrefixParser.decode
• Truth anchor: D5/S3/Arith/FibonacciAtomic/AtomicPrefixParser.parse
• Truth anchor: D5/S3/Arith/FibonacciAtomic/AtomicPrefixParser.result
• Dependency: D5/S0/Computability/Coding/PrefixFreeCode
• Dependency: D5/S3/Arith/FibonacciAtomic/GenealogicalFiberTransport