Fugu-MT 論文翻訳(概要): Complete Quantum Relational Hoare Logics from Optimal Transport Duality

論文の概要: Complete Quantum Relational Hoare Logics from Optimal Transport Duality

arxiv url: http://arxiv.org/abs/2501.15238v1
Date: Sat, 25 Jan 2025 15:01:25 GMT
ステータス: 翻訳完了
システム内更新日: 2025-01-28 13:54:41.595494
Title: Complete Quantum Relational Hoare Logics from Optimal Transport Duality
Title（参考訳）: 最適輸送双対による完全量子関係ホア論理
Authors: Gilles Barthe, Minbo Gao, Theo Wang, Li Zhou,
Abstract要約: 量子プログラムに対する量的リレーショナル・ホア論理を導入する。我々の論理は健全であり、有界な後条件とほぼ確実に終了するプログラムに対して完備であることを示す。
参考スコア（独自算出の注目度）: 10.178285424205953
License:
Abstract: We introduce a quantitative relational Hoare logic for quantum programs. Assertions of the logic range over a new infinitary extension of positive semidefinite operators. We prove that our logic is sound, and complete for bounded postconditions and almost surely terminating programs. Our completeness result is based on a quantum version of the duality theorem from optimal transport. We also define a complete embedding into our logic of a relational Hoare logic with projective assertions.
Abstract（参考訳）: 量子プログラムに対する量的リレーショナル・ホア論理を導入する。論理の作用は、正半定値作用素の新たな無限拡張にまで及んでいる。我々の論理は健全であり、有界な後条件とほぼ確実に終了するプログラムに対して完備であることを示す。我々の完全性の結果は、最適輸送からの双対性定理の量子バージョンに基づいている。我々はまた、射影的なアサーションを持つリレーショナル・ホア論理のロジックに完全な埋め込みを定義する。

関連論文リスト

Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs [3.444844635251667]
確率的振る舞いに関する局所的推論のための新しい量子ホア論理を提案する。論理学における証明規則は意味論的意味論に関して健全であることを示す。結果として得られる論理フレームワークは、CoqQLRと呼ばれ、古典量子プログラムに関する半自動推論を容易にする。
論文参考訳（メタデータ） (2023-08-09T07:23:22Z)
Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs [6.2147758224415055]
フーア論理(ホーアりょうり、英: Hoare logic)は、コンピュータプログラムの静的解析において強力な手法である。完全な量子抽象解釈は、量子ホア論理と量子不正確な論理を誘導することを示す。
論文参考訳（メタデータ） (2022-06-28T05:49:55Z)
Birkhoff-von Neumann Quantum Logic as an Assertion Language for Quantum Programs [1.1878820609988696]
量子変数を持つ一階述語論理は、量子プログラムの様々な性質を特定し、推論するためのアサーション言語として必要とされる。本稿では,Birkhoff-von Neumann量子論理を量子変数上の普遍的および存在的量子化器を用いて一階拡張する。
論文参考訳（メタデータ） (2022-05-04T08:57:44Z)
Improved Quantum Algorithms for Fidelity Estimation [77.34726150561087]
証明可能な性能保証を伴う忠実度推定のための新しい,効率的な量子アルゴリズムを開発した。我々のアルゴリズムは量子特異値変換のような高度な量子線型代数技術を用いる。任意の非自明な定数加算精度に対する忠実度推定は一般に困難であることを示す。
論文参考訳（メタデータ） (2022-03-30T02:02:16Z)
LQP: The Dynamic Logic of Quantum Information [77.34726150561087]
本稿では,複合量子システムにおける情報フローの推論のための動的論理形式について紹介する。本稿では,この論理の文法,関係意味論,音響証明システムについて述べる。アプリケーションとしては,テレポーテーションプロトコルと標準量子秘密共有プロトコルに対して,正式な正当性を与えるために,我々のシステムを利用する。
論文参考訳（メタデータ） (2021-10-04T12:20:23Z)
The Logic of Quantum Programs [77.34726150561087]
本稿では,量子プログラムにおける情報フローの論理計算について述べる。特に、複素量子系における量子測定、ユニタリ進化、絡み合いを扱うことができる動的論理を導入する。
論文参考訳（メタデータ） (2021-09-14T16:08:37Z)
Realization of arbitrary doubly-controlled quantum phase gates [62.997667081978825]
本稿では,最適化問題における短期量子優位性の提案に着想を得た高忠実度ゲートセットを提案する。 3つのトランペット四重項のコヒーレントな多レベル制御を編成することにより、自然な3量子ビット計算ベースで作用する決定論的連続角量子位相ゲートの族を合成する。
論文参考訳（メタデータ） (2021-08-03T17:49:09Z)
Depth-efficient proofs of quantumness [77.34726150561087]
量子性の証明は、古典的検証器が信頼できない証明器の量子的利点を効率的に証明できる挑戦応答プロトコルの一種である。本稿では、証明者が量子回路を一定深度でしか実行できない量子性構成の証明を2つ与える。
論文参考訳（メタデータ） (2021-07-05T17:45:41Z)
A Quantum Interpretation of Bunched Logic for Quantum Separation Logic [22.507329566323982]
プリコンディションとポストコンディションは、量子状態を記述するBI式である。量子ワンタイムパッドとシークレット共有のセキュリティを証明するロジックを実践する。
論文参考訳（メタデータ） (2021-01-30T22:24:36Z)
Quantum Hoare logic with classical variables [3.1181601933418897]
古典変数と量子変数の両方を含む簡単な時相言語に対して量子ホア論理を提案する。古典量子状態とそれに対応するアサーションの新たな定義により、論理体系は非常に単純であり、古典的プログラムの伝統的なホア論理と類似している。
論文参考訳（メタデータ） (2020-08-15T23:56:18Z)
Foundations of Reasoning with Uncertainty via Real-valued Logics [70.43924776071616]
我々は、本質的にすべての実数値論理をカバーするためにパラメータ化できる、音と強完全公理化を与える。文のクラスは非常に豊かであり、各クラスは実数値論理の式の集合に対して可能な実値の集合を記述する。
論文参考訳（メタデータ） (2020-08-06T02:13:11Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。