論文の概要: Refinement calculus of quantum programs with projective assertions
- arxiv url: http://arxiv.org/abs/2311.14215v1
- Date: Thu, 23 Nov 2023 22:12:57 GMT
- ステータス: 処理完了
- システム内更新日: 2023-11-27 16:14:03.136313
- Title: Refinement calculus of quantum programs with projective assertions
- Title(参考訳): 射影アサーションをもつ量子プログラムの精製計算
- Authors: Yuan Feng, Li Zhou, Yingte Xu
- Abstract要約: 本稿では,量子プログラムに適した微積分法を提案する。
まず、量子内における非決定論的プログラムの部分的正当性について検討する。
また,ポストコンディションを最も弱いリベラルなポストコンディションに変換する際のセマンティクスも提示する。
- 参考スコア(独自算出の注目度): 5.151896714190243
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Refinement calculus provides a structured framework for the progressive and
modular development of programs, ensuring their correctness throughout the
refinement process. This paper introduces a refinement calculus tailored for
quantum programs. To this end, we first study the partial correctness of
nondeterministic programs within a quantum while language featuring
prescription statements. Orthogonal projectors, which are equivalent to
subspaces of the state Hilbert space, are taken as assertions for quantum
states. In addition to the denotational semantics where a nondeterministic
program is associated with a set of trace-nonincreasing super-operators, we
also present their semantics in transforming a postcondition to the weakest
liberal postconditions and, conversely, transforming a precondition to the
strongest postconditions. Subsequently, refinement rules are introduced based
on these dual semantics, offering a systematic approach to the incremental
development of quantum programs applicable in various contexts. To illustrate
the practical application of the refinement calculus, we examine examples such
as the implementation of a $Z$-rotation gate, the repetition code, and the
quantum-to-quantum Bernoulli factory. Furthermore, we present Quire, a
Python-based interactive prototype tool that provides practical support to
programmers engaged in the stepwise development of correct quantum programs.
- Abstract(参考訳): リファインメント解析は、プログラムの進歩的かつモジュラーな開発のための構造化フレームワークを提供し、リファインメントプロセスを通してその正確性を保証する。
本稿では,量子プログラムに適した精細化計算法を提案する。
この目的のために、まず、処方文を含む言語において、量子内での非決定論的プログラムの部分的正当性について検討する。
状態ヒルベルト空間の部分空間と等価な直交射影は、量子状態のアサーションとして扱われる。
非決定論的プログラムがトレース非インクリエーションスーパーオペレータのセットに関連付けられる記述的意味論に加えて、ポスト条件を最も弱いリベラルなポスト条件に変換し、逆にプリコンを最強ポスト条件に変換する意味論も提示する。
その後、これらの双対意味論に基づいて洗練規則を導入し、様々な文脈で適用可能な量子プログラムの漸進的開発に体系的なアプローチを提供する。
精錬計算の実際的な応用例を示すために,$z$回転ゲートの実装,反復コード,量子から量子へのベルヌーイ工場などについて検討する。
さらに,正しい量子プログラムのステップワイズ開発に携わるプログラマに実用的なサポートを提供する,pythonベースのインタラクティブプロトタイプツールquireを提案する。
関連論文リスト
- Near-Term Distributed Quantum Computation using Mean-Field Corrections
and Auxiliary Qubits [77.04894470683776]
本稿では,限られた情報伝達と保守的絡み合い生成を含む短期分散量子コンピューティングを提案する。
我々はこれらの概念に基づいて、変分量子アルゴリズムの断片化事前学習のための近似回路切断手法を作成する。
論文 参考訳(メタデータ) (2023-09-11T18:00:00Z) - QbC: Quantum Correctness by Construction [4.572433350229651]
提案するQuantum Correctness by Construction (QbC) は,その仕様から量子プログラムを構築するための手法である。
プリコンディションとポストコンディションを使用してプログラム特性を規定し、その仕様から量子状態におけるプログラム構築のための音質および完全改善ルールを提案する。
このアプローチは、プログラムの詳細を導出する方法を自然に提案し、その過程で重要な設計上の選択を強調します。
論文 参考訳(メタデータ) (2023-07-28T16:00:57Z) - Verification of Nondeterministic Quantum Programs [1.9302781323430196]
非決定論的選択は、実装の詳細を指定せずにプログラムの振る舞いを記述する方法を提供する有用なプログラム構成である。
非決定性は量子プログラミングにも導入され、非決定性量子プログラムの終了は広く分析されてきた。
論文 参考訳(メタデータ) (2023-02-15T22:37:23Z) - Modularized and scalable compilation for quantum program in double
quantum dots [0.0]
我々は、Ansatz回路をトレーニングし、半導体二重量子ドットにおける一重項量子ビットに対する一連の普遍量子ゲートの高忠実度コンパイルを実現する。
我々の研究は、先進的で複雑な量子アルゴリズムのために、この物理資源の可能性を活用するための重要な足掛かりとなっている。
論文 参考訳(メタデータ) (2022-11-10T02:32:39Z) - Differentiable Quantum Programming with Unbounded Loops [10.648855845619705]
非有界ループを持つ最初の微分可能な量子プログラミングフレームワークを提供する。
非有界ループの微分における無限和を扱う導関数に対するランダム化推定器を導入する。
いくつかのパラメータ化量子アプリケーションに対する近接最適パラメータの自動同定に,我々のフレームワークのエキサイティングな応用を紹介した。
論文 参考訳(メタデータ) (2022-11-08T19:07:06Z) - Circuit Symmetry Verification Mitigates Quantum-Domain Impairments [69.33243249411113]
本稿では,量子状態の知識を必要とせず,量子回路の可換性を検証する回路指向対称性検証を提案する。
特に、従来の量子領域形式を回路指向安定化器に一般化するフーリエ時間安定化器(STS)手法を提案する。
論文 参考訳(メタデータ) (2021-12-27T21:15:35Z) - Realization of arbitrary doubly-controlled quantum phase gates [62.997667081978825]
本稿では,最適化問題における短期量子優位性の提案に着想を得た高忠実度ゲートセットを提案する。
3つのトランペット四重項のコヒーレントな多レベル制御を編成することにより、自然な3量子ビット計算ベースで作用する決定論的連続角量子位相ゲートの族を合成する。
論文 参考訳(メタデータ) (2021-08-03T17:49:09Z) - QuaSiMo: A Composable Library to Program Hybrid Workflows for Quantum
Simulation [48.341084094844746]
本稿では、ハイブリッド量子/古典的アルゴリズムの開発と量子シミュレーションへの応用のための構成可能な設計手法を提案する。
ハードウェアに依存しないQCORをQuaSiMoライブラリに実装する。
論文 参考訳(メタデータ) (2021-05-17T16:17:57Z) - Facial Expression Recognition on a Quantum Computer [68.8204255655161]
量子機械学習手法を用いて表情認識の可能な解を示す。
適切に定義された量子状態の振幅に符号化されたグラフの隣接行列を操作する量子回路を定義する。
論文 参考訳(メタデータ) (2021-02-09T13:48:00Z) - Composable Programming of Hybrid Workflows for Quantum Simulation [48.341084094844746]
本稿では、ハイブリッド量子/古典的アルゴリズムの開発と量子シミュレーションへの応用のための構成可能な設計手法を提案する。
ハードウェアに依存しないQCORをQuaSiMoライブラリに実装する。
論文 参考訳(メタデータ) (2021-01-20T14:20:14Z) - On the Principles of Differentiable Quantum Programming Languages [13.070557640180004]
変分量子回路(VQC)は、最も重要な短期量子応用の1つであると予測されている。
本稿では,量子回路における自己微分法の最初の形式化を提案する。
論文 参考訳(メタデータ) (2020-04-02T16:46:13Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。