Rolling Rule

Definition

Let $\mathcal{C}$ and $\mathcal{D}$ be categories. Suppose we have functors $F:\mathcal{C}\to \mathcal{D}$ and $G:\mathcal{D}\to \mathcal{C}$. The Rolling Rule states there is a canonical isomorphism between the fixed points of the compositions $FG$ and $GF$. Specifically, if $\nu (FG)$ is the terminal coalgebra of $FG:\mathcal{D}\to \mathcal{D}$ and $\nu (GF)$ is the terminal coalgebra of $GF:\mathcal{C}\to \mathcal{C}$, then the following both hold:

$\nu (FG)\cong F(\nu (GF))$ $\nu (GF)\cong G(\nu (FG))$ Likewise for initial algebras $\mu (FG),\mu (GF)$, $\mu (FG)\cong F(\mu (GF))$ $\mu (GF)\cong G(\mu (FG))$

Technical Context

We interpret this via the behavior of the fixpoint operator $\mu$ (for initial algebras) or $\nu$ (for terminal coalgebras). In many-sorted logic or functional programming, this justifies why swapping the order of nested data types results in equivalent structures. For a terminal coalgebra $(T,\tau )$ where $\tau :T\to FGT$, we can construct a terminal coalgebra for $GF$ using the action of $G$ on the structure map.

Alternative Approaches

While often called the Rolling Rule in the context of fixed-point calculi (like the $\mu$-calculus), it is also a consequence of the fact that $F$ and $G$ preserve certain limits or colimits, or more generally, it follows from the theory of adjoint functors. If $F⊣G$, the relationship between their fixed points is even more rigid.

References

backhouse1997-program-construction santocanale2002-circular-proofs