論文の概要: Equational Anti-Unification over Absorption Theories
- arxiv url: http://arxiv.org/abs/2310.11136v1
- Date: Tue, 17 Oct 2023 10:38:06 GMT
- ステータス: 処理完了
- システム内更新日: 2023-10-21 15:00:06.769569
- Title: Equational Anti-Unification over Absorption Theories
- Title（参考訳）: 吸収理論に対する等角的反統一
- Authors: Mauricio Ayala-Rincon, David M. Cerna, Andres Felipe Gonzalez
Barragan, and Temur Kutsia
- Abstract要約: 抗統一技術は、クローン検出と自動プログラム修復法で使用されている。
本稿では、反統一変調純吸収理論、すなわち、いくつかの作用素は公理 $f(x,varepsilon_f) approx f(varepsilon_f,x) approx varepsilon_f$ を満たす特別な定数と関連している。
我々はこのような理論に対する健全で完全なルールベースのアルゴリズムを提供し、さらに、反統一モジュロ吸収は無限であることを示す。
- 参考スコア（独自算出の注目度）: 1.124958340749622
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Interest in anti-unification, the dual problem of unification, is on the rise
due to applications within the field of software analysis and related areas.
For example, anti-unification-based techniques have found uses within clone
detection and automatic program repair methods. While syntactic forms of
anti-unification are enough for many applications, some aspects of software
analysis methods are more appropriately modeled by reasoning modulo an
equational theory. Thus, extending existing anti-unification methods to deal
with important equational theories is the natural step forward. This paper
considers anti-unification modulo pure absorption theories, i.e., some
operators are associated with a special constant satisfying the axiom
$f(x,\varepsilon_f) \approx f(\varepsilon_f,x) \approx \varepsilon_f$. We
provide a sound and complete rule-based algorithm for such theories.
Furthermore, we show that anti-unification modulo absorption is infinitary.
Despite this, our algorithm terminates and produces a finitary algorithmic
representation of the minimal complete set of solutions. We also show that the
linear variant is finitary.
- Abstract（参考訳）: 統合の二重問題であるアンチ・ユニフィケーションへの関心は、ソフトウェア分析や関連する分野の応用によって高まっている。
例えば、アンチユニフィケーションベースの技術はクローン検出と自動プログラム修復法で使用されている。
反統一の構文形式は多くの応用に十分であるが、ソフトウェア分析手法のいくつかの側面は方程式理論を推論することでより適切にモデル化されている。
したがって、重要な方程式理論を扱うために既存の反統一法を拡張することは自然な一歩である。
本稿では、反統一モジュロ純粋吸収理論、すなわち、いくつかの作用素は公理 $f(x,\varepsilon_f) \approx f(\varepsilon_f,x) \approx \varepsilon_f$ を満たす特別な定数と関連している。
このような理論に対する健全で完全なルールベースのアルゴリズムを提供する。
さらに, 抗統一モジュロ吸収は無限であることを示す。
それにもかかわらず、我々のアルゴリズムは最小の解集合の有限アルゴリズム表現を終了し、生成する。
また、線形変種は有限であることを示す。
関連論文リスト
- Automatic verification of Finite Variant Property beyond convergent equational theories [5.9972628641893015]
セキュリティプロトコルのほとんどの自動検証は、有限変数性(FVP)を満たす方程式理論に焦点を当てている。
本稿では,FVPの特定表現を必要とせずにFVPを証明し,E-convergentリライトシステムによって表現される理論を超越した理論のクラスについて,新たな半決定手順を提案する。
論文 参考訳（メタデータ） (2024-10-20T05:11:30Z) - Bregman-divergence-based Arimoto-Blahut algorithm [53.64687146666141]
本稿では,Arimoto-BlahutアルゴリズムをBregman-Diversergenceシステム上で定義された一般関数に一般化する。
本稿では,古典的および量子速度歪み理論に適用可能な凸最適化自由アルゴリズムを提案する。
論文 参考訳（メタデータ） (2024-08-10T06:16:24Z) - Algebraic anti-unification [0.0]
抽象は人間や人工知能にとって鍵であり、他の異なる物体や状況で共通の構造を見ることができる。
アンチ・ユニフィケーション(英: anti-unification、あるいは generalization)は、理論計算機科学とAIによる抽象研究のテキストである。
論文 参考訳（メタデータ） (2024-07-22T09:49:46Z) - Bisimulation Learning [55.859538562698496]
我々は、大きな、潜在的に無限の状態空間を持つ状態遷移系の有限バイシミュレートを計算する。
提案手法は,実際に行われている他の最先端ツールよりも高速な検証結果が得られる。
論文 参考訳（メタデータ） (2024-05-24T17:11:27Z) - Non-asymptotic convergence bounds for Sinkhorn iterates and their
gradients: a coupling approach [10.568851068989972]
本稿では,アルゴリズムの効率的な解法を実現するために,元のOT問題であるエントロピックOT問題の緩和に焦点をあてる。
この定式化はSchr"odinger Bridge問題としても知られ、特に最適制御(SOC)と結びつき、人気のあるシンクホーンアルゴリズムで解くことができる。
論文 参考訳（メタデータ） (2023-04-13T13:58:25Z) - Infeasible Deterministic, Stochastic, and Variance-Reduction Algorithms for Optimization under Orthogonality Constraints [9.301728976515255]
本稿では,着陸アルゴリズムの実用化と理論的展開について述べる。
まず、この方法はスティーフェル多様体に拡張される。
また、コスト関数が多くの関数の平均である場合の分散還元アルゴリズムについても検討する。
論文 参考訳（メタデータ） (2023-03-29T07:36:54Z) - Differentially-Private Hierarchical Clustering with Provable
Approximation Guarantees [79.59010418610625]
階層クラスタリングのための微分プライベート近似アルゴリズムについて検討する。
例えば、$epsilon$-DPアルゴリズムは入力データセットに対して$O(|V|2/epsilon)$-additiveエラーを示さなければならない。
本稿では,ブロックを正確に復元する1+o(1)$近似アルゴリズムを提案する。
論文 参考訳（メタデータ） (2023-01-31T19:14:30Z) - The Dynamics of Riemannian Robbins-Monro Algorithms [101.29301565229265]
本稿では,Robins と Monro のセミナル近似フレームワークを一般化し拡張するリーマンアルゴリズムの族を提案する。
ユークリッドのそれと比較すると、リーマンのアルゴリズムは多様体上の大域線型構造が欠如しているため、はるかに理解されていない。
ユークリッド・ロビンス=モンロスキームの既存の理論を反映し拡張するほぼ確実な収束結果の一般的なテンプレートを提供する。
論文 参考訳（メタデータ） (2022-06-14T12:30:11Z) - An application of the splitting-up method for the computation of a
neural network representation for the solution for the filtering equations [68.8204255655161]
フィルタ方程式は、数値天気予報、金融、工学など、多くの現実の応用において中心的な役割を果たす。
フィルタリング方程式の解を近似する古典的なアプローチの1つは、分割法と呼ばれるPDEにインスパイアされた方法を使うことである。
我々はこの手法をニューラルネットワーク表現と組み合わせて、信号プロセスの非正規化条件分布の近似を生成する。
論文 参考訳（メタデータ） (2022-01-10T11:01:36Z) - Lifting the Convex Conjugate in Lagrangian Relaxations: A Tractable
Approach for Continuous Markov Random Fields [53.31927549039624]
断片的な離散化は既存の離散化問題と矛盾しないことを示す。
この理論を2つの画像のマッチング問題に適用する。
論文 参考訳（メタデータ） (2021-07-13T12:31:06Z) - Dynamic programming by polymorphic semiring algebraic shortcut fusion [1.9405875431318445]
動的プログラミング(動的プログラミング、英: Dynamic Programming、DP)は、難解問題の効率的かつ正確な解法のためのアルゴリズム設計パラダイムである。
本稿では,セミリングに基づくDPアルゴリズムを体系的に導出するための厳密な代数形式について述べる。
論文 参考訳（メタデータ） (2021-07-05T00:51:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。