The function class B of Bellantoni and Cook

The syntax of the function class B and its interpretation, following [HeraudNowak2011] § 3.2. Terms of B are built from a constant zero, projections, two successors, a predecessor and a conditional, and are closed under a composition and a recursion that distinguish normal from safe argument positions; the distinction is what bounds the growth rate of the definable functions.

The class defined here is the reformulation of § 3.2, not the class of [BellantoniCook1992]. Two differences: the conditional takes four safe arguments and branches three ways, on the empty, odd and even bitstrings, where the original branches two ways on parity and treats the empty bitstring as even; and the base case of the recursion is the empty bitstring, where the original's is every bitstring denoting zero.

The two sources transpose the conditional's last two safe arguments. The order here follows the authors' Coq development, that being the artifact against which the paper's theorems were machine-checked.

Main definitions

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

BellantoniCook.Direction — the subterm positions of a shape.

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

BellantoniCook.q — the arity a shape produces.

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

BellantoniCook.compChildren — a comp node's children in the order Direction gives them.

BellantoniCook.BC — an expression of B: a sig-tree whose every node respects rc.

BellantoniCook.BC.arity — its pair of normal and safe arities.

BellantoniCook.BCOf — the expressions of a given arity pair.

BellantoniCook.Sem — the meaning of an arity pair: a function of a normal and a safe environment.

BellantoniCook.transport — transport of a meaning along an equality of arity pairs.

BellantoniCook.evalRec — the recursion on the consumed bitstring.

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

BellantoniCook.evalStep — evalValue as a slice algebra.

BellantoniCook.BC.eval — the interpretation, by the slice W-type's eliminator.

Implementation notes

This repository expresses all recursion through recursors, admitting neither a self-referential inductive nor a self-calling def, so the arity-indexed syntax is the slice W-type of sig and the interpretation is one application of SlicePFunctor.W.elim. Shape is itself non-recursive and so is the shape set of a PFunctor, not a datatype the rule reaches.

evalValue is separate 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 of the six sites.

Direction, rc and q are @[reducible]. Instance search does not delta-reduce a semireducible definition, and every numeral in evalValue elaborates against Fin (q a).1 or Direction a.

Mathlib.Logic.Equiv.Fin.Basic is imported for finSumFinEquiv. It transitively supplies Mathlib.Data.Fin.Tuple.Basic, the source of Fin.cons, Fin.tail and Fin.append used here, and Mathlib.Data.Fin.VecNotation, reached the same way by the test module's ![…] notation. Neither is imported by name, so that lake shake does not report either as a redundant import.

sigFinitary's comp branch resolves FinEnum (Unit ⊕ Fin m ⊕ Fin k) through the choice-free FinEnum.unit and FinEnum.finSum (two applications, for the outer and inner sums), 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.

References

[HeraudNowak2011]

[BellantoniCook1992]

Tags

Bellantoni-Cook, polytime, implicit computational complexity, safe recursion, W-type, polynomial functor

The seven constructor forms of B, each carrying its arities as parameters: zero the constant empty bitstring; proj n s i the ith of n normal and s safe variables; succ b the successor appending the bit b; pred the predecessor; cond the four-argument conditional; safeRec n s the recursion producing arity (n + 1, s); and comp n s m k the composition of an expression of arity (m, k) with m normal and k safe argument expressions of arity (n, 0) and (n, s).

The subterm positions of a shape. The five base forms have none; safeRec has three, its base and its two step expressions; comp has its head, its m normal arguments and its k safe arguments.

The arity each subterm position must carry: the hypotheses of the arity relation of [HeraudNowak2011] § 3.2.

The arity a shape produces: the conclusions of the arity relation of [HeraudNowak2011] § 3.2.

The signature of B as a slice polynomial functor over ℕ × ℕ, the index being the pair of normal and safe arities.

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 children of a comp node, in the order Direction gives them: the head, then the normal arguments, then the safe arguments.

An expression of B: a sig-tree every node of which carries children at the indices rc prescribes.

The arity pair of an expression: its normal and safe arities.

The expressions of arity (n, s), which is the arity relation of [HeraudNowak2011] § 3.2 as a type rather than a side condition.

The meaning of an arity pair: a function of a normal and a safe environment, each a tuple of bitstrings, returning a bitstring.

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

The recursion safeRec performs on its first normal argument, by List.rec. The base case is the empty bitstring; a step consumes the low bit b, passes the remaining bitstring v as the new first normal argument, and passes the recursive value in safe position.

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.

cond reads its first safe argument and returns the second, third or fourth according as it is empty, odd or even — the ordering of the authors' Coq development. comp applies its head's meaning to the normal arguments' meanings, each in the empty safe environment, and to the safe arguments'.

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 an expression: its arity pair together with its meaning at that pair, by the slice W-type's eliminator.