Generalization Problems with Atom-Variables in Languages with Binders and Equational Theories
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866915173987516416 |
|---|---|
| author | Nantes-Sobrinho, Daniele Schmidt-Schauss, Manfred Baumgartner, Alexander Kutsia, Temur |
| author_facet | Nantes-Sobrinho, Daniele Schmidt-Schauss, Manfred Baumgartner, Alexander Kutsia, Temur |
| contents | Generalization problems in languages with binders involve computing the most common structure between expressions while respecting bound variable renaming and freshness constraints. These problems often lack a least general solution. However, leveraging nominal techniques, we previously demonstrated that a semantic approach with atom-variables enables the elimination of redundant solutions and allows for computing unique least general generalizations (LGGs). In this work, we extend this approach to handle associative (A), commutative (C), and associative-commutative (AC) equational theories. We present a sound and weak complete algorithm for solving equational generalization problems, which generates finite weak minimal complete sets of LGGs for each theory. A key challenge arises from solving equivariance problems while taking into account these equational theories, as identifying redundant generalizations requires recognizing when one expression (with binders) is a renaming of another while possibly considering permutations of sub-expressions. This unexpected interaction between renaming and equational reasoning made this particularly difficult, necessitating semantic tests within the equivariance algorithm. Given that these equational theories naturally induce exponentially large LGG sets due to subexpression permutations, future work could explore restricted theory fragments where the generalization problem remains unitary. In these fragments, LGGs can be computed efficiently in polynomial time, offering practical benefits for symbolic computation and automated reasoning tasks. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2502_19306 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Generalization Problems with Atom-Variables in Languages with Binders and Equational Theories Nantes-Sobrinho, Daniele Schmidt-Schauss, Manfred Baumgartner, Alexander Kutsia, Temur Logic in Computer Science Generalization problems in languages with binders involve computing the most common structure between expressions while respecting bound variable renaming and freshness constraints. These problems often lack a least general solution. However, leveraging nominal techniques, we previously demonstrated that a semantic approach with atom-variables enables the elimination of redundant solutions and allows for computing unique least general generalizations (LGGs). In this work, we extend this approach to handle associative (A), commutative (C), and associative-commutative (AC) equational theories. We present a sound and weak complete algorithm for solving equational generalization problems, which generates finite weak minimal complete sets of LGGs for each theory. A key challenge arises from solving equivariance problems while taking into account these equational theories, as identifying redundant generalizations requires recognizing when one expression (with binders) is a renaming of another while possibly considering permutations of sub-expressions. This unexpected interaction between renaming and equational reasoning made this particularly difficult, necessitating semantic tests within the equivariance algorithm. Given that these equational theories naturally induce exponentially large LGG sets due to subexpression permutations, future work could explore restricted theory fragments where the generalization problem remains unitary. In these fragments, LGGs can be computed efficiently in polynomial time, offering practical benefits for symbolic computation and automated reasoning tasks. |
| title | Generalization Problems with Atom-Variables in Languages with Binders and Equational Theories |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2502.19306 |