Anti-unification of Unordered Goals

TL;DR

This paper investigates the problem of anti-unification of unordered goals in logic programming, focusing on the complexity of finding largest or most specific generalizations, and providing polynomial-time algorithms under certain conditions.

Contribution

It defines two generalization relations for unordered goals, characterizes most specific generalizations, and analyzes the computational complexity of these problems.

Findings

Most specific generalizations can be computed in polynomial time.

Minimizing the number of variables makes the problem NP-hard.

Largest common generalizations with injective variable renamings are computable in polynomial time.

Abstract

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.