論文の概要: Linear Dependent Type Theory for Quantum Programming Languages
- arxiv url: http://arxiv.org/abs/2004.13472v6
- Date: Tue, 6 Sep 2022 14:00:55 GMT
- ステータス: 処理完了
- システム内更新日: 2023-05-21 21:51:14.262476
- Title: Linear Dependent Type Theory for Quantum Programming Languages
- Title（参考訳）: 量子プログラミング言語のための線形依存型理論
- Authors: Peng Fu, Kohei Kishida, Peter Selinger
- Abstract要約: 現代の量子プログラミング言語は、量子資源と古典的な制御を統合している。
それらは量子資源の非閉性を反映するために線形型付けされなければならない。
高水準および実用的な言語は、第一級市民として量子回路もサポートすべきである。
- 参考スコア（独自算出の注目度）: 1.7166794984161973
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Modern quantum programming languages integrate quantum resources and
classical control. They must, on the one hand, be linearly typed to reflect the
no-cloning property of quantum resources. On the other hand, high-level and
practical languages should also support quantum circuits as first-class
citizens, as well as families of circuits that are indexed by some classical
parameters. Quantum programming languages thus need linear dependent type
theory. This paper defines a general semantic structure for such a type theory
via certain fibrations of monoidal categories. The categorical model of the
quantum circuit description language Proto-Quipper-M by Rios and Selinger
(2017) constitutes an example of such a fibration, which means that the
language can readily be integrated with dependent types. We then devise both a
general linear dependent type system and a dependently typed extension of
Proto-Quipper-M, and provide them with operational semantics as well as a
prototype implementation.
- Abstract（参考訳）: 現代の量子プログラミング言語は、量子資源と古典制御を統合する。
一方、それらは量子資源の非閉性を反映するために線形型付けされなければならない。
一方、高レベルで実用的な言語は量子回路を第一級市民としてサポートし、古典的なパラメータによってインデックス付けされる回路群もサポートすべきである。
したがって、量子プログラミング言語は線形依存型理論を必要とする。
本稿では、モノイド圏の特定のファイバーを通してそのような型理論の一般的な意味構造を定義する。
rios and selinger (2017) による量子回路記述言語proto-quipper-mの分類モデルは、そのようなフィブリケーションの例であり、これは言語が依存型と容易に統合できることを意味する。
次に、一般的な線形依存型システムとProto-Quipper-Mの依存型拡張の両方を考案し、それらの操作意味とプロトタイプ実装を提供する。
関連論文リスト
- Efficient Learning for Linear Properties of Bounded-Gate Quantum Circuits [63.733312560668274]
d可変RZゲートとG-dクリフォードゲートを含む量子回路を与えられた場合、学習者は純粋に古典的な推論を行い、その線形特性を効率的に予測できるだろうか?
我々は、d で線形にスケーリングするサンプルの複雑さが、小さな予測誤差を達成するのに十分であり、対応する計算の複雑さは d で指数関数的にスケールすることを証明する。
我々は,予測誤差と計算複雑性をトレードオフできるカーネルベースの学習モデルを考案し,多くの実践的な環境で指数関数からスケーリングへ移行した。
論文 参考訳（メタデータ） (2024-08-22T08:21:28Z) - Hybrid Quantum-Classical Machine Learning with String Diagrams [49.1574468325115]
本稿では,文字列ダイアグラムの観点からハイブリッドアルゴリズムを記述するための公式なフレームワークを開発する。
弦図の特筆すべき特徴は、量子古典的インタフェースに対応する関手ボックスの使用である。
論文 参考訳（メタデータ） (2024-07-04T06:37:16Z) - Categories of quantum cpos [0.0]
量子cposと呼ばれる$omega$-complete partial order (cpos)の非可換一般化が見つかる。
量子cposは将来の量子領域理論の バックボーンを形成します
論文 参考訳（メタデータ） (2024-06-03T22:13:32Z) - Quantum and Reality [0.0]
等変ホモトピー理論の原理に根ざしたエルミティシティの自然発生について述べる。
このエルミート形式の構成は、周囲線型型理論をテンソル単位型の負の単位項以上に必要としない。
LHoTTに埋め込まれた量子言語における量子ゲートと量子チャネルのユニタリティの符号化(および検証)を可能にする方法を示す。
論文 参考訳（メタデータ） (2023-11-18T11:00:12Z) - Circuit Width Estimation via Effect Typing and Linear Dependency (Long
Version) [1.3597551064547502]
本稿では,線形依存型・実効性を持つ回路記述言語Proto-Quipper-Rを提案する。
提案手法は現実的な量子アルゴリズムを検証するのに十分であることを示す。
論文 参考訳（メタデータ） (2023-10-29T18:10:31Z) - The Quantum Monadology [0.0]
関数型プログラミング言語の現代の理論は、計算サイドエフェクトとサイドコンテキストを符号化するためにモナドを使用する。
我々はGrothendieckの「操作のモチベーションヨガ」によって誘導されるパラメータ化モジュールスペクトルのカテゴリ上での(co)モナドの分析を行う。
本稿では、これらのモナディック量子効果を透明なdo-notationで表現したドメイン固有量子プログラミング言語(QS)を示す。
論文 参考訳（メタデータ） (2023-10-24T11:19:24Z) - A Framework for Demonstrating Practical Quantum Advantage: Racing
Quantum against Classical Generative Models [62.997667081978825]
生成モデルの一般化性能を評価するためのフレームワークを構築した。
古典的および量子生成モデル間の実用的量子優位性(PQA)に対する最初の比較レースを確立する。
以上の結果から,QCBMは,他の最先端の古典的生成モデルよりも,データ制限方式の方が効率的であることが示唆された。
論文 参考訳（メタデータ） (2023-03-27T22:48:28Z) - The Quantum Path Kernel: a Generalized Quantum Neural Tangent Kernel for
Deep Quantum Machine Learning [52.77024349608834]
古典的なディープニューラルネットワークの量子アナログを構築することは、量子コンピューティングにおける根本的な課題である。
鍵となる問題は、古典的なディープラーニングの本質的な非線形性にどのように対処するかである。
我々は、深層機械学習のこれらの側面を複製できる量子機械学習の定式化であるQuantum Path Kernelを紹介する。
論文 参考訳（メタデータ） (2022-12-22T16:06:24Z) - LQP: The Dynamic Logic of Quantum Information [77.34726150561087]
本稿では,複合量子システムにおける情報フローの推論のための動的論理形式について紹介する。
本稿では,この論理の文法,関係意味論,音響証明システムについて述べる。
アプリケーションとしては,テレポーテーションプロトコルと標準量子秘密共有プロトコルに対して,正式な正当性を与えるために,我々のシステムを利用する。
論文 参考訳（メタデータ） (2021-10-04T12:20:23Z) - A tutorial introduction to quantum circuit programming in dependently
typed Proto-Quipper [1.5274311118568713]
本稿では,線形依存型を持つ実験量子回路言語Proto-Quipper-Dを提案する。
本稿では,依存型が回路のプログラミングファミリを実現する方法と,依存型がガベージキュービットのタイプセーフ非計算の問題を解決する方法を示す。
論文 参考訳（メタデータ） (2020-05-17T23:31:23Z) - From a quantum theory to a classical one [117.44028458220427]
量子対古典的交叉を記述するための形式的アプローチを提示し議論する。
この手法は、1982年にL. Yaffeによって、大きな$N$の量子場理論に取り組むために導入された。
論文 参考訳（メタデータ） (2020-04-01T09:16:38Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。