Combinatorial specifications and order-raising recursive specifications

Fix a commutative ring $R$.

A combinatorial specification for an unknown class $\mathcal{Y}$ is an equation

$\mathcal{Y}=\mathrm{\Phi }(\mathcal{Y})$

whose right-hand side is built from already defined classes and from $\mathcal{Y}$ using symbolic constructions whose generating-function operations are defined over $R$. Replacing those constructions by their generating-function operations produces an associated operation $F_{\mathrm{\Phi }}(f)$ whenever all the required formal-series operations are defined at $f$. Write

$D_{\mathrm{\Phi }}:=\{f\in R\mathrm{⟦}x\mathrm{⟧}:F_{\mathrm{\Phi }}(f)\text{ is defined}\}$

for its natural domain. For example, a factor $\mathrm{SEQ}(\mathcal{Y})$ contributes $(1-f{)}^{-1}$, which is defined precisely when the constant coefficient of $1-f$ is a unit; being defined over $R$ does not make this operation total on $R\mathrm{⟦}x\mathrm{⟧}$.

Thus a specification using a construction whose series formula needs rational scalars, such as $\mathrm{CYC}$, is admitted here only when $R$ is a commutative $\mathbb{Q}$-algebra and the input satisfies that construction's order and constant-term conditions.

A nonempty set $D\subseteq D_{\mathrm{\Phi }}$ is an admissible domain when $F_{\mathrm{\Phi }}(D)\subseteq D$. The specification is order-raising on $D$ when

${\mathrm{ord}}_x(F_{\mathrm{\Phi }}(f)-F_{\mathrm{\Phi }}(g))\ge {\mathrm{ord}}_x(f-g)+1$

for all $f,g\in D$. When $D=R\mathrm{⟦}x\mathrm{⟧}$, so that $F_{\mathrm{\Phi }}$ is a total endomorphism of the whole series ring, we call the specification simply an order-raising recursive specification and write

$F_{\mathrm{\Phi }}:R\mathrm{⟦}x\mathrm{⟧}⟶R\mathrm{⟦}x\mathrm{⟧}\mathrm{.}$

This is the $x$-adic contraction condition. It says that changing the input only changes the output in strictly higher order, so successive coefficient prefixes stabilize. Specifications on a proper admissible domain require the corresponding invariant-domain fixed-point theorem; the total-map theorem developed here applies to the unqualified notion.