Equational Anti-Unification over Absorption Theories

• URL: http://arxiv.org/abs/2310.11136v1
• Date: Tue, 17 Oct 2023 10:38:06 GMT
• Title: Equational Anti-Unification over Absorption Theories
• Authors: Mauricio Ayala-Rincon, David M. Cerna, Andres Felipe Gonzalez Barragan, and Temur Kutsia
• Abstract summary: Anti-unification techniques have found uses within clone detection and automatic program repair methods. 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.
• Score: 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.

Related papers

• Automatic verification of Finite Variant Property beyond convergent equational theories [5.9972628641893015]
  Most automated verifiers for security protocols focus on equational theories that satisfy the Finite Variant Property (FVP) We propose a novel semi-decision procedure for proving FVP, without the need for a specific representation, and for a class of theories that goes beyond the ones expressed by an E-convergent rewrite system.
  arXiv  Detail & Related papers  (2024-10-20T05:11:30Z)
• Bregman-divergence-based Arimoto-Blahut algorithm [53.64687146666141]
  We generalize the Arimoto-Blahut algorithm to a general function defined over Bregman-divergence system. We propose a convex-optimization-free algorithm that can be applied to classical and quantum rate-distortion theory.
  arXiv  Detail & Related papers  (2024-08-10T06:16:24Z)
• Algebraic anti-unification [0.0]
  Abstraction is key to human and artificial intelligence as it allows one to see common structure in otherwise distinct objects or situations. Anti-unification (or generalization) is textitthe part of theoretical computer science and AI studying abstraction.
  arXiv  Detail & Related papers  (2024-07-22T09:49:46Z)
• Bisimulation Learning [55.859538562698496]
  We compute finite bisimulations of state transition systems with large, possibly infinite state space. Our technique yields faster verification results than alternative state-of-the-art tools in practice.
  arXiv  Detail & Related papers  (2024-05-24T17:11:27Z)
• Non-asymptotic convergence bounds for Sinkhorn iterates and their gradients: a coupling approach [10.568851068989972]
  We focus on a relaxation of the original OT problem, the entropic OT problem, which allows to implement efficient and practical algorithmic solutions. This formulation, also known as the Schr"odinger Bridge problem, notably connects with Optimal Control (SOC) and can be solved with the popular Sinkhorn algorithm.
  arXiv  Detail & Related papers  (2023-04-13T13:58:25Z)
• Infeasible Deterministic, Stochastic, and Variance-Reduction Algorithms for Optimization under Orthogonality Constraints [9.301728976515255]
  This article provides new practical and theoretical developments for the landing algorithm. First, the method is extended to the Stiefel manifold. We also consider variance reduction algorithms when the cost function is an average of many functions.
  arXiv  Detail & Related papers  (2023-03-29T07:36:54Z)
• Differentially-Private Hierarchical Clustering with Provable Approximation Guarantees [79.59010418610625]
  We study differentially private approximation algorithms for hierarchical clustering. We show strong lower bounds for the problem: that any $epsilon$-DP algorithm must exhibit $O(|V|2/ epsilon)$-additive error for an input dataset. We propose a private $1+o(1)$ approximation algorithm which also recovers the blocks exactly.
  arXiv  Detail & Related papers  (2023-01-31T19:14:30Z)
• The Dynamics of Riemannian Robbins-Monro Algorithms [101.29301565229265]
  We propose a family of Riemannian algorithms generalizing and extending the seminal approximation framework of Robbins and Monro. Compared to their Euclidean counterparts, Riemannian algorithms are much less understood due to lack of a global linear structure on the manifold. We provide a general template of almost sure convergence results that mirrors and extends the existing theory for Euclidean Robbins-Monro schemes.
  arXiv  Detail & Related papers  (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]
  Filtering equations play a central role in many real-life applications, including numerical weather prediction, finance and engineering. One of the classical approaches to approximate the solution of the filtering equations is to use a PDE inspired method, called the splitting-up method. We combine this method with a neural network representation to produce an approximation of the unnormalised conditional distribution of the signal process.
  arXiv  Detail & Related papers  (2022-01-10T11:01:36Z)
• Lifting the Convex Conjugate in Lagrangian Relaxations: A Tractable Approach for Continuous Markov Random Fields [53.31927549039624]
  We show that a piecewise discretization preserves better contrast from existing discretization problems. We apply this theory to the problem of matching two images.
  arXiv  Detail & Related papers  (2021-07-13T12:31:06Z)
• Dynamic programming by polymorphic semiring algebraic shortcut fusion [1.9405875431318445]
  Dynamic programming (DP) is an algorithmic design paradigm for the efficient, exact solution of intractable, problems. This paper presents a rigorous algebraic formalism for systematically deriving DP algorithms, based on semiring.
  arXiv  Detail & Related papers  (2021-07-05T00:51:02Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.