Expression combinators and the scan at a linear growth bound

Cobham.scan admits a state exceeding the input by an additive constant: its bound child prepends growth bits to the recursion variable, so the recursion bound reads |state| ≤ |w| + growth. A fold whose state carries one (p + 1)-bit block per pending subterm can exceed that, the block count rising once per R.width input bits. R.width < p + 1 is necessary for it to do so, not sufficient: an alphabet whose symbols never grow the stack keeps the state bounded whatever the carrier. At R.width ≥ p + 1 the additive bound always suffices, and Geb.CobhamFold.length_stateWordF_not_le_add exhibits the failure at the two-symbol alphabet, whose width is one.

This module supplies the bound child boundMulRaw, built over multRaw, whose value is the mult-fold self-concatenation of the recursion variable, and the scan combinator scanBRaw parameterized by its bound child, so that Cobham.scan's additive bound and the multiplicative bound mult * |w| + growth are two instances of one node. It also supplies the general expression combinators — a projection, two compositions and a concatenation — and the scan node scan2Raw at steps of arity two. Both fold constructions over this one reach scan2Raw, through scanBRaw, and the fixed-width one uses comp1Of besides; the projection, the general composition and the concatenation reach the bitstring construction alone.

The multiplier is built from Cobham.concatCompRaw, whose head is the concat generator. concat belongs to the subalgebra Cobham.SmashFree names, which [Strahm2003] Theorem 1(2) contains in the functions computable simultaneously in polynomial time and linear space, so the multiplicative bound stays inside that subalgebra; Geb.CobhamFold.smashFreeBool_boundMulRaw states this at every multiplicity and growth. Cobham.cond already takes a concatenation bound in place of [HeraudNowak2011]'s smash bound for the same reason.

Main definitions

Geb.CobhamFold.projOf, Geb.CobhamFold.compOf, Geb.CobhamFold.comp1Of, Geb.CobhamFold.concatCompOf — a projection, a composition, an arity-one expression applied to an expression, and a concatenation, as expressions.

Geb.CobhamFold.multRaw — the mult-fold self-concatenation of the recursion variable.

Geb.CobhamFold.boundMulRaw — that concatenation with growth bits prepended.

Geb.CobhamFold.scan2Raw — the scan node at steps of arity two, which read the remaining word as well as the recursive value.

Geb.CobhamFold.scanBRaw, Geb.CobhamFold.scanBW — that node at two steps lifted from arity one, which is Cobham.scan's shape, and it over expressions.

Geb.CobhamFold.scanBSem — the meaning of that node at arity one.

Geb.CobhamFold.scanMul, Geb.CobhamFold.scanMulOf — the scan at the multiplicative bound, as an expression of Cobham.C and at its declared arity.

Main statements

Geb.CobhamFold.wValid_concatCompRaw, Geb.CobhamFold.recBounded_concatCompRaw — admissibility and the recursion bound of a concatenation node, from its two arguments'.

Geb.CobhamFold.length_multSem — the multiplier's value has length mult * |x 0|, exactly.

Geb.CobhamFold.length_boundMulSem — the bound child's value has length growth + mult * |x 0|.

Geb.CobhamFold.scanBRaw_boundRaw — at the additive bound child the parameterized node is Cobham.scanRaw.

Geb.CobhamFold.boundMulRaw_ne_boundRaw — at the multiplier one, the multiplicative bound child is not the additive one, at any growth.

Geb.CobhamFold.scanBSem_nil, Geb.CobhamFold.scanBSem_cons, Geb.CobhamFold.scanBSem_eq — the scan on the empty word, on one bit, and as a List.foldr, at every bound child.

Geb.CobhamFold.scanMulSem_eq_eval — the meaning read at the raw tree is the meaning the expression carries.

Implementation notes

Cobham.concatCompRaw n a b evaluates to b's list followed by a's, the concat generator reading its second argument as the earlier part of the word. multRaw's step therefore places the projection second, so the recursion variable is prepended at each level; the value is a concatenation of copies of one list, so the order is immaterial and only length_multSem is stated.

scanBRaw differs from Cobham.scanRaw only in taking its bound child as a parameter rather than building it from a growth. Every statement about the scan's value — scanBSem_nil, scanBSem_cons, scanBSem_eq — holds at every bound child, Cobham.evalValue's boundedRec clause not consulting child three; only the recursion bound reads it.

The transports Cobham.semAt introduces disappear here by proof irrelevance: each raw tree whose meaning is read here is a WType.mk whose shape's Cobham.q reduces to 1, so the arity equation has definitionally equal sides.

References

[Cobham1965]

[HeraudNowak2011]

[Strahm2003]

Tags

Cobham, bounded recursion on notation, scan, composition, concatenation, growth bound

A projection as an expression.

An m-ary expression applied to m arguments of arity n.

An arity-one expression applied to an n-ary one: compOf at one argument.

The concatenation of two n-ary expressions, the second's value first: compOf at the concat generator.

A concatenation node is admissible when both its arguments are, at the node's own arity. Its head is the concat generator, whose admissibility is vacuous.

A concatenation node carries no recursion of its own: its comp shape's Cobham.RecBoundedValue is vacuous, so the condition is its arguments'.

Prepending a word to an expression prepends it to the expression's meaning, at every arity. Cobham.stepWord_prependOf is this at arity one.

A constant word's meaning, at every arity.

A projection's meaning is the slot it names.

A concatenation's meaning is its second argument's followed by its first's.

A composition's meaning at every arity. Geb.CobhamFold.stepWord_compOf is this at arity one.

An arity-one expression's meaning at an n-ary argument. Geb.CobhamFold.stepWord_comp1Of is this at arity one.

The mult-fold self-concatenation of the recursion variable, of arity one: the empty bitstring at mult = 0, and one more copy of the sole argument at each successor.

The multiplier has arity one, at every multiplicity. A case split, not a recursion: both Nat.rec branches are comp nodes of arity one.

The multiplier is admissible, at every multiplicity.

The multiplier's arity, in the form Cobham.fst_eval composes with.

The multiplier carries no recursion of its own: every node is a comp, a proj, or the concat or zero generator.

The meaning of the multiplier at its arity.

The multiplier's value has length exactly mult times the argument's. Stated at an arbitrary environment, which is the form the recursion bound reads it at.

The multiplier with growth bits prepended: the bound child of a scan whose state may exceed the input by a factor as well as a constant. Cobham.prependRaw supplies the prepending, so the three obligations below are its own.

The bound child has arity one, at every multiplicity and growth.

The bound child is admissible, at every multiplicity and growth.

The bound child's arity, in the form Cobham.fst_eval composes with.

The bound child carries no recursion of its own, at every multiplicity and growth.

The meaning of the bound child at its arity.

The bound child's value has length growth + mult * |x 0|.

The scan node at steps of arity two, which read the remaining word in slot zero as well as the recursive value in slot one.

The arity-two scan node is admissible from its children's.

The scan node at an arbitrary bound child: scan2Raw at two steps lifted from arity one, which is the shape Cobham.scan takes.

Cobham.scan's additive bound and the multiplicative bound are two instances of one node: at Cobham.boundRaw the parameterized node is Cobham.scanRaw itself, definitionally.

The multiplicative bound child is not the additive one at any growth, so an expression built on it is a different raw tree from the corresponding Cobham.scan even at the multiplier one. At growth zero the two are nodes of different shape; each successor wraps both in the same comp node, so the recursion carries the separation up.

The scan node is admissible when its base is, at arity zero, its two steps are, at arity one, and its bound child is, at arity one: wValid_scan2Raw at the lifted steps.

The scan node over expressions, carrying its admissibility.

The scan node's arity, in the form Cobham.fst_eval composes with.

The meaning of a scan at its arity, read at the raw tree.

The scan's value on the empty bitstring is the base's word, at every bound child.

One step of the scan: the bit selects the step, which reads the value the scan of the rest of the word returns.