Non-Cartesian Guarded Recursion with Daggers

技術要約：ダガー（dagger）を伴う非カルテジアン型ガード付き再帰

問題提起
ガード付き再帰（guarded recursion）は、古典的なプログラミング言語におけるストリームや再帰的データ型の形式化のための確立されたフレームワークであり、通常はカルテジアン閉カテゴリ（CCC）内でモデル化される。しかし、多くの重要な計算パラダイム（具体的には可逆計算、並行計算、および量子プログラミング）は、CCCにおける意味論を採用できない。これらは、逆カテゴリ（inverse categories）やヒルベルト空間のカテゴリのように、ダガー（射に対する対合的な演算子）を備えたカテゴリに依存している。誘導型（inductive types）は一部のダガーカテゴリ（例：有向完備半順序集合に濃化された逆カテゴリ）でモデル化できるが、再帰の解釈は、特にヒルベルト空間においては依然として未解決または問題のある課題である。本論文は、ダガーカテゴリの文脈においてガード付き再 recursion のデノテーション意味論を提供するというギャップに対処しており、可逆性と再帰的データ構造の両方を必要とする可逆プログラミング言語を支援することを目的としている。

手法
著者は、非カルテジアン設定において「木のトポス（topos of trees）」のアプローチ（合成的ガード付きドメイン理論）を適応させた、圏論的な構成を提案する。その手法は以下の3つの主要な段階で進行する。

1. ガード付き構成 ($C^\infty$): 終対象を持つ任意のカテゴリ $C$ から出発し、論文では新しいカテゴリ $C^\infty$（$C^{\mathbb{N}^{op}}$ と同型）を構成する。$C^\infty$ の対象は、$C$ の対象の列であり、それらは射によって接続されており、プレシェーブに似ている。この構成は、「later」関手 ($L$) と「next」自然変換 ($\nu$) を導入し、これらはシーケンスの成分をシフトし、終対象を挿入することで、ガード付き再帰に必要な遅延モダリティをモデル化する。
2. 濃化と不動点: カテゴリ $C^\infty$ は、木のトポス ($S$) 上に濃化されていることが示される。この濃化により、合成的ガード付きドメイン理論からの不動点定理の適用が可能になる。具体的には、局所縮小的な関手は $C^\infty$ 上で一意の不動点を持ち、これにより、ベースとなるカテゴリ $C$ がカルテジアン閉でなくても、ガード付き誘導型（例：ストリームやリスト）の解釈が可能になることを本論文は示している。
3. ダガー・リグ構造との統合: 可逆計算をモデル化するために、本論文はダガー・リグカテゴリ（ダガー、テンソル積 $\otimes$、および和型 $\oplus$ を持つカテゴリ）に焦点を当てる。著者は、リグ構造（テンソルと和）はガード付き構成によって保持される一方で、ダガー構造は $C^\infty$ において自動的には保持されないことに注目している。これは、自然変換の成分ごとのダガーが、構成されたカテゴリにおける有効な射を生成しない可能性があるためである。これを解決するために、論文では精緻化された部分カテゴリ $C^\infty_e$（ダガー・エピモルフィズムを用いる）と、さらに「ダガー可能」な射（その成分ごとのダガーがカテゴリにおける有効な射となるもの）のみを含む部分カテゴリ $C^\infty_\dagger$ を定義する。

主な貢献と結果

• 非カルテジアン・ガード付きモデル: 本論文は、任意の終対象を持つカテゴリから出発して、木のトポスのアプローチを非カルテシアン設定へと一般化し、ガード付き再帰の圏論的モデルを構築する。
• リグ構造の保存: ベースとなるカテゴリ $C$ がダガー・リグカテゴリであれば、ガード付き構成 $C^\infty$ がリグ構造（テンソルおよび和型）を保存することが証明されている。これにより、ペアやリストのようなデータ型のモデル化が可能になる。
• ダガー可能な部分カテゴリ: 全体的な構成は本質的にダガーをサポートしていないことを論文は特定している。そこで、ダガーを持つ射を許容する部分カテゴリ $C^\infty_\dagger$ を導入する。$C^\infty_\dagger$ は、それ自体がダガー・リグカテゴリであることが示されている。
• 不動点の存在: 定理 3.12 は、局所縮小的な関手がパラメータ化された不動点を有することを示している。この結果は、可逆的な設定内でガード付き誘導型を解釈するために $C^\infty_\dagger$ に適用される。
• ガード付き対称パターンマッチングの意味論: 論文では、構築されたモデルを、高次の可逆プログラミング言語である「ガード付き対称パターンマッチング」の解釈に適用している。その意味論は以下をカバーする：
  • 基底型（ガード付き誘導型であるリストを含む）。
  • 可逆な部分関数のジョインによって定義される一次関数（isos）。
  • $S$ において濃化された単純型ガード付き $\lambda$-計算による高次関数。
  • 具体的な例として、量子制御操作、および量子ビットのリストに対する高次の量子フーリエ変換（QFT）の定義が含まれる。

意義と主張
本論文は、ガード付き再帰の有用性を、古典的なストリーム処理から可逆および量子プログラミングのパラダイムへと拡張することを主張している。ダガーカテゴリ（可逆プログラミング）と木のトポス（ガード付き再帰）を橋渡しすることで、著者は無限のデータ型をサポートする高次の可逆言語のためのデノテーション意味論を提供する。

著者は、この構成がダガー・リグカテゴリにおけるガード付き誘導型のモデリングという問題を解決している一方で、ヒルベルト空間が一般的な再帰を解釈できるかという、より広範な未解決の問いを解決するものではないことを明示的に述べている。その意義は、可逆的なプログラミング（ダガーカテゴリ）とガード付き再帰（木のトポス）の意味論を結合し、低レベルの回路記述に頼ることなく、複雑な量子アルゴリズム（QFTなど）を高次の可逆形式で定義できる、可逆言語のための健全な圏論的基礎を提供することにある。また、ダガーカテゴリにおけるストリームの意味論は、終対象のゼロ対象としての性質により標準的な極限構成が失敗するため、新しい理論を必要とするという点を、論文は謙虚に認めている。