Anti-unification and Generalization: A Survey

1 Introduction

Anti-unification (AU), also known as generalization, is a fundamental operation used for inductive inference. It is abstractly defined as a process deriving from a set of symbolic expressions a new symbolic expression possessing certain commonalities shared between its members. It is the dual operation to unification, an operation at the foundation of modern automated reasoning and theorem proving [Baader and Snyder, 2001]. AU was introduced by Plotkin [1970] and Reynolds [1970] and may be illustrated as follows:

where f (a, g(g(c, a), h(a))) and f (a, g(c, h(a))) are two firstorder terms we want to anti-unify and f(a, g(X, h(a))) is the resulting generalization; mismatched sub-terms are replaced by variables. Note that f(a, g(X, h(a))) captures the common structure, and through substitution, either input term is derivable. Additionally, f(a, g(X, h(a))) is commonly referred to as the least general generalization as there does not exist a more specific term capturing all common structure. The term f(a, X) is more general; partly covers common structure.

∗Contact Author

Early inductive logic programming (ILP) [Cropper et al., 2022] approaches exploited the relationship between generalizations to learn logic programs [Muggleton, 1995]. Modern ILP approaches, such as Popper [Cropper and Morel, 2021], use this mechanism to simplify the search iteratively. The programming by example (pbe) [Gulwani, 2016] paradigm integrates syntactic anti-unification methods to find the least general programs satisfying the input examples. Recent work concerning library learning and compression [Cao et al., 2023] exploits equational anti-unification to find suitable programs efficiently and outperforms Dreamcoder [Ellis et al., 2021], the previous state of the art approach.

Applications outside the area of inductive synthesis typically exploit the following observation: "Syntactic similarity often implies semantic similarity". A notable example is automatic parallel recursion scheme detection [Barwell et al., 2018] where templates are developed, with the help of AU, allowing the replacement of non-parallelizable recursion by parallelized higher-order functions. Other uses are learning program repairs from repositories [de Sousa et al., 2021], preventing misconfigurations [Mehta et al., 2020], and detecting software clones [Vanhoof and Yernaux, 2019].

There is growing interest in anti-unification, yet much of the existing work is motivated by specific applications. The lack of a systematic investigation has led to, on occasion, reinvention of methods and algorithms. Illustratively, the authors of Babble [Cao et al., 2023] developed an E-graph anti-unification algorithm motivated solely by the seminal work of Plotkin [1970]. Due to the fragmentary nature of the anti-unification literature, the authors missed relevant work on equational [Burghardt, 2005] and term-graph antiunification [Baumgartner et al., 2018] among others. The discovery of these earlier papers could have probably sped up, improved, and/or simplified their investigation.

Unlike its dual unification, there are no comprehensive surveys, and little emphasis is put on developing a strong theoretical foundation. Instead, practically oriented topics dominate current research on anti-unification. This situation is unsurprising as generalization, in one form or another, is an essential ingredient within many applications: reasoning, learning, information extraction, knowledge representation, data compression, software development, and analysis, in addition to those already mentioned.

New applications pose new challenges. Some require studying generalization problems in a completely new theory, while others may be addressed adequately by improving existing algorithms. Classifying, analyzing, and surveying the known methods and their applications is of fundamental importance to shape the field and help researchers to navigate the current fragmented state-of-the-art on generalization.

In this survey, we provide (i) a general framework for the generalization problem, (ii) an overview of existing theoretical results, (iii) an overview of existing application domains, and (iv) an overview of some future directions of research.

2 Generalization Problems: an Abstract View

The definitions below are parameterized by a set of syntactic objects O, typically consisting of expressions (e.g., terms, formulas, . . . ) in some formal language. Additionally, we consider a class of mappings M from O to O. We say that µ(O) is an instance of the object O with respect to µ ∈ M. In most cases, variable substitutions are instances of such mappings. We call elements of M generalization mappings.

Our definition of the generalization problem requires two relations: The base relation defining what it means for an object to be a generalization of another, and the preference relation, defining a notion of rank between generalizations. These relations are defined abstractly, with minimal requirements. We provide the concrete instances of the base and preference relations and generalization mappings for each concrete generalization problem. One ought to consider the base relation as describing what we mean when we say an object is a generalization of another and the preference relation as describing the quality of generalizations with respect to one another. The mappings can be thought of as describing what the generalization of the objects means over the given base relation.

Definition 1. A base relation B is a binary reflexive relation on O. An object G ∈ O is a generalization of the object O ∈ O with respect to B and a class of mappings M (briefly, BMgeneralization) if B(µ(G), O) holds for some mapping µ ∈ M. A preference relation P is a binary reflexive, transitive relation (i.e., a preorder) on O. We write P(O1, O2) to indicate that the object O1 is preferred over the object O2. It induces an equivalence relation ≡P: O1 ≡P O2 iff P(O1,O2) and P(O2, O1).

We are interested in preference relations that relate to generalizations in the following way:

Definition 2 (Consistency). Let B and P be, respectively, base and preference relations defined on a set of objects O and M be a class of generalization mappings over O. We say that B and P are consistent on O with respect to M or, shortly, M-consistent, if the following holds: If G1 is a BM-generalization of O and P(G1, G2) holds for some G2, then G2 is also a BM-generalization of O. In other words, if B(µ1(G1),O) for some µ1 ∈ M and P(G1, G2), then there should exist µ2 ∈ M such that B(µ2(G2), O).

Consistency is an important property since it relates otherwise unrelated base and preference relations in the context of generalizations. The intuition being that, for M-consistent B and P, G1 is "better" than G2 as a (BM, P)-generalization of O because it provides more information: not only G1 is a generalization of O, but also any object G2 that is "dominated" by G1 in the preference relation. From now on, we assume that our base and preference relations are consistent with respect to the considered set of generalization mappings.

We focus on characterizing common BM-generalizations between multiple objects, selecting among them the "best" ones with respect to the preference relation P.

Definition 3 (Most preferred common generalizations). An object G is called a most P-preferred common BMgeneralization of objects O1, . . . , On, n ≥ 2 if

• G is a BM-generalization of each Oi, and
• for any G′ that is also a BM-generalization of each Oi, if P(G′ , G), then G′ ≡P G (i.e., if G′ is P-preferred over G, then they are P-equivalent).

For O, B, M, and P, the (BM, P)-generalization problem over O is specified as follows:

Given: Objects O1, . . . ,On ∈ O, n ≥ 2.

Find: An object G ∈ O that is a most P-preferred common BM-generalization of O1, . . . , On.

This problem may have zero, one, or more solutions. There can be two reasons why it has zero solutions: either the objects O1, . . . , On have no common BM-generalization at all (i.e, O1, . . . ,On are not generalizable, for an example see [Pfenning, 1991]), or they are generalizable but have no most P-preferred common BM-generalization.

To characterize "informative" sets of possible solutions, we introduce two notions: P-complete and P-minimal complete sets of common BM-generalizations of multiple objects:

Definition 4. A set of objects G is called a P-complete set of common BM-generalizations of the given objects O1, . . . , On, n ≥ 2, if the following properties are satisfied:

• Soundness: every G ∈ G is a common BM-generalization of O1, . . . , On, and
• Completeness: for each common BM-generalization G′ of O1, . . . , On there exists G ∈ G such that P(G, G′ ).

The set G is called P-minimal complete set of common BM-generalizations of O1, . . . ,On and is denoted by mcsgBM,P(O1, . . . ,On) if, in addition, the following holds:

• Minimality: no distinct elements of G are P-comparable: if G1, G2 ∈ G and P(G1, G2), then G1 = G2.

Note that the minimality property guarantees that if G ∈ mcsgBM,P(O1, . . . , On), then no G′ , differing from G, in the ≡P-equivalence class of G belongs to this set.

In the notation, we may skip BM, P, or both from mcsgBM,P when it is clear from the context.

Definition 5 (Generalization type). We say that the type of the (BM, P)-generalization problem between the generalizable objects O1, . . . , On ∈ O is

• unitary (1): mcsgBM,P(O1, . . . ,On) is a singleton,
• finitary (ω): mcsgBM,P(O1, . . . ,On) is finite and contains at least two elements,
• infinitary (∞): mcsgBM,P(O1, . . . ,On) is infinite,
• nullary (0): mcsgBM,P(O1, . . . , On) does not exist (i.e., minimality and completeness contradict each other).

The type of (BM, P)-generalization over O is

• unitary (1): each (BM,P)-generalization problem between generalizable objects from O is unitary,
• finitary (ω): each (BM,P)-generalization problem between generalizable objects from O is unitary or finitary, and there exists a finitary problem,
• infinitary (∞): each (BM,P)-generalization problem between generalizable objects from O is unitary, finitary, or infinitary, and there exists an infinitary problem,
• nullary (0): there exists a nullary (BM,P)-generalization problem between generalizable objects from O.

The basic questions to be answered in this context are,

• Generalization type: What is the (BM,P)-generalization type over O?
• Generalization algorithm/procedure: How to compute (or enumerate) a complete set of generalizations (preferably, mcsgBM,P) for objects fromO.

If the given objects O1, . . . ,On (resp. the desired object G) are restricted to belong to a subset S ⊆ O, then we talk about an S-fragment (resp. S-variant) of the generalization problem. It also makes sense to consider an S1-variant of an S2-fragment of the problem, where S1 and S2 are not necessarily the same.

When O is a set of terms, the linear variant is often considered: the generalization terms do not contain multiple occurrences of the same variable.

The following sections show how some known generalization problems fit into this schema. For simplicity, when it does not affect generality, we consider generalization problems with only two given objects. Also, we skip the word "common" when discussing common generalizations.

Due to space constraints, we do not discuss anti-unification for feature terms [A¨ıt-Kaci and Sasaki, 2001; Armengol and Plaza, 2000], for term-graphs [Baumgartner et al., 2018], nominal [Baumgartner et al., 2015; Schmidt-Schauß and NantesSobrinho, 2022] and approximate anti-unification [A¨ıt-Kaci and Pasi, 2020; Kutsia and Pau, 2022; Pau, 2022]. These generalization problems all fit in our general framework.

3 Generalization in First-Order Theories

3.1 First-Order Syntactic Generalization (FOSG)

Plotkin [1970] and Reynolds [1970] introduced FOSG, the simplest and best-known among generalization problems in logic. The objects are first-order terms, and mappings are substitutions that map variables to terms such that all but finitely many variables are mapped to themselves. Application of a substitution σ to a term t is denoted by tσ, which is the term obtained from t by replacing all variable occurrences by their images under σ. Table 1 specifies the concrete instances of the abstract parameters, and consistency follows from the transitivity of ⪰. The relation ≡P holds between terms that are obtained by variable renaming from each other (e.g. f(x1, g(x1, y1)) and f(x2, g(x2, y2)). The most ⪰-preferred .=-generalizations are called least general generalizations (lggs). Two terms always have an lgg unique up to variable renaming. Plotkin [1970], Reynolds [1970], and Huet [1976] introduced algorithms for computing lggs.

Example 1. Let s1 = f(a, g(a, b)) and s2 = f(c, g(c, d)). Their lgg is t = f(x, g(x, y)), which is unique up to variable names. Substitutions σ1 = {x ↦→ a, y ↦→ b} and σ2 = {x ↦→ c, y ↦→ d} give s1 and s2 from t: tσi = si, i = 1, 2. Note that s1 and s2 have other generalizations as well, e.g., f(x, g(y, z)) or x, but they are not the ⪰-preferred ones.

3.2 First-Order Equational Generalization (FOEG)

FOEG requires extending syntactic equality to equality modulo a given set of equations. Many algebraic theories are characterized by axiomatizing properties of function symbols via (implicitly universally quantified) equalities. Some wellknown equational theories include

• commutativity, C({f}), f(x, y) ≈ f(y, x).
• associativity, A({f}), f(f(x, y), z) ≈ f(x, f(y, z)).
• associativity and commutativity, AC({f}), above equalities for the same function symbol f.
• unital symbols, U({(f, e)}), f(x, e) ≈ x and f(e, x) ≈ x (e is both left and right unit element for f).
• idempotency, I({f}), f(x, x) ≈ x.

Given a set of axioms E, the equational theory induced by E is the least congruence relation on terms containing E and closed under substitution application. (Slightly abusing the notation, it is also usually denoted by E.) When a pair of terms (s, t) belongs to such an equational theory, we say that s and t are equal modulo E and write s .=E t.

In a theory, we may have several symbols that satisfy the same axiom. For instance, C({f, g}) denotes the theory where f and g are commutative; AC({f, g})C({h}) denotes the theory where f and g are associative-commutative and h is commutative; U({(f, ef ), (g, eg)}) denotes the theory where ef and eg are the unit elements for f and g, respectively. We follow the convention that if the equational theory is denoted by E1(S1) · · · En(Sn), then Si ∩Sj = ∅ for each 1 ≤ i ̸= j ≤ n.

Some results depend on the number of symbols that satisfy the associated equational axioms. We use a special notation for that: For a theory E, the notation E1 stands for E(S), where the set S contains a single element; E>1 stands for E(S) where S contains finitely many, but at least two elements. When we write only E, we mean the equational theory E(S) with a finite set of symbols S that may contain one or more elements.

We can extend this notation to combinations: for instance, (AU)>1 stands for a theory that contains at least two function symbols, e.g., f and g, that are associative and unital (with unit elements ef and eg).

Table 2 shows how FOEG fits into our general framework.

Example 2. Consider a theory E and terms s and t.

If E = AC({f}), s = f(f(a, a), b), and t = f(f(b, b), a), then mcsgE(s, t) = {f(f(x, x), y), f(f(x, a), b)}. If we had variables instead of a and b, e.g., if s = f(f(z, z), v) and t = f(f(v, v), z), then mcsgE(s, t) = {f(f(x, x), y)}, because f(f(x, z), v) (the counterpart of f(f(x, a), b)) is more general (less preferred) than f(f(x, x), y).

If E = U({(f, e)}), s = g(f(a, c), a), t = g(c, b), then mcsgE(s, t) = {g(f(x, c), f(y, x)), g(f(x, c), f(x, y))}. To see why, e.g., g(f(x, c), f(y, x)) from this set is a U-generalization of s and t, consider substitutions σ = {x ↦→ a, y ↦→ e} and ϑ = {x ↦→ e, y ↦→ b}. Then g(f(x, c), f(y, x))σ = g(f(a, c), f(e, a)) .=U s and g(f(x, c), f(y, x))ϑ = g(f(e, c), f(b, e)) .=U t.

If E = U({(f, ef), (g, eg)}), s = ef , and t = eg, then mcsgE(s, t) does not exist: Any complete set of generalizations of s and t contains elements g and g′ such that g ≻U g′ (where ≻U is the strict part of ⪰U) [Cerna and Kutsia, 2020c]. If E = I({h}), s = h(a, b), t = h(b, a), then mcsgE(s, t) = S∞, where S∞ is the limit of the following construction:

Alpuente et al. [2014] study anti-unification over A, C, and AC theories in a more general, order-sorted setting and provide the corresponding algorithms. In [Alpuente et al.,

2022], they also consider combining these theories with U in a particular order-sorted signature that guarantees finitary type and completeness of the corresponding algorithms.

Burghardt [2005] proposed a grammar-based approach to the computation of equational generalizations: from a regular tree grammar that describes the congruence classes of the given terms t1 and t2, a regular tree grammar describing a complete set of E-generalizations of t1 and t2 is computed. This approach works for equational theories that lead to regular congruence classes. Otherwise, one can use some heuristics to approximate the answer, but completeness is not guaranteed.

Baader [1991] considers anti-unification over so-called commutative theories, a concept covering commutative monoids (ACU), commutative idempotent monoids (ACUI), and Abelian groups. The object set is restricted to terms built using variables and the algebraic operator. Anti-unification over commutative theories in this setting is always unitary.

Results for some theory types are summarized as follows:

• A, C, AC: type ω [Alpuente et al., 2014];
• U1 , (AU)1 , (CU)1 , (ACU)1 : type ω. U>1 , (ACU)>1 , (CU)>1 , (AU)>1 , (AU)(CU): type 0 (but their linear variants have type ω) [Cerna and Kutsia, 2020c];
• I, AI, CI: type∞ [Cerna and Kutsia, 2020b];
• (UI)>1 , (AUI)>1 , (CUI)>1 , (ACUI)>1 , semirings: type 0 [Cerna, 2020];
• Commutative theories: type 1 [Baader, 1991].

3.3 First-Order Clausal Generalization (FOCG)

Clauses are disjunctions of literals (atomic formulas or their negations). Generalization of first-order clauses can be seen as a special case of FOEG, with one ACUI symbol (disjunction) that appears only as the top symbol of the involved expressions. It is one of the oldest theories for which generalization was studied (see, e.g., [Plotkin, 1970]). Clausal generalization (with various base relations) has been successfully used in relational learning. Newer work uses rigidity functions to construct generalizations and is used for clone detection in logic programs [Yernaux and Vanhoof, 2022b].

An important notion to characterize clausal generalization is θ-subsumption [Plotkin, 1970]: It can be defined by treating disjunction as an ACUI symbol, but a more natural definition considers a clause L1 ∨ · · · ∨ Ln as the set of literals {L1, . . . ,Ln}. Then we say the clause C θ-subsumes the clause D, written C ⪯ D, if there exists a substitution θ such that Cθ ⊆ D (where the notation Sθ is defined as {sθ | s ∈ S} for a set S). The base relation B is ⊆, generalization mappings inMare first-order substitutions, and the preference relation P is the inverse of θ-subsumption ⪰.

Clausal generalization problem is unitary: a finite set of clauses always possesses a unique lgg up to θ-subsumption equivalence ≡P. Its size can be exponential in the number of clauses it generalizes.

Example 3. [Idestam-Almquist, 1995] Let D1 = (p(a) ← q(a), q(b)) and D2 = (p(b) ← q(b), q(x)). Then both C1 = (p(y) ← q(y), q(b)) and C2 = (p(y) ← q(y), q(b), q(z), q(w)) are lggs of D1 and D2. It is easy to see that C1 ≡P C2.

Plotkin generalized the notion of θ-subsumption to relative θ-subsumption, taking into account background knowledge. Given knowledge T as a set of clauses and a clause C, we write Res(C, T ) = R if there exists a resolution derivation of the clause R from T using C exactly once. 1 The notion of relative θ-subsumption can be formulated in the following way: A clause C θ-subsumes a clause D relative to a theory T , denoted C ⪯T D, iff there exists a clause R such that Res(C, T ) = R and R ⪯ D. To accommodate this case within our framework, we modify mappings in M to be the composition of a resolution derivation and substitution application, and use P = ⪰T . The minimal complete set of relative generalizations of a finite set of clauses can be infinite.

Idestam-Almquist [1995] introduced another variant of clausal generalization, proposing a different base relation: T-implication ⇒T . Due to space limitations, we refrain from providing the exact definition. It is a reflexive non-transitive relation taking into account a set T of ground terms extending generalization under θ-subsumption to generalization under a special form of implication. Unlike implication, it is decidable. Note that Plotkin introduced θ-subsumption as an incomplete approximation of implication. Idestam-Almquist [1997] lifted relative clausal generalization to T-implication.

Idestam-Almquist [2009] introduced a modification of relative clausal generalization, called asymmetric relative minimal generalization, implementing it in ProGolem. Kuˇzelka et al. [2012] studied a bounded version of clausal generalization motivated by practical applications in clause learning. Yernaux and Vanhoof [2022a] consider different base relations for generalizing unordered logic program goals.

3.4 Unranked First-Order Generalization (UFOG)

In unranked languages, symbols do not have a fixed arity. They are often referred to as variadic, polyadic, flexary, or flexible arity symbols. To take advantage of such variadicity, unranked languages contain hedge variables (which stand for hedges: finite, possibly empty sequences of terms) together with individual variables (which stand for single terms). In this section, individual variables are denoted by x, y, z, and hedge variables by X, Y, Z. Terms of the form f() are written as f . Hedges are usually put in parentheses, but a singleton hedge (t) is written as t. Substitutions map individual variables to terms and hedge variables to hedges, flattening after application.

Example 4. Let H = (X, f(X), g(x, Y )) be a hedge and σ = {x ↦→ f(a, a), X ↦→ (), Y ↦→ (x, g(a,Z))} be a substitution where () is the empty hedge. Then Hσ = (f, g(f (a, a), x, g(a, Z))).

We provide concrete values for UFOG with respect to the parameters of our general framework in Table 3.

Kutsia et al. [2014] studied unranked generalization and proposed the rigid variant forbidding neighboring hedge variables within generalizations. Moreover, an extra parameter called the rigidity function is used to select a set of common subsequences of top function symbols of hedges to be generalized. The most natural choice for the rigidity function computes the set of longest common subsequences (lcs's) of its arguments. However, there are other interesting rigidity functions (e.g., lcs's with the minimal length bound, a single lcs chosen by some criterion, longest common substrings, etc.). The rigid variant is also finitary. Its minimal complete set is denoted by mcsgR. Kutsia et al. [2014] describe an algorithm that computes this set. We use the lcs rigidity function below.

1 In Plotkin's original definition, the derivation uses C at most once. Here we follow the exposition from [Idestam-Almquist, 1997].

Example 5. Consider singleton hedges H1 = g(f(a), f(a)) and H2 = g(f(a), f). For the unrestricted generalization case, mcsg(H1, H2) = {g(f(a), f(X)), g(f(X, Y ), f(X)), g(f(X, Y ), f(Y ))}. To see why, e.g., g(f(X, Y ), f(Y )) is a generalization of H1 and H2, consider substitutions σ = {X ↦→ (), Y ↦→ a} and ϑ = {X ↦→ a, Y ↦→ ()}. Then g(f(X, Y ), f(Y ))σ = H1 and g(f(X, Y ), f(Y ))ϑ = H2.

For a rigid variant, mcsgR(H1,H2) = {g(f(a), f(X))}. The other two elements contained in the unrestricted mcsg are now dropped because they contain hedge variables next to each other, which is forbidden in rigid variants.

Example 6. Let H1 = (f(a, a), b, f(c), g(f(a), f(a)) and H2 = (f(b, b), g(f(a), f)). Then mcsgR(H1,H2) = {(f (x, x), X, g(f (a), f (Y ))), (X, f (Y ), g(f (a), f (Z))}.

The elements of this set originate from two longest common subsequences of symbols at the top level: In both cases the lcs is f followed by g, but in the former we match the top symbols of f(a, a) and g(f(a), f(a)) from H1 to top symbols of H2, while in the latter we match f(c) and g(f(a), f(a)) from H1.

For the rigidity function computing longest common substrings, mcsgR(H1, H2) = {(X, f (Y ), g(f (a), f (Z)))}.

Unranked terms and hedges can be used to model semistructured documents, program code, execution traces, etc. Yamamoto et al. [2001] investigated unranked anti-unification in the context of inductive reasoning over hedge logic programs. They consider a special case (without individual variables), where hedges do not contain duplicate occurrences of the same hedge variable and any set of sibling arguments contains at most one hedge variable. Such hedges are called simple ones. Note that this problem as well as other related problems such as word generalization [Biere, 1993] or AU-generalization can be also solved by the algorithms from [Kutsia et al., 2014].

Anti-unification for unranked first-order terms was generalized to unranked second-order terms [Baumgartner and Kutsia, 2017] and to unranked term-graphs [Baumgartner et al., 2018]. Both problems are finitary and fit into our general framework.

3.5 Description Logics

Description logics (DLs) are important formalisms for knowledge representation and reasoning. They are decidable fragments of first-order logic. The basic syntactic building blocks in DLs are concept names (unary predicates), role names (binary predicates), and individual names (constants). Starting from these constructions, complex concepts and roles are built using constructors, which determine the expressive power of the DL. For DLs considered in this section, we show how concept descriptions (denoted by C and D) are defined inductively over the sets of concept names NC and role names NR. Below we provide definitions for the description logics EL, FLE, ALE, and ALEN, where P ∈ NC is a primitive concept, r ∈ NR is a role name, and n ∈ N.

An interpretation I = (∆I, ·I ) consists of a non-empty set ∆I , called the interpretation domain, and a mapping ·I , called the extension mapping. It maps every concept name P ∈ NC to a set P I ⊆ ∆I, and every role name r ∈ NR to a binary relation rI ⊆ ∆I×∆I . The other concept descriptions are defined as follows: ⊤I = ∆I; (C ⊓ D)I = C I ∩ DI ; (∃r.C)I = {d ∈ ∆I | ∃e. (d, e) ∈ rI ∧e ∈ C I }; (∀r.C)I = {d ∈ ∆I | ∀e. (d, e) ∈ rI ⇒ e ∈ C I }; (R nr)I = {d ∈ ∆I | #{e | (d, e) ∈ rI }Rn} where R ∈ {≥, ≤}.

Like in FOCG, subsumption is important for defining the generalization problem. A concept description C is subsumed by D, written C ⊑ D, if C I ⊆ DI holds for all interpretations I. (We write C ≡ D if C and D subsume each other.) A concept description D is called a least common subsumer of C1 and C2, if (i) C1 ⊑ D and C2 ⊑ D and (ii) if there exists D′ such that C1 ⊑D′ and C2 ⊑D′ , then D ⊑D′ .

The problem of computing the least common subsumer of two or more concept descriptions can be seen as a version of the problem of computing generalizations in DLs. It has been studied, e.g., in [Cohen and Hirsh, 1994; Baader et al., 1999; K¨usters and Molitor, 2001; Baader et al., 2007].

Example 7 ([Baader et al., 1999]). Assume the DL is EL, C = P ⊓ ∃r.(∃r.(P ⊓ Q) ⊓ ∃s.Q) ⊓ ∃r.(P ⊓ ∃s.P ), and D = ∃r.(P⊓∃r.P⊓∃s.Q). Then ∃r.(∃r.P⊓∃s.Q)⊓∃r.(P⊓∃s.⊤) is the least common subsumer of C and D.

Example 8 ([K¨usters and Molitor, 2001]). Assume the DL is ALEN, C = ∃r.(P ⊓ A1) ⊓ ∃r.(P ⊓ A2) ⊓ ∃r.(¬P ⊓ A1) ⊓ ∃r.(Q ⊓ A3) ⊓ ∃r.(¬Q ⊓ A3) ⊓ (≤ 2 r), and D = (≥ 3 r)⊓∀r.(A1⊓A2⊓A3). Then (≥ 2 r)⊓∀r : (A1⊓A3)⊓∃r : (A1 ⊓ A2 ⊓ A3) is the least common subsumer of C and D.

Table 4 shows how results for EL, FLE, ALE, and ALEN fit into our framework. Some other results about generalizations in DLs include the computation of the least common subsumer with respect to a background terminology [Baader et al., 2007], computation of the least common subsumer and the most specific concept with respect to a knowledge base [Jung et al., 2020], and anti-unification [Konev and Kutsia, 2016].

4 Higher-Order Generalization

Higher-Order generalization mainly concerns generalization in simply-typed lambda calculus, although it has been studied in other theories of Berendregt's λ-cube [Barendregt et al., 2013] and related settings (see [Pfenning, 1991]).

We consider lambda terms defined by the grammar t ::= x | c | λx.t | (t t), where x is a variable and c is a constant. A simple type τ is either a basic type δ or a function type τ → τ. We use the standard notions of λ-calculus such as bound and free variables, subterms, α-conversion, β-reduction, η-long β-normal form, etc. (see, e.g., [Barendregt et al., 2013]). Substitutions are (type-preserving) mappings from variables to lambda terms. They form the set M. In this section, x, y, z are used from bound variables and X, Y, Z for free ones.

4.1 Higher-Order αβη-Generalization (HOGαβη)

Syntactic anti-unification in simply-typed lambda calculus is generalization modulo α, β, η rules (i.e., the base relation is equality modulo αβη, which we denote by ≈ in this section). Terms are assumed to be in η-long β-normal form. The preference relation is ≿: s ≿ t iff s ≈ tσ for a substitution σ. Its inverse is denoted by ≾. Cerna and Buran [2022] show that unrestricted generalization in this theory is nullary:

Example 9. Let s = λxλy.f(x) and t = λxλy.f(y). Then any complete set of generalizations of s and t contains ≾- comparable elements. For instance, if such a set contains a generalization r = λx.λy.f(X(x, y)), there exists an infinite chain of less and less general generalizations rσ ≾ rσσ ≾ . . . with σ = {X ↦→ λx.λy.X(X(x, y), X(x, y))}.

Cerna and Kutsia [2019] proposed a generic framework that accommodates several special unitary variants of generalization in simply-typed lambda calculus. The framework is motivated by two desired properties of generalizations: to maximally keep the top-down common parts of the given terms (top-maximality) and to avoid the nesting of generalization variables (shallowness). These constraints lead to the top-maximal shallow (tms) generalization variants that allow some freedom in choosing the subterms occurring under generalization variables. Possible unitary variants are as follows: projective (pr: entire terms), common subterms (cs: maximal common subterms), other cs-variants where common subterms are not necessarily maximal but satisfy restrictions discussed in [Libal and Miller, 2022] such as (relaxed) functions-asconstructors (rfc,fc), and patterns (p). The time complexity of computing pr and p variants is linear in the size of input terms, while for the other cases, it is cubic.

Example 10. For terms λx. f(h(g(g(x))), h(g(x)), a) and λx. f(g(g(x)), g(x), h(a)), various top-maximal shallow lggs are pr-lgg: λx.f(X(h(g(g(x))), g(g(x))),X(h(g(x)), g(x)),X(a,h(a))), cs-lgg: λx.f(X(g(g(X(g(x)),Z(a)), rfclgg: λx.f(X(g(g(x))),X(g(x)),Z), fc-lgg: λx.f(X(g(x)), Y (g(x)), Z), and p-lgg: λx.f(X(x), Y (x), Z).

Table 5 relates HOGαβη to the general framework.

The linear variant of αβη-Generalization over higher-order patterns was used by [Pientka, 2009] to develop a higher-order term-indexing algorithm based on substitution trees. Insertion into the substitution requires computing the lgg of a given higher-order pattern and a higher-order pattern already in the substitution tree. Feng and Muggleton [1992] consider αβδ0ηGeneralization over a fragment of simply-typed lambda terms they refer to as λM, where δ0 denotes an additional decomposition rule for constructions similar to if-then-else. Similar to top-maximal shallow lambda terms, λM allows constants within the arguments to generalization variables. Due to space constraints, we refrain from discussing in detail [Pfenning, 1991] work on anti-unification in the calculus of constructions, where he describes an algorithm for the pattern variant. This work fits our general framework by adjusting the parameters used for αβη-Generalization over higher-order patterns.

4.2 Higher-Order Equational Generalization

Cerna and Kutsia [2020a] studied the pattern variant of higher-order equational generalization (HOEG) in simplytyped lambda calculus involving A, C, U axioms and their combinations (Table 6). In addition, they investigated fragments for which certain optimal generalizations may be computed fast. It was shown that pattern HOEG in A, C, AC theories is finitary. The same is true for the linear pattern variant of HOEG in A, C, U theories and their combinations.

The generalization problem for the considered fragments is unitary when only optimal solutions are considered. Optimality means that the solution should be at least as good as the αβη-lgg. Fragments allowing fast computation of optimal solutions (in linear, quadratic, or cubic time) were identified.

4.3 Polymorphic Higher-Order Generalization

Lu et al. [2000] consider generalization within the polymorphic lambda calculus, typically referred to as λ2 (Table 7). Unlike αβη-Generalization presented above, terms are not required to be of the same type to be generalizable. While similar holds regarding [Pfenning, 1991], Lu et al. [2000] do not restrict themselves to the pattern variant but instead restrict the preference relation. They use a restricted form of the application order, i.e. s ≿ t iff there exists terms and types r1, . . . , rn such that sr1 · · · rn ≈ t, in other words, sr1 · · · rn β-reduces to t. They restrict r1, . . . , rn to subterms of t and introduce variable-freezing to deal with bound variable order. Mappings are also based on β-reduction.

4.4 Second-Order Combinator Generalization

Hasker [1995] considers an alternative representation of second-order logic using combinators instead of lambda abstractions (Table 8). Unlike lambda terms, where the application of one term to another is performed via substitution, combinators are special symbols, each associated with a precise axiomatic definition of their effect on the input terms. Note that here substitution concerns term normalization and not the generalization problem. The generalization problems and algorithms from [Hasker, 1995] still require second-order substitutions. He considers monadic combinators, which take a single argument, and cartesian combinators, which generalize monadic combinators by allowing multiple arguments via a pairing function. Cartesian combinator generalization is nullary as the pairing function can act as a storage for irrelevant constructions. The author addresses this by introducing a concept of relevance resulting in finitary generalization problem.

5 Applications

Typical applications fall into one of the following areas: learning and reasoning, synthesis and exploration, and analysis and repair. Below we briefly discuss the state of the art in these areas and, when possible, the associated type of generalization.

5.1 Learning and Reasoning

Inductive logic programming systems based on inverse entailment, such as ProGolem [Muggleton et al., 2009], Aleph [Srinivasan, 2001] and Progol [Muggleton, 1995] used (relative) θ-subsumption, or variants of it, to search for generalizations of the most specific clause entailing a single example (the bottom clause). The ILP system Popper, developed by Cropper and Morel [2021] uses θ-subsumption-based constraints to iteratively simplify the search space. Recent extensions of this system, such as Hopper [Purgal et al., 2022], and NOPI [Cerna and Cropper, 2023] consider similar techniques over a more expressive hypothesis space.

Several authors have focused on generalization for analogical reasoning. Krumnack et al. [2007] use a restricted form of higher-order generalization to develop useful analogies. Weller and Schmid [2006] use the equational generalization method introduced by Burghardt [2005] to solve proportional analogies, i.e. "A is to B as C is to ?". Sotoudeh and Thakur [2020] discuss generalization as an tool for analogical reasoning about programs. Generalization is used in case-based reasoning [Onta˜n´on and Plaza, 2007] literature as a method to encode coverage of cases by a prediction.

Related research concerning concept blending and mathematical reasoning builds upon Heuristic-Driven Theory Projection, using a form of higher-order anti-unification [Schwering et al., 2009]. Example works in this area include [Guhe et al., 2011] and [Mart´ınez et al., 2017]. Learning reasoning rules using anti-unification from quasi-natural language sentences is discussed in [Yang and Deng, 2021]. Learning via generalization of linguistic structures has found applications in the development of industrial chatbots [Galitsky, 2019].

5.2 Synthesis and Exploration

The programming by example (pbe) paradigm is an inductive synthesis method concerned with the generation of a program within a domain-specific language (dsl) that generalizes input-output examples [Raza et al., 2014]. Efficient search through the dsl exploits purpose-built generalization methods [Mitchell, 1982]. Foundational work in this area include [Gulwani, 2011] and [Polozov and Gulwani, 2015]. Recent developments include [Dong et al., 2022], where the authors specifically reference unranked methods for synthesis within robotic process automation, and [Feser et al., 2015], where functional transformations of data structures are synthesized. An earlier tool on inductive synthesis of functional programs is IGOR II [Hofmann, 2010]. It is based on [Kitzelmann and Schmid, 2006] and exploits the basic syntactic generalization methods [Plotkin, 1970]. Johansson et al. [2011] use a form of generalization for conjecture synthesis.

Babble [Cao et al., 2023] is a method for theory exploration and compression exploiting FOEG and term-graph representations to find functions that compress the representation of other functions in a library. Bowers et al. [2023] focus on the learning aspects of the problem. Singher and Itzhaky [2021] use generalizing templates as part of the synthesis process.

5.3 Analysis and Repair

Bulychev and Minea [2008] introduced anti-unification as a method to detect clones in software and repositories (see also [Bulychev et al., 2009]). This research was further developed for specific use cases: Li and Thompson [2010] investigated clone detection in Erlang, and Yernaux and Vanhoof [2022b] studied clone detection in constraint logic programs.

Sinha [2008] and Arusoaie and Lucanu [2022], use antiunification to implement efficient symbolic execution, a type of software analysis . Hasker [1995] used SOCG to develop a derivation replay approach to automate some aspects of programming through templating. Related to derivation replay is the work of Barwell et al. [2018] concerning parallel recursion scheme detection. Maude [Clavel et al., 2002] is a declarative programming language useful for software verification tasks. It has been extended by order-sorted, equational, and syntactic anti-unification methods.

As discussed byWinter et al. [2022], recent investigations exploit anti-unification to provide program repair and bug detection capabilities. Sakkas et al. [2020] use variants of unranked hedge anti-unification as a templating mechanism for providing repairs based on type errors. This approach is also taken by the authors of Getafix, [Bader et al., 2019], and REVISAR, [de Sousa et al., 2021]. Rex, developed by Mehta et al. [2020], takes a similar approach for repairing misconfigured services, while [Siddiq et al., 2021] uses unranked hedge anti-unification to detect and repair SQL injection vulnerabilities. Zhang et al. [2022] use generalization techniques to develop edit templates from edit sequences in repositories.

6 Future Directions

Although research on anti-unification has a several decadeslong history, most of the work in this area was driven by practical applications, and the theory of anti-unification is relatively less developed (in comparison to, e.g., its dual technique of unification). To address this shortcoming, we list some interesting future work directions which, in our opinion, can significantly contribute to improving the state-of-the-art.

• Characterization of anti-unification over equational theories based on the function symbols allowed in problems alongside variables (only equational symbols, equational symbols+free constants, or equational, etc.). This choice might influence e.g., generalization type.
• Developing methods for combining anti-unification algorithms for disjoint equational theories.
• Characterization of equational theories exhibiting similar behavior and properties for generalization problems.
• Studying the influence of the preference relation choice on the type and solution set of generalization problems.
• Studying computational complexity and optimizations.

Acknowledgments

Supported by Czech Science Foundation Grant No. 2206414L, Austrian Science Fund project P 35530, and Cost Action CA20111 EuroProofNet.