論文の概要: Reasoning about concurrent loops and recursion with rely-guarantee rules
- arxiv url: http://arxiv.org/abs/2512.06242v1
- Date: Sat, 06 Dec 2025 01:57:42 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-12-09 22:03:54.256475
- Title: Reasoning about concurrent loops and recursion with rely-guarantee rules
- Title(参考訳): rely-guaranteeルールによる並列ループと再帰の推論
- Authors: Ian J. Hayes, Larissa A. Meinicke, Cliff B. Jones,
- Abstract要約: 本稿では,プログラムとループの推論のための汎用的,機械的検証,洗練について述べる。
我々は,並列スレッドからの干渉の推論を容易にする格子保証手法を利用する。
- 参考スコア(独自算出の注目度): 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: The objective of this paper is to present general, mechanically verified, refinement rules for reasoning about recursive programs and while loops in the context of concurrency. Unlike many approaches to concurrency, we do not assume that expression evaluation is atomic. We make use of the rely-guarantee approach to concurrency that facilitates reasoning about interference from concurrent threads in a compositional manner. Recursive programs can be defined as fixed points over a lattice of commands and hence we develop laws for reasoning about fixed points. Loops can be defined in terms of fixed points and hence the laws for recursion can be applied to develop laws for loops.
- Abstract(参考訳): 本研究の目的は,並列処理における再帰的プログラムの推論とループの並列化に関する一般的な,機械的検証,洗練されたルールを提案することである。
並行性に対する多くのアプローチとは異なり、式評価がアトミックであると仮定しない。
我々は、並列スレッドからの干渉をコンポジション的に推論しやすくする、並行処理に対する依存性保証アプローチを活用している。
再帰的プログラムは、コマンド格子上の固定点として定義することができ、したがって、固定点についての推論の法則を開発する。
ループは固定点の観点から定義することができ、したがって再帰の法則をループの法則の開発に適用することができる。
関連論文リスト
- To CoT or To Loop? A Formal Comparison Between Chain-of-Thought and Looped Transformers [32.84174396586435]
CoT(Chain-of-Thought)とLooped Transformerは、推論タスクのパフォーマンスを実証的に改善することが示されている。
それぞれの強みと限界を形式的に分析する。
論文 参考訳(メタデータ) (2025-05-25T17:49:37Z) - The nature of loops in programming [37.48416208168878]
プログラムのセマンティクスと検証では、ループに関する推論は2つの異なる数学的引数を生成する必要があるため複雑である。
単一かつ単純な定義が可能で、この分割を取り除くことができる。
ループが正しいことを証明するには、不変量と不変量を考案する必要はない。
関係を識別するのに十分であり、部分的正当性と終了の両方をもたらす。
論文 参考訳(メタデータ) (2025-04-10T20:58:55Z) - Invariant Relations: A Bridge from Programs to Equations [1.3342735568824553]
任意のレベルにネストしたループを持つプログラムを含む,C型プログラムの関数を導出する手法を提案する。
ループの意味を捉えるために、不変関係の概念を用いる。
論文 参考訳(メタデータ) (2023-10-07T04:11:23Z) - Consistent circuits for indefinite causal order [0.0]
論理的に一貫性があるが、循環因果構造を特徴とする多くの量子過程が提案されている。
ここでは,エキゾチックな因果構造を持つプロセスを構築する方法を提案する。
因果不等式に反するプロセスを含む、エキゾチックなプロセスの標準的な例が、このような方法で生成可能なプロセスのクラスであることを示す。
論文 参考訳(メタデータ) (2022-06-20T23:15:52Z) - Discovering Non-monotonic Autoregressive Orderings with Variational
Inference [67.27561153666211]
我々は、訓練データから高品質な生成順序を純粋に検出する、教師なし並列化可能な学習装置を開発した。
エンコーダを非因果的注意を持つトランスフォーマーとして実装し、1つのフォワードパスで置換を出力する。
言語モデリングタスクにおける経験的結果から,我々の手法は文脈認識であり,一定の順序と競合する,あるいはより優れた順序を見つけることができる。
論文 参考訳(メタデータ) (2021-10-27T16:08:09Z) - Discovering Useful Compact Sets of Sequential Rules in a Long Sequence [57.684967309375274]
COSSUは、小さな、意味のある一連の規則をマイニングするアルゴリズムである。
COSSUは、長いシーケンスから、関連するクローズド・シーケンシャル・ルールの集合を検索できることを示す。
論文 参考訳(メタデータ) (2021-09-15T18:25:18Z) - Context-aware and Scale-insensitive Temporal Repetition Counting [60.40438811580856]
時間的反復カウントは、与えられた反復行動のサイクル数を推定することを目的としている。
既存のディープラーニング手法は、実生活における複雑な反復行動に対して無効である固定された時間スケールで繰り返し動作が実行されると仮定する。
本稿では,未知かつ多様なサイクル長による繰り返しカウントの課題に対処するための文脈認識・スケール非感性フレームワークを提案する。
論文 参考訳(メタデータ) (2020-05-18T05:49:48Z) - Pseudo-Convolutional Policy Gradient for Sequence-to-Sequence
Lip-Reading [96.48553941812366]
唇読解は唇運動系列から音声内容を推測することを目的としている。
seq2seqモデルの伝統的な学習プロセスには2つの問題がある。
本稿では,これら2つの問題に対処するために,PCPGに基づく新しい手法を提案する。
論文 参考訳(メタデータ) (2020-03-09T09:12:26Z) - Consistency of a Recurrent Language Model With Respect to Incomplete
Decoding [67.54760086239514]
逐次言語モデルから無限長のシーケンスを受信する問題について検討する。
不整合に対処する2つの対策として、トップkと核サンプリングの一貫性のある変種と、自己終端の繰り返し言語モデルを提案する。
論文 参考訳(メタデータ) (2020-02-06T19:56:15Z) - Retrograde Program Analysis: A Practical Tutorial [51.56484100374058]
このチュートリアルは、定義を集中したガイドへのより長い説明を凝縮している。
目的は、短い証明、具体的な不変性、ドロップインコードとプロパティテストである。
論文 参考訳(メタデータ) (2010-06-13T13:32:37Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。