論文の概要: Birkhoff-von Neumann Quantum Logic as an Assertion Language for Quantum
Programs
- arxiv url: http://arxiv.org/abs/2205.01959v1
- Date: Wed, 4 May 2022 08:57:44 GMT
- ステータス: 処理完了
- システム内更新日: 2023-02-14 09:17:00.824907
- Title: Birkhoff-von Neumann Quantum Logic as an Assertion Language for Quantum
Programs
- Title（参考訳）: 量子プログラムの補助言語としてのBirkhoff-von Neumann量子論理
- Authors: Mingsheng Ying
- Abstract要約: 量子変数を持つ一階述語論理は、量子プログラムの様々な性質を特定し、推論するためのアサーション言語として必要とされる。
本稿では,Birkhoff-von Neumann量子論理を量子変数上の普遍的および存在的量子化器を用いて一階拡張する。
- 参考スコア（独自算出の注目度）: 1.1878820609988696
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: A first-order logic with quantum variables is needed as an assertion language
for specifying and reasoning about various properties (e.g. correctness) of
quantum programs. Surprisingly, such a logic is missing in the literature, and
the existing first-order Birkhoff-von Neumann quantum logic deals with only
classical variables and quantifications over them. In this paper, we fill in
this gap by introducing a first-order extension of Birkhoff-von Neumann quantum
logic with universal and existential quantifiers over quantum variables.
Examples are presented to show our logic is particularly suitable for
specifying some important properties studied in quantum computation and quantum
information. We further incorporate this logic into quantum Hoare logic as an
assertion logic so that it can play a role similar to that of first-order logic
for classical Hoare logic and BI-logic for separation logic. In particular, we
show how it can be used to define and derive quantum generalisations of some
adaptation rules that have been applied to significantly simplify verification
of classical programs. It is expected that the assertion logic defined in this
paper - first-order quantum logic with quantum variables - can be combined with
various quantum program logics to serve as a solid logical foundation upon
which verification tools can be built using proof assistants such as Coq and
Isabelle/HOL.
- Abstract（参考訳）: 量子変数を持つ一階述語論理は、量子プログラムの様々な性質(例えば正しさ)を指定・推論するためのアサーション言語として必要である。
驚くべきことに、そのような論理は文献に欠落しており、既存の一階 birkhoff-von neumann 量子論理は古典変数とそれらの上での量子化のみを扱う。
本稿では,Birkhoff-von Neumann量子論理を量子変数上の普遍的および存在的量子化器で一階拡張することにより,このギャップを埋める。
例えば、量子計算や量子情報で研究されている重要な特性を特定するのに、論理が特に適していることを示す。
さらに、この論理を量子ホア論理にアサーション論理として組み込んで、古典ホア論理の1階述語論理や分離論理のBI論理と同じような役割を果たすようにした。
特に、古典プログラムの検証を大幅に単純化するために適用されたいくつかの適応規則の量子一般化を定義し、導出する方法を示す。
本論文で定義されているアサーション論理(量子変数を含む一階量子論理)は、様々な量子プログラム論理と組み合わせることで、coqやisabelle/holなどの証明アシスタントを用いて検証ツールを構築するための確立された論理基盤となることが期待される。
関連論文リスト
- BI-based Reasoning about Quantum Programs with Heap Manipulations [5.744265100221585]
ヒープ操作を伴う量子プログラミング言語Q While-hpのセマンティクスについて述べる。
我々は,意味を分離するための解釈を含む,BIスタイルの量子論理を開発する。
次に、この量子BIスタイルの論理をアサーション言語として採用し、ヒープ制御量子プログラムを推論する。
論文 参考訳（メタデータ） (2024-09-16T10:34:45Z) - Simple Tests of Quantumness Also Certify Qubits [69.96668065491183]
量子性の検定は、古典的検証者が証明者が古典的でないことを(のみ)証明できるプロトコルである。
我々は、あるテンプレートに従う量子性のテストを行い、(Kalai et al., 2022)のような最近の提案を捉えた。
すなわち、同じプロトコルは、証明可能なランダム性や古典的な量子計算のデリゲートといったアプリケーションの中心にあるビルディングブロックであるqubitの認定に使用できる。
論文 参考訳（メタデータ） (2023-03-02T14:18:17Z) - Abstract interpretation, Hoare logic, and incorrectness logic for
quantum programs [6.2147758224415055]
フーア論理(ホーアりょうり、英: Hoare logic)は、コンピュータプログラムの静的解析において強力な手法である。
完全な量子抽象解釈は、量子ホア論理と量子不正確な論理を誘導することを示す。
論文 参考訳（メタデータ） (2022-06-28T05:49:55Z) - On the Common Logical Structure of Classical and Quantum Mechanics [0.0]
量子論は、量子命題の完全な意味を適切に考慮すれば、古典的な分配性法則を満たすことを示す。
古典力学における統計命題の格子は同じ構造を辿り、古典命題の類似非可換部分格子が得られることを示す。
論文 参考訳（メタデータ） (2022-06-21T18:31:53Z) - Entanglement and coherence in Bernstein-Vazirani algorithm [58.720142291102135]
Bernstein-Vaziraniアルゴリズムは、オラクルに符号化されたビット文字列を決定できる。
我々はベルンシュタイン・ヴァジラニアルゴリズムの量子資源を詳細に分析する。
絡み合いがない場合、初期状態における量子コヒーレンス量とアルゴリズムの性能が直接関係していることが示される。
論文 参考訳（メタデータ） (2022-05-26T20:32:36Z) - 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) - 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) - Secure Two-Party Quantum Computation Over Classical Channels [63.97763079214294]
古典的アリス(Alice)と量子的ボブ(Quantum Bob)が古典的なチャネルを通してのみ通信できるような設定を考える。
悪質な量子逆数の場合,ブラックボックスシミュレーションを用いた2次元量子関数を実現することは,一般に不可能であることを示す。
我々は、QMA関係Rの古典的量子知識(PoQK)プロトコルを入力として、古典的当事者によって検証可能なRのゼロ知識PoQKを出力するコンパイラを提供する。
論文 参考訳（メタデータ） (2020-10-15T17:55:31Z) - Quantum Hoare logic with classical variables [3.1181601933418897]
古典変数と量子変数の両方を含む簡単な時相言語に対して量子ホア論理を提案する。
古典量子状態とそれに対応するアサーションの新たな定義により、論理体系は非常に単純であり、古典的プログラムの伝統的なホア論理と類似している。
論文 参考訳（メタデータ） (2020-08-15T23:56:18Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。