論文の概要: On Abstract Machine Semantics for Proto-Quipper-M

• arxiv url: http://arxiv.org/abs/2105.03522v1
• Date: Fri, 7 May 2021 22:16:11 GMT
• ステータス: 処理完了
• システム内更新日: 2023-04-01 05:28:39.431684
• Title: On Abstract Machine Semantics for Proto-Quipper-M
• Title（参考訳）: プロト・クイッパー-Mの抽象機械意味論について
• Authors: Andrea Colledan
• Abstract要約: クニッパー(Quipper)は、量子回路を記述するためのドメイン固有プログラミング言語である。 Haskellの組み込み言語として実装されているので、Quipperは非常に実用的な関数型言語です。 Haskellには線形型がないため、量子状態の非閉性に反するQuipperプログラムを書くのは容易である。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Quipper is a domain-specific programming language for the description of quantum circuits. Because it is implemented as an embedded language in Haskell, Quipper is a very practical functional language. However, for the same reason, it lacks a formal semantics and it is limited by Haskell's type system. In particular, because Haskell lacks linear types, it is easy to write Quipper programs that violate the non-cloning property of quantum states. In order to formalize relevant fragments of Quipper in a type-safe way, the Proto-Quipper family of research languages has been introduced over the last years. In this paper we first review Proto-Quipper-M, an instance of the Proto-Quipper family based on a categorical model for quantum circuits, which features a linear type system that guarantees that the non-cloning property holds at compile time. We then derive a tentative small-step operational semantics from the big-step semantics of Proto-Quipper-M and we prove that the two are equivalent. After proving subject reduction and progress results for the tentative semantics, we build upon it to obtain a truly small-step semantics in the style of an abstract machine, which we eventually prove to be equivalent to the original semantics.
• Abstract（参考訳）: quipperは量子回路を記述するためのドメイン固有プログラミング言語である。 Haskellの組み込み言語として実装されているので、Quipperは非常に実用的な関数型言語です。 しかし、同じ理由で形式的な意味論が欠けており、Haskellの型システムによって制限されている。 特に、Haskellには線形型がないため、量子状態の非閉性に反するQuipperプログラムを書くのは容易である。 タイプセーフな方法でQuipperの関連するフラグメントを形式化する目的で、Proto-Quipperファミリーの研究言語がここ数年にわたって導入されてきた。 本稿では, 量子回路のカテゴリモデルに基づくProto-Quipper-Mのインスタンスとして, 非閉鎖特性がコンパイル時に保持されることを保証する線形型システムを提案する。 次に、Proto-Quipper-Mのビッグステップ意味論から仮の小さな操作意味論を導き、両者が等価であることを証明する。 仮意味論の主題の縮小と進歩の結果を証明した後、抽象機械のスタイルで真に小さな意味論を得るように構築し、最終的に元の意味論と同値であることが証明される。

関連論文リスト

• Dictionary Learning Improves Patch-Free Circuit Discovery in Mechanistic Interpretability: A Case Study on Othello-GPT [59.245414547751636]
  本稿では,アクティベーションパッチに代わる回路発見フレームワークを提案する。 当社のフレームワークはアウト・オブ・ディストリビューション(out-of-distribution)に悩まされており、複雑さの観点からより効率的であることが証明されています。 我々はOthelloという名前の合成タスクで訓練された小さなトランスフォーマーを掘り下げ、その内部に人間に理解可能な微細な回路がいくつかある。
  論文  参考訳（メタデータ） (2024-02-19T15:04:53Z)
• Chain of Code: Reasoning with a Language Model-Augmented Code Emulator [115.16975276693267]
  我々は、LMコード駆動推論を改善するシンプルながら驚くほど効果的な拡張であるChain of Codeを提案する。 キーとなるアイデアは、プログラム内のセマンティックなサブタスクを、インタープリタが明示的にキャッチできるフレキシブルな擬似コードとしてフォーマットすることを、LMに促すことである。
  論文  参考訳（メタデータ） (2023-12-07T17:51:43Z)
• LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers [60.009969929857704]
  論理的推論は、科学、数学、社会に潜在的影響を与える可能性のある人工知能にとって重要なタスクである。 本研究では、LINCと呼ばれるモジュール型ニューロシンボリックプログラミングのようなタスクを再構成する。 我々は,FOLIOとProofWriterのバランスの取れたサブセットに対して,ほぼすべての実験条件下で,3つの異なるモデルに対して顕著な性能向上を観察した。
  論文  参考訳（メタデータ） (2023-10-23T17:58:40Z)
• OrdinalCLIP: Learning Rank Prompts for Language-Guided Ordinal Regression [94.28253749970534]
  我々は、リッチなセマンティックCLIP潜在空間からランクの概念を学ぶことを提案する。 OrdinalCLIPは学習可能なコンテキストトークンと学習可能なランク埋め込みで構成されている。 実験結果から,本パラダイムは一般順序回帰タスクにおける競合性能を達成できることが示唆された。
  論文  参考訳（メタデータ） (2022-06-06T03:54:53Z)
• A Paradigm Change for Formal Syntax: Computational Algorithms in the Grammar of English [0.0]
  私たちは、プログラム言語を、プロセスベースの英語構文のモデルにします。 機能語と内容語の組み合わせをモデリングのトピックとして選んだ。 モデルの適合性は、アルゴリズムに不可欠な3つの機能特性を導出し、英語文法におけるそれらの存在を確認することによって検証された。
  論文  参考訳（メタデータ） (2022-05-24T07:28:47Z)
• Proto-Quipper with dynamic lifting [1.5274311118568713]
  我々は、Quipper に存在する Dynamic lifting という構造で Proto-Quipper-M を拡張する。 動的リフトにより、Proto-Quipperプログラムは古典的および量子計算をインターリーブすることができる。
  論文  参考訳（メタデータ） (2022-04-27T16:34:15Z)
• On Dynamic Lifting and Effect Typing in Circuit Description Languages (Extended Version) [0.0]
  本稿では,量子回路記述言語Quipperの中核となる特徴をモデル化したパラダイム計算Proto-Quipper-Mの一般化を紹介する。 この拡張はProto-Quipper-Kと呼ばれ、非常に一般的なダイナミックリフトを捉えることを目的としている。
  論文  参考訳（メタデータ） (2022-02-15T18:33:41Z)
• RNNs can generate bounded hierarchical languages with optimal memory [113.73133308478612]
  RNNは、自然言語構文の足場を反映した境界階層言語を効率的に生成できることを示す。 Dyck-($k$,$m$)は、よくネストされた括弧($k$型)と$m$バウンドされたネスト深さの言語である。 明示的な構成により,$O(m log k)$ hidden units の RNN がメモリの指数的削減に十分であることを示す。
  論文  参考訳（メタデータ） (2020-10-15T04:42:29Z)
• A tutorial introduction to quantum circuit programming in dependently typed Proto-Quipper [1.5274311118568713]
  本稿では,線形依存型を持つ実験量子回路言語Proto-Quipper-Dを提案する。 本稿では,依存型が回路のプログラミングファミリを実現する方法と,依存型がガベージキュービットのタイプセーフ非計算の問題を解決する方法を示す。
  論文  参考訳（メタデータ） (2020-05-17T23:31:23Z)
• A Tale of a Probe and a Parser [74.14046092181947]
  言語のニューラルモデルにエンコードされている言語情報の計測は、NLPで人気が高まっている。 研究者は、他のモデルの出力から言語構造を抽出するために設計された教師付きモデル"プローブ"をトレーニングすることで、この企業にアプローチする。 そのようなプローブの1つは、構文情報が文脈化された単語表現でエンコードされる範囲を定量化するために設計された構造プローブである。
  論文  参考訳（メタデータ） (2020-05-04T16:57:31Z)
• Linear Dependent Type Theory for Quantum Programming Languages [1.7166794984161973]
  現代の量子プログラミング言語は、量子資源と古典的な制御を統合している。 それらは量子資源の非閉性を反映するために線形型付けされなければならない。 高水準および実用的な言語は、第一級市民として量子回路もサポートすべきである。
  論文  参考訳（メタデータ） (2020-04-28T13:11:06Z)

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

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。