Problems with fixpoints of polynomials of polynomials

TL;DR

This work develops a fibred, container-based framework for fixpoints of polynomial endofunctors, enabling systematic construction of initial algebras, terminal coalgebras, and mixed fixpoints via $\zeta$-expressions. It introduces $\zeta$-expressions as a syntax that generalizes $\mu$-bicomplete notions to the fibred container setting and interprets them as problems whose denotations yield regular infinite tree languages and correspond to Weihrauch degrees through the notion of the answerable part. Under mild assumptions on the base category (lextensive with indexed $\mathcal{W}$- and $\mathcal{M}$-types), the main existence theorem shows that fibred polynomial endofunctors admit these three fixpoints, providing a constructive pathway from base fixpoints to complex, layered fixpoints. The paper then analyzes parallelization and iteration operators, linking them to the free monad on a polynomial and to Weihrauch reductions, and grounds the theory with ground problems and automata-theoretic representations, illustrating a rich interaction between category theory, logic, and computability theory. It further demonstrates that many Weihrauch degrees appear as the answerable parts of closed $\zeta$-expressions, while also acknowledging limitations and open questions about capturing higher degrees and more intricate reductions.

Abstract

Motivated by applications in computable analysis, we study fixpoints of certain endofunctors over categories of containers. More specifically, we focus on fibred endofunctors over the fibrewise opposite of the codomain fibration that can be themselves be represented by families of polynomial endofunctors. In this setting, we show how to compute initial algebras, terminal coalgebras and another kind of fixpoint $ζ$. We then explore a number of examples of derived operators inspired by Weihrauch complexity and the usual construction of the free polynomial monad. We introduce $ζ$-expressions as the syntax of $μ$-bicomplete categories, extended with $ζ$-binders and parallel products, which thus have a natural denotation in containers. By interpreting certain $ζ$-expressions in a category of type 2 computable maps, we are able to capture a number of meaningful Weihrauch degrees, ranging from closed choice on $\{0, 1\}$ to determinacy of infinite parity games, via an "answerable part" operator.

Figures (6)

• Figure 1: Endofunctors $\mathsf{Cont}(\mathcal{C}) \to \mathsf{Cont}(\mathcal{C})$ defined via fixpoint equations. Since the definition of $\star$ requires $\mathcal{C}$ to be a lccc, the last two definitions are not quite the same as the operators on Weihrauch degrees (see PricePradic25).
• Figure 2: Problems from the Weihrauch lattice as the answerable part of the interpretation of some $\zeta$-expressions in represented spaces. On the left-hand side is the part of the Weihrauch lattice we capture, where all inequalities are known to be strict below $\mathbf{\Pi}^1_1\text{-}\mathsf{CA}_0$. $\mathbf{\Gamma}\text{-}\mathsf{FindWS}$ is the answerable part of the problem where a question is code for a $\mathbf{\Gamma}$-set $A$ which is answered by a winning strategy for the player with winning condition $A$ in a Gale-Stewart game over ${\mathbb{N}^\mathbb{N}}$.
• Figure 3: Informal string diagram representing the composition of (unary 1-dimensional) container morphisms $(\gamma, \varphi) \circ (\psi, \theta)$. Note that it is not meant to simply be interpreted in a cartesian category in this paper.
• Figure 4: Definitions of the tensorial products on $\mathsf{Cont}(\mathcal{C})$; we allow ourself to use the internal language of $\mathcal{C}$ as a locally cartesian closed category for $\star$ and let the reader guess what is the unique possibility for the morphism.
• Figure 5: Matrix of the kinds of fixpoints we get from applying the recipe outlined after \ref{['thm:fp-exist']} and \ref{['prop:2algebraMu']}.

Theorems & Definitions (86)

• Definition 1: carboni93extensive
• Remark 2
• Example 3
• Example 4
• Example 5
• Lemma 6: Lambek's lemma
• Proposition 8: Corollary of GKpoly
• Definition 9
• Definition 10
• Example 11