論文の概要: A quantum let within the lambda calculus
- arxiv url: http://arxiv.org/abs/2608.29380v1
- Date: Sat, 29 Aug 2026 17:38:37 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-01 18:31:30.947839
- Title: A quantum let within the lambda calculus
- Title（参考訳）: ラムダ計算における量子レター
- Abstract要約: Selinger と Valiron の業績以来、量子計算の標準設計はプログラムの外で量子状態を維持してきた。
この設定ではテンソル除去が可能であることを示す。
量子テレポーテーションと3ビットビットフリップ符号による構成性について述べる。
- 参考スコア（独自算出の注目度）: 45.88028371034407
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Since the seminal work of Selinger and Valiron, the standard design for quantum lambda calculi has kept the quantum state outside the program: terms manipulate pointers to an external register. This is largely due to the difficulty of eliminating tensor products. For example, the calculus $λ_ρ^\circ$ embeds density matrices directly within terms, where terms carry the entire computation state, a feature particularly appealing for program verification. However, lacking a tensor elimination construct, it can neither access the individual qubits of a compound state nor discard them. Borgna showed that this inability to discard qubits makes the calculus strictly less expressive than the quantum lambda calculus of Selinger and Valiron. In this paper we show that tensor elimination is possible in this setting. The key observation is that the Pauli decomposition, combined with the spectral decomposition of the Pauli matrices, allows any $n$-qubit density matrix to be expressed as a real linear combination of tensor products of single-qubit density matrices. Exploiting this fact, we extend $λ_ρ^\circ$ with a construct $\mathrm{let}\ x^{\otimes n} = ρ \mathrm{in}\ t$, which binds each $x_i$ to a single-qubit density matrix arising from the decomposition of $ρ$. We equip the extended calculus with a rewrite system, a type system, and a denotational semantics, and prove Subject Reduction, Progress, Strong Normalisation, Soundness, and Adequacy. The new construct also recovers the missing ability to discard qubits, thereby restoring expressiveness. Moreover, we show that this is achieved in a physically principled way: a variable unused in $t$ is interpreted exactly as being partial-traced out, as dictated by the no-deleting theorem. We illustrate the resulting compositionality through quantum teleportation and the three-qubit bit-flip code.
- Abstract（参考訳）: Selinger と Valiron のセミナルな研究以来、量子ラムダ計算の標準的な設計は、量子状態をプログラムの外に保持してきた。
これは主にテンソル生成物の除去が難しいためである。
例えば、$λ_ρ^\circ$は密度行列を直接項内に埋め込む。
しかし、テンソル除去構造が欠如しているため、複合状態の個々の量子ビットにアクセスすることも、それらを捨てることもできない。
ボルグナは、この量子ビットを捨てることができないことが、スリンガーとヴァリロンの量子ラムダ計算よりも厳密に表現力に欠けることを示した。
本稿では,この設定でテンソル除去が可能であることを示す。
鍵となる観察は、パウリ分解とパウリ行列のスペクトル分解を組み合わせることで、任意の$n$量子密度行列を1量子密度行列のテンソル積の実線型結合として表現できるということである。
この事実を露呈すると、$λ_ρ^\circ$ は構成 $\mathrm{let}\ x^{\otimes n} = ρ \mathrm{in}\ t$ で拡張される。
我々は、拡張計算に書き直しシステム、型システム、意味論を装備し、主観的削減、進歩、強正規化、健全性、妥当性を証明する。
新しい構造体はまた、クォービットを破棄する能力の欠如を回復し、表現性を回復する。
さらに、これは物理的に原則化された方法で達成されることを示す:$t$で未使用の変数は、非削除定理によって規定されるように、正確には部分トラスアウトであると解釈される。
量子テレポーテーションと3ビットビットフリップ符号による構成性について述べる。
関連論文リスト
- Two-Tower Quantum Matrix Chain Multiplication: Trading Qubits for Depth [73.08853228981701]
行列連鎖乗法は、科学計算、機械学習、グラフ解析における問題である。
我々は、$K$行列の$mathcalW$を回路深さの量子状態にエンコードする量子サブルーチンであるemphTwo-Tower Matrixを提案する。
論文 参考訳（メタデータ） (2026-07-14T18:42:40Z) - From Hilbert's Tenth Problem to Quantum Speedup: Explicit Oracles for Bounded Diophantine Systems [0.0]
我々は、有界整数領域上のディオファント方程式を解くために、完全に可逆的なアルゴリズムフレームワークを導入する。
抽象ブラックボックスの仮定を超えて、この明示的なアーキテクチャ合成は、必要な量子演算が有界なオーバーヘッドとして働くことを保証している。
論文 参考訳（メタデータ） (2026-05-13T18:01:01Z) - Explicit Quantum Circuits for Simulating Linear Differential Equations via Dilation [0.0]
本稿では,拡張形式と明示的な量子回路構成を結合する具体的なパイプラインを提案する。
解析面では、量子実装に適した連続拡張作用素の離散化を導入する。
得られたスキームは、指数関数的に小さな境界効果まで、オーダー$O(M-3/2)$の大域的誤差境界を達成することを証明した。
論文 参考訳（メタデータ） (2025-09-20T18:54:49Z) - BELT: Block Encoding of Linear Transformation on Density Matrices [6.803593864509459]
Blockを紹介します。
任意の線形写像をシミュレートする体系的プロトコルであるBELT (Linear Transformation) の$。
BELTはコヒーレント量子進化を通じて$mathcalN(rho)$に関する情報の操作と抽出を可能にする。
BELTはエンタングルメント検出、量子チャネル反転、擬微分作用素に応用している。
論文 参考訳（メタデータ） (2025-08-18T11:54:40Z) - Learning finitely correlated states: stability of the spectral reconstruction [1.9573380763700716]
未知の状態のコピーから最小次元の実現を学習する作業を考える。
無限鎖上の有限相関変換不変状態に対して、最小次元の実現は再構成できる。
論文 参考訳（メタデータ） (2023-12-12T18:47:12Z) - The $\mathfrak S_k$-circular limit of random tensor flattenings [1.2891210250935143]
置換群代数上のアマルガメーションを持つ作用素値円系への収束を示す。
応用として、ボゾン量子状態の大きなランダム密度行列の法則を記述する。
論文 参考訳（メタデータ） (2023-07-21T08:59:33Z) - Vectorization of the density matrix and quantum simulation of the von
Neumann equation of time-dependent Hamiltonians [65.268245109828]
我々は、von-Neumann方程式を線形化するための一般的なフレームワークを開発し、量子シミュレーションに適した形でレンダリングする。
フォン・ノイマン方程式のこれらの線型化のうちの1つは、状態ベクトルが密度行列の列重ね元となる標準的な場合に対応することを示す。
密度行列の力学をシミュレートする量子アルゴリズムを提案する。
論文 参考訳（メタデータ） (2023-06-14T23:08:51Z) - Quantifying nonstabilizerness of matrix product states [0.0]
我々は,最近導入された安定化器R'enyiエントロピー(SREs)によって定量化された非安定化器性が,行列積状態(MPSs)に対して効率的に計算可能であることを示す。
我々はこの観測を利用して量子イジング鎖における基底状態の非安定化の研究を再考し、より大きなシステムサイズまで正確な数値結果を提供する。
論文 参考訳（メタデータ） (2022-07-26T17:50:32Z) - A lower bound on the space overhead of fault-tolerant quantum computation [51.723084600243716]
しきい値定理は、フォールトトレラント量子計算の理論における基本的な結果である。
振幅雑音を伴う耐故障性量子計算の最大長に対する指数的上限を証明した。
論文 参考訳（メタデータ） (2022-01-31T22:19:49Z) - Sub-bosonic (deformed) ladder operators [62.997667081978825]
ファジィネスという厳密な概念から派生した変形生成および消滅作用素のクラスを提示する。
これにより変形し、ボゾン準可換関係は、修正された退化エネルギーとフォック状態を持つ単純な代数構造を誘導する。
さらに、量子論において導入された形式論がもたらす可能性について、例えば、自由準ボソンの分散関係における線型性からの偏差について検討する。
論文 参考訳（メタデータ） (2020-09-10T20:53:58Z) - Quantum Gram-Schmidt Processes and Their Application to Efficient State
Read-out for Quantum Algorithms [87.04438831673063]
本稿では、生成した状態の古典的ベクトル形式を生成する効率的な読み出しプロトコルを提案する。
我々のプロトコルは、出力状態が入力行列の行空間にある場合に適合する。
我々の技術ツールの1つは、Gram-Schmidt正則手順を実行するための効率的な量子アルゴリズムである。
論文 参考訳（メタデータ） (2020-04-14T11:05:26Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。