Multi-clocked Guarded Recursion Beyond {\omega}

技術要約：$\omega$ を超えるマルチクロック型ガード付き再帰

問題提起
マルチクロック型ガード付き再帰（Clocked Type Theory, CloTT など）を備えた型理論は、共帰的型（coinductive types）を用いたプログラミングや、非決定性や確率的選択といった高度な構成要素を特徴とするプログラミング言語の表示モデルを構築するための柔軟な枠組みを提供する。これらの理論は、木のトポス（$\omega$ によってインデックス付けされたもの）上のプレシェーブや、より最近ではキュービカル集合のプレシェーブを用いてモデル化することに成功してきたが、これらを標準的な集合論という「現実の世界」に関連付けることには依然としてギャップが存在する。

具体的には、標準的な集合論的解釈では、クロック量化と特定の関手（有限冪集合関手 $P_f$ や有限分布関手 $D_f$ など）や存在量化との可換性を保持できない場合がある。木のトポスにおいては、存在量化が必ずしも集合における存在へと外部化されるわけではなく、また $P_f$ や $D_f$ といった関手は、標準的なモデルにおいてクロック量化と可換ではない。その結果、Clocked Cubical Type Theory で証明された結果（例：モナド間の分配則や Probabilistic FPC における文脈的同値性に関する事項）は、現在、キュービカルモデル内の hsets 上のモナドに関する言明として解釈されており、その妥当性が標準的な集合の圏（$\mathbf{Set}$）において検証されていない。

手法
本論文では、必要な可換性を回復するために、マルチクロック型ガード付き再帰の外部的プレシェーブモデルをより高い順序数（$\rho > \omega$）へと拡張する方法を調査する。その手法は以下の通りである：

1. モデルの拡張： CloTT のプレシェーブモデル（Mannaa らによって $\rho = \omega$ の場合に定義されたもの）を、任意の正則極限順序数 $\rho$ によってインデックス付けされるように一般化する。モデルは、時間オブジェクトの圏 $T_\rho$（対象は有限のクロック集合と $\rho$ への写像のペア）上のプレシェーブの圏において構築される。
2. 可換性の意味論的解析： クロックに対する普遍量化（$\forall \kappa$）が、以下のものと可換となる条件を分析する：
   • 代数的理論によって生成される関手（具体的には $P_f$ や $D_f$ といったモナド）。
   • 存在量化（$\exists$）。
3. 構文的および意味論的条件：
   • 関手について： 関数 $F$ が $\kappa$-接近可能（$\kappa$-accessible）であり、$\kappa$-小な交わりを保存し、かつ単射のプルバックを保存する場合、 $F$ は $\rho^{op}$-インデックス付き極限（したがってクロック量化）と可換であることを確立する。ただし、$\rho$ が $\kappa$ の濃度を持つ順序数を含むことを条件とする。
   • 代数的理論について： 構文的条件が特定されている。すなわち、代数的理論は「ドロップ方程式（drop equations）」（二つの項における自由変数の集合が異なる方程式）を含んではならない。これにより、生成されるモナドが上記の意味論的条件を満たすことが保証される。
   • 存在量化について： 型 $X$ 上の存在量化 $\exists$ と $\forall \kappa$ が可換となるのは、 $X$ のファイバーの濃度がインデックス順序数 $\rho$ よりも厳密に小さい場合であることを証明する。また、「本質的に一意な」存在量化（証拠が有限の遅延ステップの範囲内で一意となるもの）についても扱う。

主要な貢献と結果

• Set に対する保存性： 本論文は、Clocked Type Theory モデルの標準的な集合論的モデルに対する保存性を明示し、証明している。これは、$\mathbf{Set}$ の内部言語で表現可能であり、かつ CloTT で証明可能なあらゆる言明は、$\mathbf{Set}$ においても真であることを意味する。
• モナドの可換性： 代数的理論によって生成されるモナドがクロック量化と可換となるための意味論的条件と、構文的基準（ドロップ方程式の不在）を提供する。これにより、インデックス順序数 $\rho$ が十分に大きい場合（例：可算操作に対して $\omega_1$）、$P_f$ や $D_f$ を用いた集合論的モデルにおける使用が正当化される。
• 存在量化の可換性： 十分に大きな正則順序数（例：$\omega_1$ 以上）を選択することで、クロックに対する普遍量化が、$\rho$ 未満の濃度の集合に対する存在量化と可換になることを示す。これにより、木のトポスから $\mathbf{Set}$ へと存在量化の証明を外部化する際の問題が解決される。
• 先行研究の解釈： Clocked Cubical Type Theory において形式化された以下のアプリケーションについて、それらが十分な大きさのインデックス順序数を持つ集合論的モデルにおいて解釈可能であることを示す：
  • 非決定論的および確率的システムの余代数的モデリング。
  • 弱双模倣性（weak bisimilarity）およびモナド間の分配則に関する推論。
  • Probabilistic FPC における文脈的同値性の証明。
    これらは、これらの結果が標準的な集合論的解釈の下で正しいことを証明するものである。

意義
本論文は、モデルのインデックス順序数を変化させることで、ガード付き再帰の内部論理（生産性と共帰性をエレガントに扱う）と、標準的な集合論という外部の世界との間のギャップを埋めることができると主張している。

その主要な意義は、Clocked Cubical Type Theory のメカニズムを用いて証明された結果を、キュービカル集合の特定の性質に依存することなく、標準的な集合論において検証することを可能にする点にある。これは、非決定性、確率論、および共帰的述語を含むエンコーディングの正当性を、適切なインデックス順序数を用いることで、基礎的な意味論的根拠を確立できることを示唆している。なお、これらの証明に用いられるメタ理論は古典的な集合論であるが、得られた結果は、商的帰納的型（quotient inductive types）や存在量化を含む共帰的型のエンコーディングの正当性を保証する、厳密な集合論的根拠を与えるものである。