The generic ranked recognizer

The validity scan of Geb/Mathlib/Data/Tree/Ranked/Preorder.lean, at an arbitrary ranked alphabet, composed with a verdict test into a recognizer, as an expression of Cobham's class.

Main definitions

Cobham.bufBits — the incomplete block in a slot of the alphabet's width.

Cobham.stateWord — the scan state as a bitstring.

Cobham.dispatchWidth — the number of state bits a step dispatches on.

Cobham.decodeState — the inverse of the state layout.

Cobham.dropCount, Cobham.nextPrefix — the bits a step drops and prepends.

Cobham.rankedStep, Cobham.rankedSem — the recognizer's step and the meaning of its scan.

Cobham.ranked, Cobham.rankedOf — the scan as an expression of C, and at its declared arity.

Cobham.acceptWord, Cobham.acceptTest — the accepting state's word and the test deciding it.

Cobham.isRankedRaw, Cobham.isRanked, Cobham.isRankedOf, Cobham.isRankedSem — the recognizer's raw tree, the expression of C over it, that expression at its declared arity, and its meaning.

Main statements

Cobham.length_bufBits_of_lt, Cobham.length_stateWord_of_lt — the slot's and the state word's lengths.

Cobham.dropWhile_bufBits — the slot past its padding.

Cobham.ofFn_bits_stateWord — the state word truncated to a window and zero-padded.

Cobham.decodeState_stateWord_of_lt — the decoder inverts the layout up to capping the pending count at the depth window.

Cobham.dropCount_min_depth, Cobham.nextPrefix_min_depth — capping the pending count at the depth window changes neither.

Cobham.stateWord_scanStep_of_lt — a step rewrites a bounded prefix and drops a bounded number of bits.

Cobham.stepWord_rankedStep_of_lt, Cobham.rankedSem_eq — the expression computes the scan, one step and then on every input.

Cobham.length_rankedSem_le — the recursion bound the scanner asks for.

Cobham.rankedSem_eq_eval — the meaning read at the raw tree is the meaning the expression carries.

Cobham.ofFn_bits_stateWord_eq_iff — the verdict window separates the accepting state from every other reachable one.

Cobham.stepWord_acceptTest — the test's value at the state it reads.

Cobham.wValid_isRankedRaw — the raw tree's admissibility, from its two components'.

Cobham.isRankedSem_apply, Cobham.isRankedSem_eq_ite — the composition's value, and the value on both branches.

Cobham.isRankedSem_eq_singleton_iff_valid — the recognizer accepts exactly the words spelling a term.

Cobham.isRankedSem_eq_eval — the meaning read at the raw tree is the meaning the expression carries.

Cobham.isRankedSem_binRanked_eq_singleton_iff_isTreeSem — at the two-symbol alphabet it accepts the language Cobham.isTree accepts.

Implementation notes

RankedAlphabet.Scan carries an incomplete block, a count of pending subterms, and a liveness flag. The count is unbounded and the other two are not, and an expression of the class reaches only a bounded prefix of a word, so the count is the tail and the layout admits no alternative.

The block cannot be delimited by its own length, since the fields after it would then stand at a position not statically known. It occupies a slot of exactly R.width bits, delimited by a true sentinel preceded by false padding: reading from offset one, past the flag, the first true is the sentinel and the block is what follows it, the padding being all false. The slot's length is invariant under accumulation — the padding shrinks as the block grows — which is why the fields after it never move. This costs R.width bits rather than the 2 * R.width a separate fill counter would.

length_bufBits_of_lt's hypothesis is consumed rather than decorative. Nat subtraction being truncated, a block of length R.width or more yields a slot of length one past the block, and stateWord is then not injective: at R.width = 2 the states ⟨[false, true], 0, true⟩ and ⟨[false], 1, true⟩ share the word [true, true, false, true]. The invariant excluding this is RankedAlphabet.length_buf_scanFinal_lt.

The pending count is unary. Binary would need a truncated subtraction definable in the class, and Cobham/Tree.lean's recognizer represents its own depth in unary already.

ofFn_bits_stateWord is stated at an arbitrary window, the dispatch and the verdict reading different ones.

The branch family's domain is Fin (dispatchWidth R) → Bool at a symbolic width, so recovering the fields index by index would carry a bound proof at every step. decodeState avoids that by passing through List.ofFn and reading the fields with the List API. This also keeps the module clear of DecidableEq (Fin n → Bool), which resolves through Fintype.decidablePiFintype, measured as depending on Classical.choice, while DecidableEq (List Bool) measures clean.

The run of false past the slot is cleared by a two-case reduction rather than by List.takeWhile_replicate, which was measured to depend on Classical.choice through List.filter_replicate. A proof shortened back onto that lemma fails lake lint.

The dispatch reads the flag and the slot together with the low R.maxArity + 1 bits of the pending count, which give min depth (R.maxArity + 1). Those bits decide r ≤ depth for every symbol: if the count is at least R.maxArity + 1 then every arity is below it, and otherwise those bits are the count itself. RankedAlphabet.le_maxArity_of_arOf_eq_some is what makes the window sufficient, and it is what dropCount_min_depth and nextPrefix_min_depth consume.

Neither SmashFree (ranked R) nor SmashFree (isRanked R) is stated here. smashFreeBool is a WType.elim over the whole tree, so at a symbolic alphabet it is not decide-dischargeable and needs a recursion mirroring wValid_casesRaw, and at a concrete alphabet it forces every node. Nothing in this module uses smash, so the statement is expected to hold and is left to the branch that needs it. Cobham/Tree.lean keeps comb and isTree, so isTree_smashFree and the [Strahm2003] Theorem 1(2) reasoning keep their subject.

No equivalence here is discharged by omega, which pulls Classical.choice on an Iff goal; each is built from its two implications or from Iff.trans.

isRankedSem_eq_ite pins the value on the rejecting branch as well as the accepting one. isRankedSem_eq_singleton_iff_valid alone would admit a recognizer returning [false] on a rejected word, so correctness as a function is not implied by correctness of the accepted set.

The containment this module realizes is an instance of Cobham's characterisation of the polynomial-time functions; what it delivers is an explicit expression computing the decision, not a new theorem.

References

[Cobham1965]

[Strahm2003]

Tags

Cobham, bounded recursion on notation, ranked alphabet, preorder, scan, recognizer

The incomplete block in a slot of the alphabet's width: false padding, a true sentinel, then the block.

The scan state as a bitstring: the liveness flag, the block slot, then the pending count in unary.

The number of state bits a step dispatches on: the flag, the slot, and enough of the pending count to decide r ≤ depth for every arity r.

The slot holds the alphabet's width, the padding shrinking as the block grows. Nat subtraction being truncated, the hypothesis is consumed.

The state word's length: the flag, the slot, and the pending count.

The slot past its padding is the sentinel followed by the block.

The state word truncated to a window past the slot and zero-padded: the flag, the slot, and the pending count capped at the window. Stated at an arbitrary window, the dispatch and the verdict reading different ones.

The inverse of the state layout, read off List.ofFn of the bit family: the flag is the head, the block is the slot past its padding and sentinel, and the pending count is the run of true that follows the slot. Every operation is structural, so no Fin arithmetic and no Fintype-derived decidability arises.

The decoder inverts the layout, up to capping the pending count at the depth window R.maxArity + 1.