Cobham's class of bitstring functions

The syntax of a Cobham-style function algebra on bitstrings, whose recursion scheme is bounded recursion on notation [Cobham1965], together with its interpretation over every sig-tree. Terms are built from a constant zero, projections, two successors, a smash and a concat generator, and are closed under a composition and a bounded recursion. [HeraudNowak2011]'s grammar for C (O | Πⁱₙ | S_b | # | Compⁿ | Rec) has no concatenation generator; the concat generator here is added, grounded in [Strahm2003]'s operator list [ε, I, s₀, s₁, ∗; COMP, BRN], and is what makes the smash-free bound SmashFree names expressible at all. sig fixes the shape of the syntax alone — each constructor's arity and the arity relation its subterms must satisfy — and eval gives the meaning of any tree respecting that relation. Cobham's class itself is the subtype C of trees whose recursions additionally respect the length bound the scheme imposes, carrying eval down to C.eval.

A bitstring is List Bool, its head the word's last bit. succ b — S_b in [HeraudNowak2011]'s notation, s₀/s₁ in [Strahm2003]'s — prepends by consing b. boundedRec's recursion evalRec — [HeraudNowak2011]'s Rec — peels that head at each step, passing the remaining bitstring on as the new recursion variable. concat — ∗ in [Strahm2003]'s list — reads its second argument as the earlier part of the word and its first as the later part, fun x ↦ x 1 ++ x 0, consistent with the same convention.

SmashFree names the subalgebra [ε, I, s₀, s₁, ∗; COMP, BRN], which [Strahm2003] Theorem 1(2) contains in the functions computable simultaneously in polynomial time and linear space, a characterization [Strahm2003] attributes to [Thompson1972] and [Strahm2010] Theorem 5 restates. [Clote1999] Theorem 3.20 gives an arithmetic analogue over the naturals. Linear space alone is the second Grzegorczyk class [Ritchie1963] (via [Clote1999] Theorem 3.36 and its Corollary 3.37), the class Bellantoni's safe recursion also characterizes [Bellantoni1992] (via [Clote1999] Theorem 3.101).

Main definitions

Cobham.Shape — the seven constructor forms, with their arities as parameters.

Cobham.Direction — the subterm positions of a shape.

Cobham.rc — the arity each subterm position must carry.

Cobham.q — the arity a shape produces.

Cobham.sig — the signature, as a slice polynomial functor over ℕ.

Cobham.sigFinitary — every shape has finitely many directions.

Cobham.Sem — the meaning of an arity: a function of an environment of bitstrings.

Cobham.transport — transport of a meaning along an equality of arities.

Cobham.evalRec — the recursion boundedRec performs on its recursion variable.

Cobham.evalValue — the meaning of one node from its children's meanings.

Cobham.evalStep — evalValue as a slice algebra.

Cobham.eval — the interpretation of a sig-tree, by the slice W-type's eliminator.

Cobham.arity — the arity of a sig-tree.

Cobham.semAt — the meaning of a tree at a given arity.

Cobham.RecBoundedValue — the length bound one node imposes.

Cobham.RecBounded — RecBoundedValue at every node, hereditarily.

Cobham.C — Cobham's class: the trees satisfying RecBounded.

Cobham.C.arity — the arity of an expression.

Cobham.COf — the expressions of a given arity.

Cobham.C.eval — the meaning of an expression, at its own arity.

Cobham.zeroAt, Cobham.zeroAtOf — the empty bitstring at an arbitrary arity.

Cobham.concatRaw / Cobham.smashRaw — the two generators as single nodes.

Cobham.concatOf / Cobham.smashOf — those nodes as expressions of arity two.

Cobham.predRaw / Cobham.pred — the predecessor, as a raw tree and as an expression of arity one.

Cobham.predSem — the meaning of the predecessor.

Cobham.predIter, Cobham.predIterOf — the iterated predecessor.

Cobham.prepend, Cobham.prependOf — a fixed word prepended to an expression.

Cobham.constAt, Cobham.constAtOf — the constant word at a given arity.

Cobham.diag, Cobham.diagOf — a binary expression at its sole argument in both positions.

Cobham.concatCompRaw — the concatenation of two raw trees of a common arity.

Cobham.condRaw / Cobham.cond — the four-way conditional, as a raw tree and as an expression of arity four.

Cobham.condSem — the meaning of the conditional.

Cobham.smashFreeBool — whether no smash node occurs anywhere in a raw tree.

Cobham.SmashFree — the subalgebra [ε, I, s₀, s₁, ∗; COMP, BRN], excluding the smash generator.

Main statements

Cobham.transport_transport — transport along a composite equality is the composition of two transports.

Cobham.fst_eval — the index component of a tree's interpretation is its arity.

Cobham.recBounded_mk — RecBounded unfolded one level, on a raw node.

Cobham.predSem_eq — the predecessor drops the word's last bit.

Cobham.wIndexRoot_predIterRaw, Cobham.wValid_predIterRaw, Cobham.recBounded_predIterRaw — the iterated predecessor's arity, admissibility and recursion bound.

Cobham.wIndexRoot_prependRaw, Cobham.wValid_prependRaw, Cobham.recBounded_prependRaw — prepending preserves the arity, admissibility and the recursion bound.

Cobham.wIndexRoot_diagRaw, Cobham.wValid_diagRaw, Cobham.recBounded_diagRaw — the diagonal's arity, admissibility and recursion bound.

Cobham.condSem_eq — the conditional branches on the emptiness and parity of its first argument.

Implementation notes

Every def in this module is @[expose], so a wrapper module and the tests can unfold them across the module boundary; the sigFinitary instance, the Decidable (SmashFree ·) instance, and the theorems need no such tag.

concatRaw and smashRaw are named apart from the expressions built on them because instance search finds Decidable (sig.WValid w) when w is a constant but not when it is a literal WType.mk application, with or without an ascription, so decide discharges admissibility only of a named tree.

Direction, rc and q are @[reducible]. Instance search does not delta-reduce a semireducible definition, and sigFinitary resolves FinEnum (sig.B a) against the literal Direction a each branch produces.

sigFinitary's comp branch resolves FinEnum (Unit ⊕ Fin m) through the choice-free FinEnum.unit and FinEnum.finSum, and its other branches resolve FinEnum (Fin n) through the choice-free FinEnum.finFin. Those instances are scoped in namespace FinEnum; this module's open scoped FinEnum is required for them to win resolution over mathlib's Classical.choice-dependent counterparts, which lake lint rejects.

evalValue is a separate definition from evalStep because the match on Shape must generalize the compatibility hypothesis, which arrives bundled in SliceDomPFunctor.Obj. A child's meaning carries the index it was built at rather than the index rc prescribes, equal but not definitionally so; transport carries it across, with the motive of ▸ fixed once instead of at each use site. evalValue's boundedRec clause does not consult its bound child's meaning: the bound is a side condition on admissibility, imposed by RecBoundedValue, not part of a tree's value.

eval is a slice morphism, so the index it returns agrees with arity only by SlicePFunctor.W.comp_elim, a funext theorem; C.eval is therefore transport (fst_eval _) (eval _).2 rather than the second projection alone, and the index equation RecBoundedValue consumes is the node's compatibility composed with fst_eval. recBounded_mk is stated on the raw ⟨WType.mk a f, _⟩ rather than on SlicePFunctor.W.mk, at which the WType.rec of RecProp iota-reduces and the unfolding is definitional; the index equation is a hypothesis, definitional proof irrelevance making the choice of proof term immaterial. C.arity and C.eval qualify arity and eval because the namespace of the declaration being elaborated is in scope, which would otherwise make each body self-referential.

zeroAtRaw carries a free arity, at which decide does not apply; its admissibility is the pair of an Unit ⊕ Fin m case analysis and the funext the index condition asks for.

References

[Bellantoni1992]

[Clote1999]

[Cobham1965]

[HeraudNowak2011]

[Ritchie1963]

[Strahm2003]

[Strahm2010]

[Thompson1972]

Tags

Cobham, bounded recursion on notation, linear space, W-type, polynomial functor

The seven constructor forms of Cobham's class, each carrying its arities as parameters: zero the constant empty bitstring; proj n i the ith of n variables; succ b the successor appending the bit b; smash and concat the two bitstring generators; comp n m the composition of an m-ary expression with m n-ary argument expressions; boundedRec n the bounded recursion producing arity n + 1.

The subterm positions of a shape. The five base forms — zero, proj, succ, smash and concat — have none, smash and concat being generators rather than recursive constructions; comp has its head and its m argument expressions; boundedRec has four, its base, its two step expressions and its bound.

The arity each subterm position must carry: the hypotheses of the arity relation of bounded recursion on notation [Cobham1965].

The arity a shape produces: the conclusions of the arity relation of bounded recursion on notation [Cobham1965].

The signature of Cobham's class as a slice polynomial functor over ℕ, the index being the arity.

Every shape has finitely many directions, which is what makes admissibility of a sig-tree decidable. The branches ascribe their instances explicitly: instance search stops at reducible transparency on the projection sig.B a, so a bare inferInstance does not find them.

The meaning of an arity: a function of an environment of bitstrings, one per argument, returning a bitstring.

Transport of a meaning along an equality of arities. Named so that the motive of ▸ is fixed once rather than inferred at each use in evalValue.

Transport composes. A transport along a composite equality and the composition of two transports agree, which is not definitional when neither index reduces: at a variable expression the arity equation is opaque, so neither Eq.rec fires. Named for its left-hand side, as core's cast_cast is.

The recursion boundedRec performs on its recursion variable, by List.rec, matching [HeraudNowak2011]'s Rec (f(y·i, x) = h_i(y, f(y,x), x)), not [Strahm2003]'s last-argument form. The base case is the empty bitstring; a step consumes the low bit b, passes the remaining bitstring v as the new recursion variable, and passes the recursive value alongside it.

The meaning of one node, from its children's meanings and the proof that each child's index is the one rc prescribes. A separate definition from evalStep because the match on Shape must generalize that proof.

The bitstring generators read the ambient environment directly, Direction being Fin 0 for each: zero returns the empty bitstring; proj n i returns the ith argument; succ b prepends b to the argument. smash and concat are Cobham's two generators: smash marks its result with a leading true, so |#(a, b)| = |a| · |b| + 1; concat reads its second argument as the earlier part of the word and its first as the later part, consistent with the list head representing the word's last bit. comp applies its head's meaning to the argument expressions' meanings, each read at the ambient environment. boundedRec performs evalRec on its recursion variable, its base and two step children supplying g, h₀ and h₁.

evalValue as an algebra for sig in the slice over ℕ. Returning the shape's own output index as the first component makes the eliminator's coherence obligation hold by rfl.

The interpretation of a sig-tree: its arity together with its meaning at that arity, by the slice W-type's eliminator.

The arity of a sig-tree.

The index component of a tree's interpretation is the tree's arity. eval is a morphism in the slice over ℕ, so composing it with the index projection gives sig.wIndex; this is that equation read at a single tree, the form transport consumes.

The meaning of a tree at a given arity.

The recursion bound of one node, from its children and the proof that each child's evaluated index is the one rc prescribes. It is vacuous at every shape but boundedRec, where it is the side condition of bounded recursion on notation [Cobham1965]: at every environment, the recursion's value is no longer than the meaning of the bound child. evalValue's boundedRec clause supplies the bounded quantity, read at the same environment.

The admissibility of a sig-tree: every node satisfies RecBoundedValue, hereditarily. The fold over the tree is carried by the slice W-type's Prop-valued paramorphism SlicePFunctor.W.RecProp; the index equation RecBoundedValue requires is the node's compatibility (SliceDomPFunctor.compatible_iff) composed with fst_eval, since compatibility constrains a child's wIndex rather than the index its interpretation carries.

One-level unfolding of RecBounded on a raw node ⟨WType.mk a f, hv⟩: the root's RecBoundedValue together with admissibility of every child. Stated on the raw tree rather than on SlicePFunctor.W.mk, so that WType.rec iota-reduces and the equation is definitional.

Cobham's class as a type of expressions: the sig-trees whose recursions respect the length bound.

The arity of an expression, that of the underlying tree.

The expressions of a given arity.

The meaning of an expression, at its own arity. The underlying tree's interpretation carries the index eval computed, equal to the arity by fst_eval but not definitionally so, hence the transport.

The empty bitstring at an arbitrary arity.

The empty bitstring as an expression of arity n.

zeroAt n at its declared arity.

The concat generator as a single node, its Direction being empty.

The concat generator as an expression of arity two, its RecBoundedValue vacuous and its hereditary conjunct empty.

The smash generator as a single node, its Direction being empty.

The smash generator as an expression of arity two, as concatOf.

The predecessor as a single boundedRec node, transcribing [HeraudNowak2011] § 4's Rec O Π⁰₂ Π⁰₂ Π⁰₁: base the constant empty bitstring, both steps the first of their two arguments, bound the sole argument. In an evalRec step environment the first slot holds the bitstring remaining after the last bit is peeled, so both steps return that remainder.

The predecessor as an expression of arity one. Its recursion respects the bound because its value at y is y with its last bit dropped, of length |y| - 1, while the bound child returns y; at the empty bitstring the value is empty.