論文の概要: Encoding call-by-push-value in the pi-calculus

• arxiv url: http://arxiv.org/abs/2506.10584v1
• Date: Thu, 12 Jun 2025 11:21:36 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-06-13 15:37:22.700312
• Title: Encoding call-by-push-value in the pi-calculus
• Title（参考訳）: pi-calculus におけるcall-by-push-value の符号化
• Authors: Benjamin Bennetzen, Nikolaj Rossander Kristensen, Peter Buus Steffensen,
• Abstract要約: 我々は,push-value-calculus (CBPV) の pi-i-calculus における Levys コール・バイ・プッシュ・バリュー・カルカス(CBPV) の符号化を定義し,符号化が健全かつ完全であることを証明した。 我々は、音性、完全性、および全ての必要な補題の非公式な(手で)証明を提示する。 本稿では,p-i-calculus における CBPV のエンコーディング,非同期なpolyadic pi-calculus および局所的なpi-calculus を含む。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: In this report we define an encoding of Levys call-by-push-value lambda-calculus (CBPV) in the pi-calculus, and prove that our encoding is both sound and complete. We present informal (by-hand) proofs of soundness, completeness, and all required lemmas. The encoding is specialized to the internal pi-calculus (pi-i-calculus) to circumvent certain challenges associated with using de Bruijn index in a formalization, and it also helps with bisimulation as early-, late- and open-bisimulation coincide in this setting, furthermore bisimulation is a congruence. Additionally, we argue that our encoding also satisfies the five criteria for good encodings proposed by Gorla, as well as show similarities between Milners and our encoding. This paper includes encodings from CBPV in the pi-i-calculus, asynchronous polyadic pi-calculus and the local pi-calculus. We begin a formalization of the proof in Coq for the soundness and completeness of the encoding in the pi-i-calculus. Not all lemmas used in the formalization are themselves formally proven. However, we argue that the non-proven lemmas are reasonable, as they are proven by hand, or amount to Coq formalities that are straightforward given informal arguments.
• Abstract（参考訳）: 本稿では, push-value lambda-calculus (CBPV) の pi-calculus における符号化を定義し, 符号化が健全かつ完全であることを証明した。 我々は、音性、完全性、および全ての必要な補題の非公式な(手で)証明を提示する。 符号化は内部のpi-calculus(pi-i-calculus)に特化され、形式化におけるde Bruijn指数の使用に伴うある種の問題を回避する。 さらに、我々のエンコーディングは、Gorlaが提案した良いエンコーディングの5つの基準を満たすとともに、ミルナーズとエンコーディングの類似性も示している。 本稿では,p-i-calculus における CBPV のエンコーディング,非同期なpolyadic pi-calculus および局所的なpi-calculus を含む。 我々は、pi-i-計算における符号化の健全性と完全性に対するCoqの証明の形式化を開始する。 形式化で使われるすべての補題が公式に証明されているわけではない。 しかし、証明されていない補題は手動で証明されるため理にかなったものであるか、非公式な議論が与えられた場合の直接的なCoq形式に等しいかのどちらかである。

関連論文リスト

• Encodings of Observable Subalgebras [0.0]
  システムの可観測物のサブセットのみを保持するエンコーディングについて検討する。 我々の研究は全 CAR 代数の符号化にも当てはまるが、偶数パリティセクターの符号化にも当てはまる。
  論文  参考訳（メタデータ） (2025-02-27T23:32:31Z)
• Linear-time Minimum Bayes Risk Decoding with Reference Aggregation [52.1701152610258]
  最小ベイズリスク(MBR、Minimum Bayes Risk)は、機械翻訳の品質向上を図ったテキスト生成技術である。 これは2次複雑性を持つ実用計量のペアワイズ計算を必要とする。 本稿では,集約された参照表現に対して計算したスコアを用いて,ペアワイズメトリックスコアを近似する。
  論文  参考訳（メタデータ） (2024-02-06T18:59:30Z)
• Context Perception Parallel Decoder for Scene Text Recognition [52.620841341333524]
  シーンテキスト認識手法は高い精度と高速な推論速度を達成するのに苦労している。 本稿では、STRにおけるARデコーディングの実証的研究を行い、ARデコーダが言語文脈をモデル化するだけでなく、視覚的文脈知覚のガイダンスも提供することを明らかにする。 我々は一連のCPPDモデルを構築し、提案したモジュールを既存のSTRデコーダにプラグインする。英語と中国語のベンチマーク実験により、CPPDモデルはARベースモデルよりも約8倍高速に動作し、高い競争精度を達成できることを示した。
  論文  参考訳（メタデータ） (2023-07-23T09:04:13Z)
• Single-shot decoding of good quantum LDPC codes [38.12919328528587]
  量子タナー符号が逆雑音の単ショット量子誤り補正(QEC)を促進することを証明した。 本稿では,複数ラウンドのQECにおける誤りを抑えるために,並列復号アルゴリズムを各ラウンドで一定時間実行するのに十分であることを示す。
  論文  参考訳（メタデータ） (2023-06-21T18:00:01Z)
• GRACE: Discriminator-Guided Chain-of-Thought Reasoning [75.35436025709049]
  本稿では, 正しい推論手順を導出するために, GRACE (CorrectnEss Discriminator) を用いたチェーン・オブ・シークレット・リAsoningを提案する。 GRACEは、正しいステップと間違ったステップに対して対照的な損失で訓練された判別器を採用しており、復号時に次のステップ候補を採点するために使用される。
  論文  参考訳（メタデータ） (2023-05-24T09:16:51Z)
• Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs [5.045988012508899]
  オートフォーマル化(Autoformalization)は、自然言語で書かれた証明を、対話的定理証明を通じてコンピュータで検証可能な形式表現に変換することによって、この問題に対処しようとする。 本稿では, 基本数学的証明を, Coq の対話的定理証明器の言語における等価な形式化に変換する, ユニバーサルトランスフォーマーアーキテクチャに基づく意味解析手法を提案する。
  論文  参考訳（メタデータ） (2023-01-05T17:56:00Z)
• Entanglement-Assisted Quantum Error-Correcting Codes over Local Frobenius Rings [10.533569558002796]
  有限可換局所フロベニウス環$mathcalR$上の古典的加法符号から絡み合い支援量子誤り訂正符号(EAQECCs)を構築するためのフレームワークを提供する。 また、付加的なコードに余分な座標を加えることで、構成結果のEAQECCのパラメータを決定する上で、ある程度の柔軟性が得られます。
  論文  参考訳（メタデータ） (2022-02-01T06:58:56Z)
• Neural Proof Nets [0.8379286663107844]
  本稿では,Sinkhorn ネットワークをベースとした証明ネットのニューラルバリアントを提案する。 AEThelでは,テキスト文の正しい書き起こしを線形ラムダ計算の証明や用語として70%の精度で行うことができる。
  論文  参考訳（メタデータ） (2020-09-26T22:48:47Z)
• PBS-Calculus: A Graphical Language for Coherent Control of Quantum Computations [77.34726150561087]
  本稿では,量子演算のコヒーレント制御を含む量子計算を表現・推論するためにPBS計算を導入する。 我々はこの言語に方程式理論を加え、それが健全で完備であることが証明された。 我々は、制御された置換の実装やループのアンロールのようなアプリケーションを考える。
  論文  参考訳（メタデータ） (2020-02-21T16:15:58Z)
• Single-Shot Decoding of Linear Rate LDPC Quantum Codes with High Performance [5.33024001730262]
  我々は、線形符号化率、スケーリング距離、効率的な復号方式を用いて、低密度パリティチェック(LDPC)量子コード群を構築し、解析する。 コードファミリーは、Guth と Lubotzky が最初に示唆したように、閉じた4次元の双曲型のテッセルレーションに基づいている。
  論文  参考訳（メタデータ） (2020-01-10T17:21:27Z)

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

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