The fold scan of a preorder spelling

RankedAlphabet.scanStep reads a preorder spelling right to left, carrying an incomplete block, a count of pending subterms and a liveness flag. At a completed block the symbol pops its arity from the count and pushes one, so the count is the height of a stack whose entries carry no data.

This module replaces that count by a stack of values of an arbitrary carrier and the pop-push by an application of an algebra of the ranked alphabet. toScan projects the resulting state onto RankedAlphabet.Scan by taking the stack's length, and toScan_foldScanStep shows the projection is a step homomorphism at every carrier and every algebra: the validity scan is the image of the fold scan under the terminal map, not a separate construction.

foldOut reads the final state as an Option, absent exactly where the word spells no term, and foldOut_eq identifies it with RankedAlphabet.parse followed by the fold. R.Term is the initial algebra of the alphabet, so that fold is the unique algebra morphism out of it.

Main definitions

Geb.CobhamFold.symOf — the symbol a block denotes, refining RankedAlphabet.arOf, which returns only its arity.

Geb.CobhamFold.Term.fold — the unique algebra morphism out of the term algebra.

Geb.CobhamFold.FoldScan — the fold scan's state.

Geb.CobhamFold.foldScanStep, Geb.CobhamFold.foldScanFrom, Geb.CobhamFold.foldScanFinal — one step, the scan from a state, and the scan from the initial state.

Geb.CobhamFold.toScan — the projection onto RankedAlphabet.Scan.

Geb.CobhamFold.foldOut — the final state read as an Option.

Main statements

Geb.CobhamFold.arOf_eq_map_symOf — RankedAlphabet.arOf is symOf followed by the arity.

Geb.CobhamFold.toScan_foldScanStep, Geb.CobhamFold.toScan_foldScanFinal — the projection is a step homomorphism, and carries the whole scan.

Geb.CobhamFold.mem_stack_foldScanFinal — every value on the scan's stack is one the algebra produced.

Geb.CobhamFold.foldScanFrom_code — a completed block pops its arity's worth of stack and pushes the algebra applied to them.

Geb.CobhamFold.foldScanFrom_ofFn — a family of spellings pushes one value each, in index order.

Geb.CobhamFold.foldScanFrom_spell — a spelling pushes one value, the fold of the term it spells.

Geb.CobhamFold.Term.fold_unique — the term algebra is initial, so Term.fold is the algebra morphism out of it rather than one of several.

Geb.CobhamFold.Term.fold_map, Geb.CobhamFold.foldOut_map — fold fusion, and the agreement of two folds at different carriers whose algebras commute with a map.

Geb.CobhamFold.foldOut_eq — the fold scan computes RankedAlphabet.parse followed by Term.fold.

Geb.CobhamFold.buf_foldScanFinal, Geb.CobhamFold.length_stack_foldScanFinal, Geb.CobhamFold.length_buf_foldScanFinal_lt — the projection's consequences for the incomplete block and the stack's height, which every state layout over this scan consumes.

Geb.CobhamFold.width_mul_depth_add_length_buf_scanFinal_le — the sharper bound on the pending count: the alphabet's width times the count, plus the incomplete block, is at most the word's length.

Geb.CobhamFold.width_mul_depth_scanFinal_le — its corollary dropping the incomplete block, R.width * depth ≤ |w|.

Implementation notes

The stack's head is the value of the term spelled immediately to the right of the symbol being read, which is that symbol's child zero: scanning right to left, RankedAlphabet.scanFrom_append reads the later part of a word first, so within a symbol's children the last one scanned — and so the one pushed last — is child zero. foldScanStep therefore indexes the algebra's argument by position in the stack directly.

foldScanStep branches by dite where RankedAlphabet.scanStep branches by a match on decide: the arity branch needs the comparison's proof to index the stack, which a match on a Bool does not supply.

symOf is what RankedAlphabet.arOf would be if the scan needed the symbol rather than its arity; arOf_eq_map_symOf is what makes the two scans branch alike, and so what toScan_foldScanStep rests on.

width_mul_depth_add_length_buf_scanFinal_le sharpens RankedAlphabet.depth_scanFinal_le_length by the alphabet's width. The pending count rises only at a completed block, so it counts symbols rather than bits. The invariant carries the incomplete block's length because a partial block is progress toward the next increment; without that summand the induction does not close at the completing step. omega treats the products as atoms, so the completing step supplies the two linear facts relating them.

References

[GambinoHyland2004]

Tags

ranked alphabet, preorder, scan, fold, catamorphism, initial algebra

The symbol a block denotes, absent at a block denoting none. RankedAlphabet.arOf returns that symbol's arity; a fold needs the symbol itself, to select the algebra's operation.

The arity of a block's symbol is the arity of what symOf returns, so the validity scan and the fold scan take the same branch at every block.

A block denotes the symbol it spells.

The unique algebra morphism out of the term algebra: the fold of a term at an algebra of the ranked alphabet. RankedAlphabet.Term is that alphabet's W-type, so the morphism is its eliminator.

The fold on a term, in the RankedAlphabet.Term.mk presentation.

The term algebra is initial: a map commuting with the algebra is the fold, so Term.fold is the algebra morphism out of it rather than one of several. RankedAlphabet.Term is a WType, so this is WType.elim_unique at the alphabet's shape and direction families, read at a point; the initiality it expresses is [GambinoHyland2004]'s for polynomial functors.

Fold fusion: a map commuting with two algebras carries one fold to the other. A corollary of initiality, and the statement that identifies the results of two fold constructions at different carriers.

The state of the fold scan: the bits of an incomplete block, the stack of values of the subterms already scanned, and whether the scan has failed. RankedAlphabet.Scan is this state with the stack replaced by its length.

The bits of an incomplete block, most recently read first.

The values of the subterms already scanned, the most recently completed first.

Whether the scan has not yet failed.

The projection onto the validity scan's state: the stack's length is the pending count.

One step of the fold scan, reading one bit. A failed state absorbs. An incomplete block takes the bit; a complete one is decoded, and its symbol pops its arity's worth of stack, applies the algebra to them and pushes the result, failing when the block spells no symbol or the stack is short of the arity.

The projection is a step homomorphism: the validity scan is the fold scan at every carrier and every algebra, read through the stack's length.