Nominal anti-unification with atom-variables
File(s)LIPIcs-FSCD-2022-7.pdf (903.19 KB)
Published version
Author(s)
Schmidt-Schauß, Manfred
Nantes Sobrinho, Daniele
Type
Conference Paper
Abstract
Anti-unification is the task of generalizing a set of expressions in the most specific way. It was extended to the nominal framework by Baumgarter, Kutsia, Levy and Villaret, who defined an algorithm solving the nominal anti-unification problem, which runs in polynomial time. Unfortunately, when an infinite set of atoms are allowed in generalizations, a minimal complete set of solutions in nominal anti-unification does not exist, in general. In this paper, we present a more general approach to nominal anti-unification that uses atom-variables instead of explicit atoms, and two variants of freshness constraints: NL_A-constraints (with atom-variables), and Eqr-constraints based on Equivalence relations on atom-variables. The idea of atom-variables is that different atom-variables may be instantiated with identical or different atoms. Albeit simple, this freedom in the formulation increases its application potential: we provide an algorithm that is finitary for the NL_A-freshness constraints, and for Eqr-freshness constraints it computes a unique least general generalization. There is a price to pay in the general case: checking freshness constraints and other related logical questions will require exponential time. The setting of Baumgartner et al. is improved by the atom-only case, which runs in polynomial time and computes a unique least general generalization.
Date Issued
2022-06-28
Date Acceptance
2022-04-16
Citation
LIPIcs : Leibniz International Proceedings in Informatics, 2022, 228, pp.7:1-7:22
ISSN
1868-8969
Publisher
Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
Start Page
7:1
End Page
7:22
Journal / Book Title
LIPIcs : Leibniz International Proceedings in Informatics
Volume
228
Copyright Statement
© Manfred Schmidt-Schaußand Daniele Nantes-Sobrinho;
licensed under Creative Commons License CC-BY 4.0 (https://creativecommons.org/licenses/by/4.0/)
licensed under Creative Commons License CC-BY 4.0 (https://creativecommons.org/licenses/by/4.0/)
License URL
Source
Formal Structures for Computation and Deduction
Publication Status
Published
Start Date
2022-06-02
Finish Date
2022-08-05
Coverage Spatial
Haifa, Israel