Equational Anti-Unification over Absorption Theories
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2023
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866912440488296448 |
|---|---|
| author | Ayala-Rincon, Mauricio Cerna, David M. Barragan, Andres Felipe Gonzalez Kutsia, Temur |
| author_facet | Ayala-Rincon, Mauricio Cerna, David M. Barragan, Andres Felipe Gonzalez Kutsia, Temur |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2310_11136 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Equational Anti-Unification over Absorption Theories Ayala-Rincon, Mauricio Cerna, David M. Barragan, Andres Felipe Gonzalez Kutsia, Temur Logic in Computer Science Software Engineering 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. |
| title | Equational Anti-Unification over Absorption Theories |
| topic | Logic in Computer Science Software Engineering |
| url | https://arxiv.org/abs/2310.11136 |