The scan combinator over Cobham's class

A scanner is a right-to-left fold over a bitstring whose state is itself a bitstring: a base value, one step per bit read, and a bound on how far the state can exceed the input. Cobham.evalRec supplies the recursion, peeling the word's last bit at each step and passing the rest of the word on; the state is the recursive value it passes alongside.

evalRec applies its step to Fin.cons v (Fin.cons (ih x) x): slot zero is the rest of the word, slot one the recursive value, slots two upward the ambient environment. A fold's step is a function of the state alone, so a scanner's steps are COf 1, lifted into the shape evalRec applies by composition with proj 2 1.

Main definitions

Cobham.boundRaw — the bound child, succ true iterated over proj 1 0.

Cobham.liftRaw — a step of arity one in evalRec's step shape.

Cobham.scanRaw — the boundedRec node over a base, two lifted steps and a bound child.

Cobham.scanW — that node over expressions, carrying admissibility.

Cobham.boundSem, Cobham.scanSem — the meanings of the bound child and of the scan, at arity one.

Cobham.baseWord, Cobham.stepWord, Cobham.scanStepWord — the words a base and a step contribute, and the semantic step of the fold.

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

Main statements

Cobham.wValid_boundRaw, Cobham.wValid_liftRaw, Cobham.wValid_scanRaw — admissibility of the three trees, the last from its components'.

Cobham.wIndexRoot_boundRaw, Cobham.wIndexRoot_liftRaw, Cobham.arity_boundRaw, Cobham.arity_scanW — their arities.

Cobham.boundSem_eq — the bound child prepends growth bits.

Cobham.scanSem_nil, Cobham.scanSem_cons, Cobham.scanSem_eq — the scan on the empty word, on one bit, and as a List.foldr.

Cobham.baseWord_eq_eval, Cobham.stepWord_eq_eval — each component's word is the one its expression of C carries.

Cobham.recBounded_boundRaw, Cobham.recBounded_liftRaw — the bound child and a lifted step carry no recursion of their own.

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

Implementation notes

Admissibility of a node requires the children's index equations alongside their own admissibility, SlicePFunctor.wValid_mk constraining wIndexRoot ∘ children; that is where the raw layer and the expression layer meet, and it is why wValid_scanRaw takes six hypotheses rather than three. The equations are stated through SlicePFunctor.wIndexValid_index_eq_wIndexRoot, the goal presenting the index as WIndex.index ∘ wIndexValid rather than as wIndexRoot.

decide discharges none of these: at a variable child nothing reduces. It remains available at a named constant, which is what the instances built on this module use.

A child family indexed by Fin 4 is bound as fun d : Fin 4 ↦ …. Instance search stops at reducible transparency on the projection sig.B a, so without the ascription a numeral index fails to elaborate.

Each component's meaning is transported along the composition of fst_eval with the component's arity equation, in one step rather than two. transport along an equation whose sides reduce to the same literal disappears by proof irrelevance; along an opaque equation it does not, and a transport along a composite equality is then not definitionally the composition of two transports. The scan node's own arity reduces to one whatever its children are, so its transport disappears; a component's arity equation is base.2 or step.2 at a variable, which reduces to nothing. The composed form is what keeps scanSem_nil a rfl and lets scanSem_cons's change land, at the price of making the two bridges to C.eval theorems rather than definitions.

scanSem_cons is not definitional in its last step: the lifted step applies its head at fun _ : Fin 1 ↦ r, while stepWord applies it at ![r], and the two agree only by funext.

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]

Tags

Cobham, bounded recursion on notation, scan, fold, polynomial functor

The bound child: succ true iterated growth times over the recursion variable, of arity one. growth = 0 is the Nat.rec base, the bare projection.

The bound child has arity one, at every growth. A case split, not a recursion: both Nat.rec branches are nodes whose shape q sends to one.

The bound child is admissible, at every growth.

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

An arity-one tree applied to argument one of an arity-two tree: a comp node whose head is the arity-one tree and whose sole argument is proj 2 1. Motivating instance: a scanner's step, carried into the shape evalRec applies, whose argument one holds the recursive value.

A lifted step has arity two, whatever it lifts.

A lifted step is admissible when what it lifts is admissible and of arity one.

The scan node: a boundedRec of ambient arity zero over a base, two lifted steps and a bound child.

The scan node is admissible when its base is, at arity zero, and its two steps are, at arity one. These index equations are where the raw layer and the expression layer meet.

The scan node over expressions, carrying its admissibility.

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

The meaning of the bound child at its arity.

The bound child prepends growth bits to the recursion variable. Stated at an arbitrary environment, which is the form the recursion bound reads it at; at ![u] it does not match the goal RecBoundedValue presents.

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

The word a base contributes, read at the raw tree.

The word a step contributes at the state it reads, read at the raw tree.

The semantic step of a scan: the bit selects which step reads the state.

The base's word is the one its expression of C carries. Not a rfl: a component's arity equation is opaque at a variable, so the transport along the composite and the composition of two transports differ.

A step's word is the one its expression of C carries, as baseWord_eq_eval for the base.

The scan's value on the empty bitstring is the base's word.

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

A scanner computes the right fold of its steps over the word, from its base. It holds at every growth, evalValue's boundedRec clause not consulting its bound child.

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

A lifted step carries the recursions of what it lifts and no other, the comp node's own condition being vacuous.

The scanner as an expression of C: the scan node with its recursion bound discharged from a bound on the value the scan produces. The bound is an argument rather than a field of a structure, no consumer holding a scanner as a value.