The fold at a bitstring carrier

Geb/Prototypes/Computability/CobhamFoldProto/Expr.lean folds at a carrier with a fixed-width bit encoding, dispatching each step on a constant window that holds the whole stack the step reads. This module folds at the carrier List Bool with the algebra's operations supplied as expressions of Cobham's class, so the carrier is unrestricted and the algebra is whatever the class can define.

Main definitions

Geb.CobhamFold.stackWordV, Geb.CobhamFold.stateWordV — the stack and the state as bitstrings.

Geb.CobhamFold.stackSize — the total length of the pending values.

Geb.CobhamFold.entryWordOf, Geb.CobhamFold.applyAlgOf, Geb.CobhamFold.newStackOf, Geb.CobhamFold.rebuildOf — the step's stack rewrite, as expressions.

Geb.CobhamFold.branchV, Geb.CobhamFold.foldStepV — one step of the fold.

Geb.CobhamFold.decodeVAt — the inverse of the layout at a window.

Geb.CobhamFold.foldGrowthV — the growth the state layout's fixed part contributes.

Geb.CobhamFold.foldSemV, Geb.CobhamFold.foldExprV, Geb.CobhamFold.foldExprOfV — the scan, and the scan as a member of Cobham.C.

Geb.CobhamFold.readoutWidthV, Geb.CobhamFold.outWordV, Geb.CobhamFold.readOfV — the readout's window, its output word, and the readout as an expression.

Geb.CobhamFold.foldOutOfV, Geb.CobhamFold.foldOutExprV, Geb.CobhamFold.foldOutSemV — the readout composed onto the scan by Geb.CobhamFold.comp1Of.

Geb.CobhamFold.algOfFixed — a fixed-width carrier's algebra transported here.

Main statements

Geb.CobhamFold.stackWordV_cons, Geb.CobhamFold.length_stackWordV — the stack's layout and its length.

Geb.CobhamFold.stepWord_dropEntriesOf_stackWordV, Geb.CobhamFold.stepWord_entryOf_stackWordV — the primitives read the stack.

Geb.CobhamFold.stepWord_dropEntriesOf_stackWordV_append, Geb.CobhamFold.stepWord_entryOf_stackWordV_append — the same two reads at a stack layout followed by an arbitrary remainder, which each need the count to be within the stack.

Geb.CobhamFold.decodeState_stateWordV — the dispatch window decodes the flag, the block and the count capped at the window.

Geb.CobhamFold.stepWord_foldStepV — a step of the expression computes a step of the fold scan.

Geb.CobhamFold.foldSemV_eq, Geb.CobhamFold.length_foldSemV_le — the expression computes the fold scan's state word, and the recursion bound it satisfies under the linear-growth hypothesis.

Geb.CobhamFold.stepWord_readOfV — the readout's value at a state word.

Geb.CobhamFold.length_fold_le_of_growth — an algebra lengthening by at most a constant per symbol folds a term to a value linear in its node count.

Geb.CobhamFold.potential_foldScanStep_le, Geb.CobhamFold.potential_foldScanFinal_le, Geb.CobhamFold.stackSize_le_of_growth — the same condition bounds the scan's potential R.width * stackSize + c * |buf|, and so discharges the linear-growth hypothesis length_foldSemV_le takes.

Geb.CobhamFold.potential_foldScanStep_le_of_invariant, Geb.CobhamFold.potential_foldScanFinal_le_of_invariant, Geb.CobhamFold.stackSize_le_of_growth_of_invariant — the same three with the growth condition assumed only of values satisfying a predicate the scan's stack carries, which an algebra duplicating its children's payloads needs; the unrestricted forms are these at the trivial predicate.

Geb.CobhamFold.foldOutSemV_eq — the expression computes Geb.CobhamFold.foldOut, spelled by outWordV; with foldOut_eq this is RankedAlphabet.parse followed by the algebra morphism.

Geb.CobhamFold.foldOut_algOfFixed — at an algebra whose carrier stays within a fixed width, the fold this construction computes and the one the fixed-width construction computes agree, up to the encoding. It is a statement about the two algebras at the shared semantic layer, which each construction is separately proved to compute (foldOutSemV_eq here, foldOutSem_eq there).

Geb.CobhamFold.foldSemV_eq_eval, Geb.CobhamFold.foldOutSemV_eq_eval — the meanings read at the raw trees are the meanings the expressions carry.

Implementation notes

Names here carry a V suffix where their fixed-width counterparts in Geb/Prototypes/Computability/CobhamFoldProto/Layout.lean and Geb/Prototypes/Computability/CobhamFoldProto/Expr.lean carry an F or, where the fixed-width name came first, no suffix at all: the two constructions define the same notions at a variable-width and at a fixed-width carrier, and the suffix is what keeps them apart in one namespace.

The state layout

stateWordV R s = stateWord R (toScan s) ++ false :: stackWordV s.stack

The state word is the recognizer's — the liveness flag, the block slot, and the pending count in unary — followed by a false sentinel and the stack, whose entries are Geb.CobhamFold.entryWord's self-delimiting spellings.

Two consequences. The pending count stays inside a constant dispatch window, so the test R.arity i ≤ depth is still a bounded one and the branch family is Cobham.dispatchWidth R wide — the recognizer's own width, independent of the carrier. And the sentinel is required: an entry begins with its length in unary, so without a false between the count and the stack the decoder's takeWhile would run out of the count and into the first entry's prefix.

Cost

Each primitive the step reads the stack with is itself a recursion whose step is not constant. Geb.CobhamFold.dropEntryOf's step applies Cobham.pred, itself a boundedRec; Geb.CobhamFold.takeEntryOf's step runs a fresh dropEntryOf over the remaining word. Counting a boundedRec's cost as the sum over its levels of its step's cost, dropEntryOf is quadratic in its argument and takeEntryOf cubic, so a fold's state-reading here is polynomial of a degree above two rather than quadratic.

Nothing here measures a number of reduction steps, as Geb/Mathlib/Computability/Cobham/Tree.lean records of its own subject; the paragraph above is an analysis of the expression under one cost model, and a machine evaluating it is not obliged to follow that 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, so no step reading such a field is constant. It bears on this layout, whose steps do read one; it does not exclude some other expression computing the same fold without reading an unbounded field. It is an argument about the expression, not a theorem stated here.

The algebra is an arbitrary member of the class and so carries whatever cost the class admits, putting a fold above its algebra by whatever the state-reading costs. The state-reading is therefore not what limits a fold: any cost the class admits at all is reached by spending it inside the algebra. How far that goes is a question about the class, not about this construction, and it is not settled here — only the left-to-right inclusion of [Strahm2003] Theorem 1(2) is relied on anywhere in this repository, and docs/references.bib records that the equality fails read literally.

Space is what binds. The state holds every pending value, so a linear-space reading forces a constant c bounding the pending values' total length by c * n, which is the hypothesis Geb.CobhamFold.length_foldSemV_le takes. That hypothesis is not an artifact of this construction: [Clote1999]'s arithmetic analogue reads its class as one of functions of linear growth.

The dispatch is no wider here than at a fixed-width carrier, and narrower at every positive carrier width; at p = 0 the two coincide, which Geb.CobhamFold.dispatchWidthF_zero states. The fixed-width dispatch reads the stack, so its branch family is 2 ^ (1 + R.width + (p + 1) * (R.maxArity + 1)); here it reads only the flag, the slot and the count, so the family is 2 ^ Cobham.dispatchWidth R whatever the carrier. This is a statement about the branch family alone: the completing branch here carries a rebuildOf subtree no fixed-width branch does, and the two expressions' sizes are not compared.

References

[Clote1999]

[Cobham1965]

[Strahm2003]

Tags

Cobham, bounded recursion on notation, fold, self-delimiting, bitstring carrier

The stack as a bitstring: the self-delimiting spelling of each entry, the top entry first.

The empty stack's layout.

The stack's layout, one entry at a time.

The total length of the pending values.

The empty stack's values are empty.

The pending values' total length, one entry at a time.

The stack's layout is twice the pending values' total length plus one bit per entry.

The state as a bitstring: the recognizer's state word, a false sentinel, then the stack.

The state word's length.

Dropping whole entries from the stack's layout drops whole entries from the stack.

The j-th entry primitive reads the j-th pending value.

Dropping as many entries as a stack layout holds leaves what follows it. Geb.CobhamFold.stepWord_dropEntriesOf_stackWordV is this at the empty remainder, where the hypothesis is unnecessary.