Self-delimiting bitstrings in Cobham's class

A stack whose entries are bitstrings of varying length needs entries that delimit themselves, and a step that reads one needs to parse it. This module supplies the parsing primitives as expressions of Cobham's class.

An entry spelling the payload u is List.replicate u.length true followed by false followed by u: a unary length prefix, read from the list's head, which is the end a step of the outer scan pops from.

Cobham.scan lifts steps of arity one, applying them to the recursive value alone. dropUnaryOf, dropEntryOf and takeEntryOf need the remaining word as well, which Cobham.evalRec supplies in slot zero of a step's environment, so scan2 takes its steps at arity two directly.

takeEntryOf is the one whose use of it is least avoidable. Its recursion appends a bit at the end of the payload accumulated so far, which is not a head operation; the concat generator supplies the append, and the appended bit is read off the remaining word by firstBitOf after dropEntryOf. Without slot zero the payload would not be extractable and the algebra could not be applied.

Main definitions

Geb.CobhamFold.scan2 — the arity-two scan node as an expression; Geb.CobhamFold.scan2Raw itself lives with the scan combinators in Geb/Prototypes/Computability/CobhamFoldProto/Bound.lean.

Geb.CobhamFold.entryWord — the self-delimiting spelling of a payload.

Geb.CobhamFold.firstBitOf, Geb.CobhamFold.unaryOf, Geb.CobhamFold.takeUnaryOf, Geb.CobhamFold.dropUnaryOf, Geb.CobhamFold.dropEntryOf, Geb.CobhamFold.takeEntryOf — the parsing primitives.

Geb.CobhamFold.idOf, Geb.CobhamFold.dropEntriesOf, Geb.CobhamFold.entryOf — the identity, and the primitives iterated to reach the j-th entry. The composition combinators they are built from live in Geb/Prototypes/Computability/CobhamFoldProto/Bound.lean.

Main statements

Geb.CobhamFold.scan2Sem_nil, Geb.CobhamFold.scan2Sem_cons — the arity-two scan on the empty word and on one bit.

Geb.CobhamFold.stepWord_firstBitOf, Geb.CobhamFold.stepWord_unaryOf, Geb.CobhamFold.stepWord_takeUnaryOf, Geb.CobhamFold.stepWord_dropUnaryOf, Geb.CobhamFold.stepWord_dropEntryOf, Geb.CobhamFold.stepWord_takeEntryOf — what each primitive computes.

Geb.CobhamFold.take_succ_append_take_one — a truncation splits at its last bit.

Geb.CobhamFold.takeEntrySem_entryWord, Geb.CobhamFold.dropEntrySem_entryWord — the payload and the remainder of a self-delimiting entry.

Geb.CobhamFold.two_mul_length_takeEntrySem_add_length_dropEntrySem_le — the payload counted twice and the remainder fit inside the word.

Geb.CobhamFold.scan2Sem_eq_eval — the meaning read at the raw tree is the meaning the expression carries.

Implementation notes

Every primitive's value is no longer than its argument, so each takes Cobham.boundRaw 0 as its bound child: the recursion variable itself dominates. The bounds are established over arbitrary words, not only over well-formed entries, since Cobham.RecBoundedValue quantifies over every environment.

Each primitive recurses over the whole word, not over the entry it reads. Cobham.evalRec recurses to the empty word whatever the value depends on, so dropEntryOf touches every bit of its argument although, at an entry spelling the payload u, the first 2 * u.length + 1 bits are what fix where its value starts. Their steps are not constant either: dropEntryOf's applies Cobham.pred, itself a boundedRec, and takeEntryOf's runs a fresh dropEntryOf over the remaining word, so counting a boundedRec's cost as the sum over its levels of its step's cost makes dropEntryOf quadratic in its argument and takeEntryOf cubic.

Nothing here measures a number of reduction steps, as Geb/Mathlib/Computability/Cobham/Tree.lean records of its own subject; the paragraph above analyses the expression under one cost model.

The accompanying lower bound rests only on the class's shape rather than on a cost model: reading an unbounded field of the state requires a recursion over the state, boundedRec being the class's only recursion. It is an argument about the expression, not a theorem stated here.

That gives a dichotomy rather than a spectrum, in what a step reads rather than in what it costs. A carrier whose values are bounded by a constant is the fixed-width case — pad to that constant and dispatch on a constant window, and no step reads an unbounded field. A carrier whose values are unbounded needs entries of this shape, and every step reads one. There is no intermediate regime, a bound of any constant B being the fixed-width case at width B. Neither case has constant-time steps: reading even a bounded prefix of the state goes through a boundedRec over the state.

Only boundedRec nodes carry a Cobham.RecBoundedValue obligation, comp's being vacuous, so composing these primitives imposes no further bound. This is why entryWord's spelling, which is longer than its argument, needs no growth allowance: it is a composition, not a recursion.

References

[Cobham1965]

Tags

Cobham, bounded recursion on notation, self-delimiting, prefix code

The arity-two scan node over expressions, carrying its admissibility.

The arity-two scan node's arity.

The meaning of the arity-two scan at its arity.

The word an arity-two step contributes at the remaining word and the recursive value.

The arity-two scan on the empty bitstring is its base's word.

One step of the arity-two scan, which reads the remaining word as well as the value the scan of that word returns.

The arity-two scan as an expression of the class, its recursion bounded by the recursion variable itself.

scan2 at its declared arity.

The meaning read at the raw tree is the meaning the expression carries.

Prepending a word prepends it to what an arity-two step contributes.

A constant arity-two step contributes its word, whatever it reads.

A projection contributes the slot it names.

A composition contributes its head's value at its argument's.

A concatenation contributes its second argument's value followed by its first's.

The predecessor's value at an arity-one step.

The first bit of a word, absent at the empty word.

What the first-bit primitive computes.