技術要約: Granthi: ユニット演算による高階量子プログラミング

1. 問題提起

既存の量子プログラミング言語は、高階構造（関数、制御抽象、プログラム生成器）が完全に古典的なホスト言語側に存在し、量子レイヤーは量子ビットやレジスタに対する一次的な操作に限定されるという、分離されたアーキテクチャを採用するのが一般的である。この設計は、量子プログラム自体に対する抽象化を制限している。すなわち、量子値を変数として渡したり、結果として返したり、あるいは高階構成要素の中で合成したりすることができない。

さらに、古典的なデータ抽象メカニズム（パターンマッチング、ケース解析、反復）は、未使用の選択肢を破壊的に検査・破棄することに依存しており、これは制御フローの崩壊を招く。これらの原理は、純粋なユニタリ設定とは相容れない。なぜなら、量子設定では、プログラムの振る舞いを不可逆的に変化させることなく、データを自由に検査したり、コピーしたり、破棄したりすることはできないからである。その結果、純粋なユニタリ意味論を維持しつつ、静的な回路へとコンパイル可能な、真の高階コヒーレント制御（量子スイッチなど）をサポートするプログラミング言語が存在しない。

2. 手法

本論文では、以下の3つのコアとなる設計上のコミットメントに基づいた、純粋なユニタリ高階量子プログラミング言語であるGranthiを提示する。

1. 第一級量子プログラム: 量子プログラムは第一級の値であり、渡すこと、返すこと、およびコヒーレントに合成することが可能である。
2. タグ保存ルーティング: 加法的構造は、観測的な分岐ではなく、タグ保存型のルーティングとして定義される。これにより、状態を崩壊させることなく、制御を重ね合わせの中に留めることができる。
3. 有限ラベル型: プログラマー向けの有限ラベル型は、名前付きの可逆操作を備えたドメインレベルの制御空間を提供し、これらは再帰型や表現の隠蔽を持たない平坦な $n$ 元和へと精緻化される。

コア言語と意味論

• 線形 $\lambda$-計算の基礎: コアは、テンソル積 ($\otimes$)、コヒーレント和 ($\oplus$)、および線形関数空間 ($\multimap$) を持つ線形 $\lambda$-計算である。基底型 $\mathbb{b}$ は一次元のシードであり、有限次元のシステムはコヒーレント和（例：$QBool := \mathbb{b} \oplus \mathbb{b}$）として構築される。
• 境界ユニタリ性: 中心的な意味論的革新は「境界ビュー（boundary view）」である。型 $A \multimap B$ の項は、構造化されたインターフェースを持つ開いた回路の断片として扱われる。適用は、リソースを消費する簡約ステップではなく、結合構造（配線インターフェース）として解釈される。型付けされたすべての項は、その境界インターフェース上のユニタリ演算子を表す。
• 正規化と決定性: 言語は $\beta/\eta$-安定な規律を強制する。システムは、すべての閉じた型付け済み項が定義上の等価性を除いて一意の正規形を持つことを証明し、これにより、ソースレベルの再配置（正規化）がコンパイルされたユニタリ回路を変更しないことを保証する。
• 量子拡張: コアは、証明された対合（自己逆演算子）と、行列指数関数 ($e^{i\theta J}$) を通じて連続的なユニタリ族を生成する項構成子 Exp によって拡張されている。これにより、測定や混合状態を導入することなく、位相シフトや制御操作が可能となる。

コンパイル

Granthiシステムは、エンドツーエンドのコンパイラを実装している。

1. 精緻化（Elaboration）: 表層プログラム（OCaml DSLで記述）は、バインダーフリーのコアIRへと精緻化される。
2. 回路生成: コンパイラは、ユニタリ境界の配線を、pytket バックエンドを用いた物理的な量子ビットレイアウト上の静的な量子回路として実現する。
3. ワイヤレイアウト: コンパイラは、タグレジスタと共有ペイロードバンドルを含む和型のための特定のワイヤエンコーディングを使用する。構造的同型（結合律、対称律、分配律）は、ゲートを一切伴わない純粋なワイヤ置換へとコンパイルされる。一方、コヒーレント制御構成（case など）は、タグレジスタに対して作用する制御ゲートへとコンパイルされる。

3. 主な貢献

• 高階ユニタリ意味論: Granthiは、高階構造が古典的なホストに限定されるのではなく、量子レイヤー自体に内在しているプログラミング言語の初の事例を提供する。これは、高階の可逆性が、閉じられたデータから露出したインターフェースへと転置された通常のユニタリ性であることを示している。
• 合成に対するコヒーレント制御: 言語は、量子スイッチを定義可能な項としてサポートする。スイッチは、2つの演算の合成順序を重ね合わせの中に置くものであり、これが静的な回路へとコンパイルされることは、このような高階の効果がプログラマブルであり、物理的に実現可能であることを証明している。
• 制御フロー上の干渉: 言語は、制御フローの履歴に対する干渉（例：位相マーキングを伴う可逆的なショートサーキット論理積）をサポートする。これは古典的なアナロジーを持たない現象であるが、明示的な証拠ワイヤをスレッドし、観測することなく特定のブランチに位相を適用することで実現される。
• 有限制御データ型: システムは、名前付きの可逆操作を備えた、プログラマー向けの有限ラベル型（例：巡回群 $\mathbb{Z}_5$）を導入している。これらはコアの和と配線のメカニズムへと精緻化され、ドメイン固有の制御空間（例：群コヒーレントなパターンマッチング）が効率的にコンパイルされる（例：$n$ 元和のディスパッチに対して $O(\log n)$ ゲート）。
• 形式的保証: 本論文は、正規化、決定性、および境界ユニタリ性の定理を確立している。コンパイルされた回路が、レイアウト同型を通じて転送された意味論的ユニタリと等しいことを、バックエンドのプリミティブの正当性を仮定した上で証明している。

4. 結果

著者らは、pytket をターゲットとする Python コンパイラを備えた OCaml DSL として Granthi を実装した。プロトタイプは以下の例で検証された。

• 量子スイッチ: 実行例は、因果的順序の重ね合わせを実現する8量子ビットの静的回路へとコンパイルされる。
• 制御演算: 一様制御適用および $n$ 元制御ディスパッチ（例：SELECT コンビネータ）が実装され、効率的なゲート数（例：$n$ 元和に対する $O(\log n)$ タグ反転）が示された。
• 標準アルゴリズム: システムは、Deutsch–Jozsa、隠部分群、Simon、Bell、およびGHZ状態を含む標準的なアルゴリズムを正常にコンパイルし、検証した。
• ゲートコスト分析: 実装により、乗法的および構造的操作はゼロゲート（純粋な配線）にコンパイルされる一方で、量子プリミティブとコヒーレント制御構成は必要なゲートを導入することが確認された。例えば、量子スイッチは $2 + 2(|f| + |g|)$ 個のゲートへとコンパイルされる。

5. 意義と範囲

本論文は、測定や古典的フィードバックから独立した、高階抽象化を研究するための規律あるユニタリコアとして Grathi を位置づけている。

• 範囲: Granthi は、すべての型付け済み項が境界ユニタリを表し、静的な回路へとコンパイルされるという不変量を維持するために、測定、混合状態、古典的フィードバック、および再帰型を意図的に除外している。
• ポジショニング: Granthi は、高階構造をホストではなくオブジェクト言語内に配置するという点で、既存の言語（Quipper や Q# など）とは異なる。また、一般的な直交性判定に依存する Qunity とは異なり、加法的型構造の中に直交性を組み込んでいる。
• 今後の方向性: 著者らは、完全な量子プログラミングシステムには、測定、混合状態の意味論、およびより豊かなデータ抽象化を含むようにコアを拡張する必要があることを認めている。Granthi は、ハードウェアの制約や測定の効果が導入される前に、量子プログラムがどのように構造化されるべきかを理解するための基礎的なステップとして提供されている。

要約すると、Granthi は、制御フロー自体が干渉に参加できる、純粋なユニタリの枠組みの中で、高階の量子制御が物理的に意味を持ち、かつプログラマブルであることを実証している。