The preorder stack scan in Cobham's class

An expression of C computing, in a single right-to-left pass over a bitstring, the stack depth of the word read as the preorder spelling of a term of RankedAlphabet.Binary.binRanked, together with the scan's liveness verdict. The two are carried in one recursive value, told apart by its head: while no node bit has been read below depth two the value is the depth in unary offset by one, so its head is true; once one has been, the value is [false], which the node step reproduces, that value's two predecessors being empty. Each bit is read once.

The recursion is a boundedRec node, so admissibility requires a bound: the scan's value is never longer than the recursion variable by more than one bit, which the scanner's bound child expresses at growth one. That is the side condition of bounded recursion on notation [Cobham1965], and discharging it is what places the scan in C rather than merely in the syntax sig describes.

The one-test on the scan's predecessor is the recognizer, correct against the Valid predicate of the encoding. Composed with RankedAlphabet.valid_iff_exists_spell, isTreeSem_eq_singleton_iff_exists_spell states that an expression of C accepts exactly the spellings of terms. isTreeSem_eq_ite pins its value on the rejecting branch as well: the two iff statements alone do not imply it, since a recognizer returning [false] rather than [] on a rejected word would satisfy both while disagreeing with isTreeSem_eq_ite there, so the correctness the latter states is a property of the function and not only of the accepted set.

isTree_smashFree places isTree in the subalgebra SmashFree names, [ε, I, s₀, s₁, ∗; COMP, BRN]; with [Strahm2003] Theorem 1(2), deciding RankedAlphabet.Valid at RankedAlphabet.Binary.binRanked is computable simultaneously in polynomial time and linear space.

Main definitions

Cobham.oneAt, Cobham.falseAt — the one-bit strings at an arbitrary arity.

Cobham.inc — prepending true, of arity one.

Cobham.predPred — the argument with two bits dropped, of arity one.

Cobham.combFalseStep, Cobham.combTrueStep — the leaf step and the node step of the scan, of arity one.

Cobham.comb — the stack depth and the underflow verdict in one value, of arity one.

Cobham.eqOneInner — whether the predecessor of the argument is empty, of arity one.

Cobham.eqOne — whether a bitstring has length one, of arity one.

Cobham.isTree — the recognizer, of arity one.

Cobham.combSem, Cobham.eqOneSem, Cobham.isTreeSem — the meaning of the scan, the length test and the recognizer at its arity, over which every statement of the module is stated.

Every expression is given as a raw tree …Raw and as the expression … of C carrying admissibility. The ascription …Of at the reduced arity is given for the scan, the length test and the recognizer, matching the interface BellantoniCook.comb, BellantoniCook.eqOne and BellantoniCook.isTree present, and for an expression whose reduced arity a proof reads.

Main statements

Cobham.combSem_def — the scan's meaning is the scanner's, at the two steps.

Cobham.combSem_nil, Cobham.combSem_cons_false, Cobham.combSem_cons_true — the scan unfolded at each constructor of the recursion variable, with the recursive value exposed.

Cobham.combSem_eq — the scan computes RankedAlphabet.Binary.depth in unary, offset by one, while RankedAlphabet.Binary.ok holds, and [false] once it has failed.

Cobham.length_combSem_le — the recursion bound scan asks for, which comb, combOf and combSem_eq_eval each pass to the scanner.

Cobham.combSem_eq_eval, Cobham.isTreeSem_eq_eval — the meaning read at the raw tree is the meaning the expression of C carries.

Cobham.eqOneSem_env — the one-test at an arbitrary environment is the test at the canonical one.

Cobham.eqOneSem_eq — eqOne accepts exactly the bitstrings of length one.

Cobham.isTreeSem_apply — one step of the recognizer: the one-test on the scan's predecessor.

Cobham.isTreeSem_eq_ite — the recognizer's value on both branches: [true] on a word binRanked's scan accepts and [] on every other.

Cobham.isTreeSem_eq_singleton_iff_valid — isTree accepts exactly the words binRanked's scan accepts.

Cobham.isTreeSem_eq_singleton_iff_exists_spell — equivalently, exactly the spellings of binRanked's terms.

Cobham.isTree_smashFree — the recognizer lies in the subalgebra SmashFree names.

Implementation notes

Each raw tree is named apart from the expression built on it because instance search finds Decidable (sig.WValid w) when w is a constant but not when it is a literal WType.mk application, so decide discharges admissibility only of a named tree. oneAtRaw and falseAtRaw carry a free arity, at which decide does not apply; their admissibility is the pair of an Unit ⊕ Fin m case analysis and the funext that the index condition asks for. The admissibility of an expression embedding pred or cond reuses that expression's own component rather than repeating its proof.

combSem is the meaning read at the raw tree rather than at comb. Cobham.eval asks only for admissibility as a sig-tree, not for the recursion bound, so the scan is characterized by combSem_eq before the expression carrying that bound exists. The bound is then that characterization together with RankedAlphabet.Binary.depth_le_length: the value is [false], of length one, or the depth in unary offset by one, and the depth never exceeds the word length, while the scanner's bound child, at growth one, returns one bit more than the recursion variable. combSem is the scanner's meaning at its arity, and combSem_eq_eval reads it back through C.eval, as isTreeSem_eq_eval does for the recognizer.

That bound is a bound on the value combSem produces at each step, not a bound on the cost of evaluating the expression that computes it: nothing in this module measures a number of reduction steps or an amount of space consumed while doing so. isTree_smashFree states only that isTree avoids the smash generator; the polynomial-time, linear-space reading of that membership is [Strahm2003] Theorem 1(2), cited and not reproved here.

cond and pred are boundedRec nodes in this algebra rather than generators, so a step's meaning reduces only once the value it scrutinizes is in constructor form: combSem_cons_false and combSem_cons_true are therefore not definitional. Each is a corollary of scanSem_cons, proved by rewriting to the step's own application at the recursive value, generalizing that value, and matching on it. The node step's guard drops two bits through two pred nodes, each of which peels a bit only at a literal, so the match reaches the fourth constructor layer of the value.

combSem names the meaning at the reduced arity, so that rewriting under it type-checks. A meaning taken through the Sigma projection instead has a type headed by that projection rather than by an arrow, and rw under it fails as not type-correct at implicit transparency.

eqOne and isTree are comp compositions of pred, cond and comb, carrying no boundedRec node of their own, so each admissibility obligation is discharged by the anonymous constructor pairing the node's own condition, vacuous at a comp, with a case analysis over its children, reusing the embedded subexpression's own RecBounded component rather than repeating its proof. Unlike a primitive predecessor shape, pred here is itself a boundedRec node (predRaw), so its value on the scan's result does not reduce on a symbolic word: isTreeSem_apply is proved by rewriting to the composition's own application, generalizing the scan's value, and matching on it, rather than by rfl.

The meanings this module reads at a raw tree are taken through Cobham.semAt, which names the composite of fst_eval with the tree's arity equation once rather than spelling it at each site.

References

[Cobham1965]

[Strahm2003]

Tags

Cobham, bounded recursion on notation, binary tree, preorder, stack depth, smash-free, polynomial time, linear space

The one-bit string [true] at an arbitrary arity.

The one-bit string [true] as an expression of arity n.

oneAt n at its declared arity.

The one-bit string [false] at an arbitrary arity.

The one-bit string [false] as an expression of arity n.

falseAt n at its declared arity.

Prepend true to the sole argument.

Prepending true, as an expression of arity one.

inc at its declared arity.

The sole argument with two bits dropped. It is empty exactly when the argument is the failure flag, whose two predecessors truncate to the empty bitstring, or a depth below two.

Dropping two bits, as an expression of arity one.

predPred at its declared arity.

The leaf step: push a level onto a live value, whose head is true, and return the failure flag on a value that is empty or has head false. Of arity one, the state being the sole argument a fold's step reads.

The leaf step as an expression of arity one.

combFalseStep at its declared arity.

The node step: pop a level when at least two remain, and return the failure flag otherwise. An existing failure propagates, its guard being empty. Of arity one, as combFalseStep.

The node step as an expression of arity one.

combTrueStep at its declared arity.

The raw tree of the scan, as a scanner: base [true], the empty bitstring having depth zero and satisfying RankedAlphabet.Binary.ok; growth one, the value being never longer than the recursion variable by more than one bit.

The scan's meaning at its arity, as the scanner's. Cobham.eval asks only for admissibility as a sig-tree, so the scan is characterized before the expression carrying its recursion bound exists.

The scan is the scanner at its two steps. Stated because a def carries no equation lemma: the cons lemmas rewrite by it, and length_combSem_le rewrites by it in reverse, its statement being the one scan asks for.

The scan's value on the empty bitstring: depth zero, offset by one.

A leaf bit pushes a level onto a live value, and is absorbed by a failure.

A node bit pops a level when at least two remain, and fails otherwise. The guard is the value with two bits dropped, so a failure, whose two predecessors are empty, propagates.