論文の概要: 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を提案する。
関連論文リスト
- Quantum Homogenization as a Quantum Steady State Protocol on NISQ Hardware [42.52549987351643]
量子ホモジェナイゼーション(quantum homogenization)は、貯水池に基づく量子状態近似プロトコルである。
我々は、標準的な量子同化プロトコルを、動的に等価(mathttSWAP$)$alpha$の定式化に拡張する。
提案プロトコルは,コード部分空間の修正が可能な完全正のトレース保存(CPTP)マップを生成する。
論文 参考訳（メタデータ） (2024-12-19T05:50:54Z) - Design and synthesis of scalable quantum programs [0.8007726207322294]
任意のサイズと複雑さの量子プログラムを作成するためのスケーラブルで堅牢なアプローチを提案する。
量子プログラムは、最終プログラム上の制約と目的とともに、ハイレベルモデルの観点から表現される。
この技術は電子設計の自動化手法を量子コンピューティングに適用し、事実上無限の機能空間で実現可能な実装を見つける。
論文 参考訳（メタデータ） (2024-12-10T10:12:03Z) - Qrisp: A Framework for Compilable High-Level Programming of Gate-Based Quantum Computers [0.52197339162908]
ハイレベルプログラミングパラダイムと量子ハードウェアのギャップを埋めるために設計されたフレームワークであるQrispを紹介する。
Qrispの特長は、プログラムを回路レベルにコンパイルし、既存の物理バックエンドで実行可能にすることである。
論文 参考訳（メタデータ） (2024-06-20T23:40:22Z) - Near-Term Distributed Quantum Computation using Mean-Field Corrections
and Auxiliary Qubits [77.04894470683776]
本稿では,限られた情報伝達と保守的絡み合い生成を含む短期分散量子コンピューティングを提案する。
我々はこれらの概念に基づいて、変分量子アルゴリズムの断片化事前学習のための近似回路切断手法を作成する。
論文 参考訳（メタデータ） (2023-09-11T18:00:00Z) - Semidefinite programming relaxations for quantum correlations [42.72938925647165]
量子相関論において、半定緩和のコアアイデアがどのように様々な研究トピックに適用できるかを論じる。
これらのトピックには、非局所性、量子通信、量子ネットワーク、絡み合い、量子暗号が含まれる。
論文 参考訳（メタデータ） (2023-07-05T18:00:07Z) - Verification of Nondeterministic Quantum Programs [1.9302781323430196]
非決定論的選択は、実装の詳細を指定せずにプログラムの振る舞いを記述する方法を提供する有用なプログラム構成である。
非決定性は量子プログラミングにも導入され、非決定性量子プログラムの終了は広く分析されてきた。
論文 参考訳（メタデータ） (2023-02-15T22:37:23Z) - Differentiable Quantum Programming with Unbounded Loops [10.648855845619705]
非有界ループを持つ最初の微分可能な量子プログラミングフレームワークを提供する。
非有界ループの微分における無限和を扱う導関数に対するランダム化推定器を導入する。
いくつかのパラメータ化量子アプリケーションに対する近接最適パラメータの自動同定に,我々のフレームワークのエキサイティングな応用を紹介した。
論文 参考訳（メタデータ） (2022-11-08T19:07:06Z) - 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) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。