Step recursion reveals structure of complex number sequences
Step Recursion: Exact Membership Spectra, Mixed Strides, and Collapse
Logic in Computer Science
Summary
This paper studies how sequences of numbers generated by repeatedly applying a function behave under different kinds of recursion. The authors explore when and how these sequences fit into mathematical systems known as function algebras, distinguishing between bounded and unbounded recursion cases. They show precise ways to understand membership in these algebras and find conditions under which the recursion simplifies ('collapses') to well-known forms. Their work links properties like polynomial growth of sequences to the definability of common arithmetic operations within these algebras.
What this means in practice
- •For formal methods engineers: Analyze properties of recursion schemes in program verification models handling complex iteration patterns.
- •For compilers and program analyzers: Determine when recursive function definitions can be simplified or transformed based on growth characteristics of iterated functions.
A theory result. No direct application yet.
Authors
Kirill Osipov
Abstract
For a strictly increasing $G:\mathbb{N}\to\mathbb{N}$ with $G(0)\geq 1$, we study minimal-basis function algebras generated by recursion along generalized inverses of its iterates. Bounded recursion requires an earlier pointwise majorant; unbounded recursion has no such requirement. If the orbit $G^{[t]}(0)$ has no polynomial upper bound, we obtain exact fixed-function membership spectra, reverse-divisibility inclusion, and indexed intersections that need not be single-stride algebras. Every finite divisibility-downset is realized in both regimes, and mixed strides admit fixed functions expressing any finite monotone Boolean condition on their additive stride monoid. For every generator, the realized bounded spectra form a bounded meet-semilattice: a construction sharing a bounding input coordinate realizes finite intersections without an unrestricted selector. Polynomial orbit growth is equivalent to definability of each of ordinary predecessor, unary doubling, and addition in any fixed unbounded stride algebra. In this case the algebra is ordinary primitive recursion relative to its inverse map, giving full collapse for primitive-recursive $G$. Ordinary predecessor belongs to a bounded stride algebra exactly when the orbit is polynomially bounded and $G$ has bounded successive differences; equivalently, ordinary bounded recursion embeds. A locality obstruction explains the additional bounded requirement, and two primitive-recursive generators with quadratic orbits have opposite bounded collapse behavior.