Tags:anti-unification, generalisation, higher-order deduction and nominal algorithms
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 the type of the set of solutions in nominal anti-unification (with explicit atoms) is infinitary, since every solution set can be strictly refined. 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.