The fold over recognized terms as an expression of Cobham's class

The fold scan of Geb/Prototypes/Computability/CobhamFoldProto/Fold.lean, laid out as a bitstring by Geb/Prototypes/Computability/CobhamFoldProto/Layout.lean, carried by the scan combinator of Geb/Prototypes/Computability/CobhamFoldProto/Bound.lean, and composed with a readout into an expression computing RankedAlphabet.parse followed by the fold.

At p = 0 and the carrier Unit this construction meets the recognizer of Geb/Mathlib/Computability/Cobham/RankedTree.lean; the module Geb/Prototypes/Computability/CobhamFoldProto/Degenerate.lean identifies the state layout, the dispatch window, the readout window and the step, and the two accept the same language. They are not the same expression. The raw trees differ — Geb.CobhamFold.boundMulRaw_ne_boundRaw separates the two bound children at multiplicity one, at every growth — and the rejecting words differ, this module's outWord spelling both branches at the width p + 1 where Cobham.isRankedSem_eq_ite gives the empty bitstring.

Main definitions

Geb.CobhamFold.foldStepF — one step of the scan, as an expression of arity one.

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

Geb.CobhamFold.foldSemF — the meaning of the scan.

Geb.CobhamFold.foldExprF, Geb.CobhamFold.foldExprOfF — the scan as an expression of Cobham.C, and at its declared arity.

Geb.CobhamFold.readoutWidth, Geb.CobhamFold.outWord, Geb.CobhamFold.readState, Geb.CobhamFold.readOf — the readout's window, its output word, the Option it reads off the window, and the readout as an expression.

Geb.CobhamFold.foldOutOf, Geb.CobhamFold.foldOutExpr, Geb.CobhamFold.foldOutSem — the readout composed onto the scan by Geb.CobhamFold.comp1Of.

Main statements

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

Geb.CobhamFold.foldSemF_eq — the expression computes the fold scan's state word on every input.

Geb.CobhamFold.length_foldSemF_le — the recursion bound the scan combinator asks for, at a multiplier covering one stack entry per symbol block.

Geb.CobhamFold.length_outWord, Geb.CobhamFold.headD_outWord, Geb.CobhamFold.bits_tail_outWord — the output's width, the marker separating its two branches, and the recoverability of the value.

Geb.CobhamFold.stepWord_readOf — the readout's value at the state it reads.

Geb.CobhamFold.foldOutSem_eq — the composition computes Geb.CobhamFold.foldOut, spelled by outWord.

Geb.CobhamFold.foldOutSem_eq_parse — the same value read as RankedAlphabet.parse followed by the algebra morphism.

Geb.CobhamFold.foldSemF_eq_eval, Geb.CobhamFold.foldOutSem_eq_eval — the meanings read at the raw trees are the meanings the expressions carry.

Implementation notes

The multiplier is a parameter constrained by p + 1 ≤ mult * R.width, rather than fixed at p + 1. The state carries one (p + 1)-bit entry per pending subterm and the pending count rises once per R.width input bits — that is Geb.CobhamFold.width_mul_depth_scanFinal_le — so any multiplier meeting the inequality bounds the state. mult = p + 1 always meets it, RankedAlphabet.width_pos giving 1 ≤ R.width; a wide alphabet admits a smaller one.

The readout reads two stack entries: one to carry the value, and one more whose marker distinguishes a stack of exactly one entry from a longer one. That is the Cobham.acceptWord R ++ [false] of the recognizer's verdict test, one entry wide rather than one bit wide.

outWord spells none as a false marker followed by p false bits, so both branches have the width p + 1, and the marker alone separates them. A rejected word receives that word rather than merely something other than an accepted one, which is the discipline Cobham.isRankedSem_eq_ite records.

readState tests the decoded state's three fields rather than matching on its stack: a match whose pattern fixes the stack's length does not reduce at a variable stack.

References

[Cobham1965]

Tags

Cobham, bounded recursion on notation, ranked alphabet, fold, catamorphism

One step of the fold expression: dispatch on the state's leading bits, prepend the rebuilt prefix and drop the consumed bits. Every branch has that one shape.

A step of the expression computes a step of the fold scan, on a state whose incomplete block is short of the width. This is where the decoder, the two truncation lemmas and the step lemma meet.

The growth the state layout's fixed part contributes: the flag and the slot.

The fold expression's scan, at the two steps and the multiplicative bound.

The expression computes the fold scan's state word on every input.