Anti-unification in logic programming refers to the process of capturing common syntactic structure among given goals, computing a single new goal that is more general called a generalization of the given goals. Finding an arbitrary common generalization for two goals is trivial, but looking for those common generalizations that are either as large as possible (called largest common generalizations) or as specific as possible (called most specific generalizations) is a non-trivial optimization problem, in particular when goals are considered to be \textit{unordered} sets of atoms. In this work we provide an in-depth study of the problem by defining two different generalization relations. We formulate a characterization of what constitutes a most specific generalization in both settings. While these generalizations can be computed in polynomial time, we show that when the number of variables in the generalization needs to be minimized, the problem becomes NP-hard. We subsequently revisit an abstraction of the largest common generalization when anti-unification is based on injective variable renamings, and prove that it can be computed in polynomially bounded time.
翻译:逻辑编程中的反统一是指在给定目标之间捕捉共同综合结构的过程,计算一个更普遍的新目标,称为对给定目标的概括化。为两个目标寻找任意的通用概括化是微不足道的,但寻找尽可能大(所谓的最大共同概括化)或尽可能具体(所谓的最具体的概括化)的通用概括化是一个非边际优化问题,特别是当目标被认为是 ktextit{unordered} 原子组时。在这项工作中,我们通过界定两种不同的概括化关系,对问题进行深入研究。我们对两种情况下最具体的概括化进行定性。虽然这些概括化可以在多元时间内计算,但我们表明,当一般化变数的数量需要最小化时,问题就会变得难以解决。当反对统一时,我们随后重新审视了以预言性变式重新命名为基础的最大共同概括化的抽象化,并证明它可以在多式约束的时间内进行计算。