Anti-unification (computer science)
Anti-unification is the process of constructing a generalization common to two given symbolic expressions. As in unification, several frameworks are distinguished depending on which expressions (also called terms) are allowed, and which expressions are considered equal. If variables representing functions are allowed in an expression, the process is called "higher-order anti-unification", otherwise "first-order anti-unification". If the generalization is required to have an instance literally equal to each input expression, the process is called "syntactical anti-unification", otherwise "E-anti-unification", or "anti-unification modulo theory". An anti-unification algorithm should compute  for given expressions a complete, and minimal generalization set, that is, a set covering all generalizations, and containing no redundant members, respectively. Depending on the framework, a complete and minimal generalization set may have one, finitely many, or possibly infinitely many members, or may not exist at all; it cannot be empty, since a trivial generalization exists in any case. For first-order syntactical anti-unification, Gordon Plotkin gave an algorithm that computes a complete and minimal singleton generalization set containing the so-called "least general generalization" (lgg). Anti-unification should not be confused with dis-unification. The latter  means the process of solving systems of inequations, that is of finding values for the variables such that all given inequations are satisfied. This task is quite different from finding generalizations. Prerequisites. Formally, an anti-unification approach presupposes First-order term. Given a set formula_12 of variable symbols, a set formula_13 of constant symbols and sets formula_14 of formula_15-ary function symbols, also called operator symbols, for each natural number formula_16, the set of (unsorted first-order) terms formula_2 is recursively defined to be the smallest set with the following properties: For example, if "x" ∈ "V" is a variable  symbol, 1 ∈ "C" is a constant symbol, and add ∈ "F" is a binary function symbol, then "x" ∈ "T", 1 ∈ "T", and (hence) add("x",1) ∈ "T" by the first, second, and third term building rule, respectively. The latter term is usually written as "x"+1, using Infix notation and the more common operator symbol + for convenience. Substitution. A "substitution" is a mapping formula_19 from variables to terms; the notation formula_20 refers to a substitution mapping each variable formula_21 to the term formula_22, for formula_23, and every other variable to itself. Applying that substitution to a term is  written in postfix notation as formula_24; it means to (simultaneously) replace every occurrence of each variable formula_21 in the term by formula_22. The result of applying a substitution to a term is called an "instance" of that term . As a first-order example, applying the substitution formula_27 to the term Generalization, specialization. If a term formula_4 has an instance equivalent to a term formula_5, that is, if formula_30 for some substitution formula_31, then formula_4 is called "more general" than formula_5, and formula_5 is called "more special" than, or "subsumed" by, formula_4. For example, formula_36 is more general than formula_37 if  formula_7 is commutative, since then formula_39. If formula_1 is literal (syntactic) identity of terms, a term may be both more general and more special than another one only if both terms differ just in their variable names, not in their syntactic structure; such terms are called "variants", or "renamings" of each other. For example, formula_41 is a variant of formula_42, since formula_43 and formula_44. However, formula_41 is "not" a variant of formula_46, since no substitution can transform the latter term into the former one, although formula_47 achieves the reverse direction. The latter term is hence properly more special than the  former one. A substitution formula_31 is "more special" than, or "subsumed" by, a substitution formula_49 if formula_50 is more special than formula_51 for each variable formula_52. For example, formula_53 is more special than formula_54, since formula_55 and formula_56 is more special than formula_57 and formula_58, respectively. Anti-unification problem, generalization set. An "anti-unification problem" is a pair formula_59 of terms. A term formula_4 is a common "generalization", or "anti-unifier", of formula_61 and formula_62 if formula_63 and formula_64 for some substitutions formula_65. For a given anti-unification problem, a set formula_66 of anti-unifiers is called "complete" if each  generalization subsumes some term formula_67; the set formula_66 is called "minimal" if none of its members subsumes another one. First-order syntactical anti-unification. The framework of first-order syntactical anti-unification is based on formula_2 being the set of "first-order terms" (over some given set formula_12 of variables, formula_13 of constants and formula_14 of formula_15-ary function symbols) and on formula_1 being "syntactic equality". In this framework, each anti-unification problem formula_59 has a complete, and obviously minimal, singleton solution set formula_76. Its member formula_4 is called the "least general generalization (lgg)" of the problem, it has an  instance syntactically equal to formula_61 and another one syntactically equal to formula_62. Any common generalization of formula_61 and formula_62 subsumes formula_4. The lgg is unique up to variants: if formula_83 and formula_84 are both complete and minimal solution sets of the same syntactical anti-unification problem, then formula_85 and formula_86 for some terms formula_87 and formula_88, that are renamings of each other. Plotkin has given an algorithm to compute the lgg of two given terms. It presupposes an injective mapping formula_89, that is, a mapping assigning each pair formula_90 of terms an own variable formula_91, such that no two pairs  share the same variable. The algorithm consists of two rules: For example, formula_92; this least general generalization reflects the common property of both inputs of being square numbers. Plotkin used his algorithm to compute the "relative least general generalization (rlgg)" of two clause sets in first-order logic, which was the basis of the Golem approach to inductive logic programming.