Problems with fixpoints of polynomials of polynomials

技术摘要：多项式函子的多项式不动点问题

问题陈述
本文探讨了刻画容器范畴（具体为余域纤维化之纤维逆上的纤维化自函子）上自函子不动点的挑战。虽然基于范畴 $C$ 的多项式函子已被公认可 admitting 初始代数（最小不动点，$\mu$）和终端余代数（最大不动点，$\nu$），但作者研究了这些不动点提升到容器范畴 $\text{Cont}(C)$ 时的行为。

识别出的一个核心问题是，针对无限并行化（$\zeta X. P \otimes X$）或无限顺序迭代（$\zeta X. X \star P$）等算子的标准不动点构造，在 Weihrauch 复杂度的背景下往往无法产生有意义的“最大不动点”。具体而言，此类函子的终端余代数可能定义了一个问题空间（例如问题流），但未能提供相应的答案空间，从而有效地使问题平凡化。作者寻求对一种“中间”不动点（记为 $\zeta$）的结构化理解，该不动点允许计算初始代数、终端余代数以及这一中间不动点，而不会使答案空间平凡化。

方法论
作者建立了一个基于纤维多项式函子的范畴框架。他们假设基础范畴 $C$ 是一个 $\Pi$WM-范畴（即：扩展的、局部笛卡尔闭的，且具有依赖 W-类型和 M-类型）。

1. 纤维多项式函子：他们将函子 $F: \text{Cont}(C) \to \text{Cont}(C)$ 定义为纤维多项式，如果它是一个关于形状函子 $\text{shape}: \text{Cont}(C) \to C$ 的纤维函子，且其基础分量 $F_0: C \to C$ 是一个多项式函子。
2. 提升不动点（定理 18）：核心方法论贡献是计算 $F$ 不动点的“配方”，即通过从基础范畴 $C$ 提升不动点来实现。要计算 $F$ 的终端余代数，首先计算基础函子 $F_0$ 的终端余代数 $(\nu F_0, c_{\nu F_0})$。然后，计算在 $\nu F_0$ 纤维上诱导函子的终端余代数。这一两步过程允许构建三种类型的不动点：
   • 初始代数（$\mu F$）：通过 $F_0$ 的初始代数和纤维中的终端余代数计算得出。
   • 终端余代数（$\nu F$）：通过 $F_0$ 的终端余代数和纤维中的初始代数计算得出。
   • $\zeta$-不动点：一种混合构造，在基础层和纤维层均使用终端余代数，生成一个容器 $\zeta F$，并满足同构 $F(\zeta F) \cong \zeta F$。
3. $\zeta$-表达式：作者引入了一种名为$\zeta$-表达式的语法，通过引入 $\zeta$-绑定符和并行积扩展了 $\mu$-双完备范畴。这些表达式被解释为纤维多项式函子。
4. 自动机理论解释：利用正则树语言理论和奇偶博弈理论，作者表明任何闭 $\zeta$-表达式都可以算法地转换为正则博弈树语言 $L_E$。该表达式的指称对应于一个问题，其中问题是 $L_E$ 中的树，而答案是关联奇偶博弈中“偶”玩家的获胜策略。
5. 可回答部分算子：认识到 $\zeta$-表达式的指称往往因存在不可回答的问题而具有平凡度（等价于 $0$、$I$或$1$），作者引入了Ans算子。该算子将容器限制为其“可回答部分”（即问题有答案的子对象），从而允许提取非平凡的 Weihrauch 度。

关键贡献与结果

• 存在性定理（定理 18）：本文证明了对于 $\Pi$WM-范畴上的纤维多项式函子，初始代数、终端余代数以及中间 $\zeta$-不动点总是存在的。这为无限并行化和迭代等算子提供了严格的范畴基础，这些算子此前在 Weihrauch 复杂度中已被研究，但缺乏统一的理论结构。
• Weihrauch 度的刻画：通过对 $\zeta$-表达式的指称应用Ans算子，作者捕捉到了 Weihrauch 格中的相当大一部分。具体而言，他们表达了：
  • $\mathbb{N}$ 上的闭选择（$C_{\mathbb{N}}$）和有限集（$C_k$）。
  • 弱柯尼希引理（WKL）。
  • 极限算子（$\lim$）及其变体。
  • $\Delta^0_1$ 和 $\Delta^0_2$ 目标的确定性。
  • 这些原理的无限并行化。
• 未过滤表达式的平凡性（命题 32，推论 57）：作者证明，如果没有Ans算子，闭 $\zeta$-表达式的度是平凡的。这突显了过滤掉不可回答问题以恢复有意义计算内容的必要性。
• 自动机理论界限（命题 40）：本文确立了通过 $\zeta$-表达式（应用Ans后）可表达的问题受限于具有特定优先级的奇偶博弈的确定性。具体而言，它们在 Weihrauch 格中无法表达严格高于 $(\Sigma^0_2)_k\text{-FindWS}$ 的问题。
• 严格层级：作者证明了某些层级的严格不等式，例如 $(\Sigma^0_1)^c_{k}\text{-FindWS} < (\Sigma^0_1)^c_{k+1}\text{-FindWS}$，并将它们与 $\Pi^1_1\text{-CA}_0$ 的有限迭代联系起来。

意义与主张
本文声称提供了容器背景下不动点的“结构化理解”， bridging 了多项式函子的代数理论与 Weihrauch 可归约性的计算理论之间的鸿沟。

• 统一：它将 Weihrauch 度上算子的代数理论（此前依赖于特设定义）与容器和多项式函子的范畴理论统一起来。
• 表达能力：它表明，当与Ans算子结合时，$\zeta$-表达式具有惊人的表达能力，捕捉了从闭选择到无限奇偶博弈确定性的基准问题。
• 局限性：作者谦逊地承认了其方法的局限性。他们指出，自动机理论的刻画将可表达度限制在奇偶博弈确定性之下。他们推测，像成对拉姆齐定理（$RT^2_2$）这样的自然度不与任何 Ans($\llbracket E \rrbracket$) 等价。
• 开放问题：本文最后提出，两个 $\zeta$-表达式的可回答部分的等价性是否可判定，并将此与树自动机的索引问题联系起来。

这项工作并未提出新的实验应用，而是提供了一个理论框架，用于通过范畴论和不动点逻辑的视角来理解和构造可计算分析及 Weihrauch 复杂度中的问题。