Anti-unification (computer science)

Given a set ${\displaystyle V}$ of variable symbols, a set ${\displaystyle C}$ of constant symbols and sets ${\displaystyle F_{n}}$ of ${\displaystyle n}$-ary function symbols, also called operator symbols, for each natural number ${\displaystyle n\geq 1}$, the set of (unsorted first-order) terms ${\displaystyle T}$ is recursively defined to be the smallest set with the following properties:[3]

• every variable symbol is a term: V ⊆ T,
• every constant symbol is a term: C ⊆ T,
• from every n terms t₁,...,t_n, and every n-ary function symbol f ∈ F_n, a larger term ${\displaystyle f(t_{1},\ldots ,t_{n})}$ can be built.

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.

A substitution is a mapping ${\displaystyle \sigma :V\longrightarrow T}$ from variables to terms; the notation ${\displaystyle \{x_{1}\mapsto t_{1},\ldots ,x_{k}\mapsto t_{k}\}}$ refers to a substitution mapping each variable ${\displaystyle x_{i}}$ to the term ${\displaystyle t_{i}}$, for ${\displaystyle i=1,\ldots ,k}$, and every other variable to itself. Applying that substitution to a term t is written in postfix notation as ${\displaystyle t\{x_{1}\mapsto t_{1},\ldots ,x_{k}\mapsto t_{k}\}}$; it means to (simultaneously) replace every occurrence of each variable ${\displaystyle x_{i}}$ in the term t by ${\displaystyle t_{i}}$. The result tσ of applying a substitution σ to a term t is called an instance of that term t. As a first-order example, applying the substitution ${\displaystyle \{x\mapsto h(a,y),z\mapsto b\}}$ to the term

f(	x	, a, g(	z	), y)	yields
f(	h(a,y)	, a, g(	b	), y)	.

If a term ${\displaystyle t}$ has an instance equivalent to a term ${\displaystyle u}$, that is, if ${\displaystyle t\sigma \equiv u}$ for some substitution ${\displaystyle \sigma }$, then ${\displaystyle t}$ is called more general than ${\displaystyle u}$, and ${\displaystyle u}$ is called more special than, or subsumed by, ${\displaystyle t}$. For example, ${\displaystyle x\oplus a}$ is more general than ${\displaystyle a\oplus b}$ if ${\displaystyle \oplus }$ is commutative, since then ${\displaystyle (x\oplus a)\{x\mapsto b\}=b\oplus a\equiv a\oplus b}$.

If ${\displaystyle \equiv }$ 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, ${\displaystyle f(x_{1},a,g(z_{1}),y_{1})}$ is a variant of ${\displaystyle f(x_{2},a,g(z_{2}),y_{2})}$, since ${\displaystyle f(x_{1},a,g(z_{1}),y_{1})\{x_{1}\mapsto x_{2},y_{1}\mapsto y_{2},z_{1}\mapsto z_{2}\}=f(x_{2},a,g(z_{2}),y_{2})}$ and ${\displaystyle f(x_{2},a,g(z_{2}),y_{2})\{x_{2}\mapsto x_{1},y_{2}\mapsto y_{1},z_{2}\mapsto z_{1}\}=f(x_{1},a,g(z_{1}),y_{1})}$. However, ${\displaystyle f(x_{1},a,g(z_{1}),y_{1})}$ is not a variant of ${\displaystyle f(x_{2},a,g(x_{2}),x_{2})}$, since no substitution can transform the latter term into the former one, although ${\displaystyle \{x_{1}\mapsto x_{2},z_{1}\mapsto x_{2},y_{1}\mapsto x_{2}\}}$ achieves the reverse direction. The latter term is hence properly more special than the former one.

A substitution ${\displaystyle \sigma }$ is more special than, or subsumed by, a substitution ${\displaystyle \tau }$ if ${\displaystyle x\sigma }$ is more special than ${\displaystyle x\tau }$ for each variable ${\displaystyle x}$. For example, ${\displaystyle \{x\mapsto f(u),y\mapsto f(f(u))\}}$ is more special than ${\displaystyle \{x\mapsto z,y\mapsto f(z)\}}$, since ${\displaystyle f(u)}$ and ${\displaystyle f(f(u))}$ is more special than ${\displaystyle z}$ and ${\displaystyle f(z)}$, respectively.

An anti-unification problem is a pair ${\displaystyle \langle t_{1},t_{2}\rangle }$ of terms. A term ${\displaystyle t}$ is a common generalization, or anti-unifier, of ${\displaystyle t_{1}}$ and ${\displaystyle t_{2}}$ if ${\displaystyle t\sigma _{1}\equiv t_{1}}$ and ${\displaystyle t\sigma _{2}\equiv t_{2}}$ for some substitutions ${\displaystyle \sigma _{1},\sigma _{2}}$. For a given anti-unification problem, a set ${\displaystyle S}$ of anti-unifiers is called complete if each generalization subsumes some term ${\displaystyle t\in S}$; the set ${\displaystyle S}$ is called minimal if none of its members subsumes another one.

• One associative and commutative operation: Pottier, Loic (Feb 1989), Algorithms des completion et generalisation en logic du premier ordre (These de doctorat); Pottier, Loic (1989), Generalisation de termes en theorie equationelle – Cas associatif-commutatif, INRIA Report, vol. 1056, INRIA
• Commutative theories: Baader, Franz (1991). "Unification, Weak Unification, Upper Bound, Lower Bound, and Generalization Problems". Proc. 4th Conf. on Rewriting Techniques and Applications (RTA). LNCS. Vol. 488. Springer. pp. 86–91. doi:10.1007/3-540-53904-2_88.
• Free monoids: Biere, A. (1993), Normalisierung, Unifikation und Antiunifikation in Freien Monoiden (PDF), Univ. Karlsruhe, Germany
• Regular congruence classes: Heinz, Birgit (Dec 1995), Anti-Unifikation modulo Gleichungstheorie und deren Anwendung zur Lemmagenerierung, GMD Berichte, vol. 261, TU Berlin, ISBN 978-3-486-23873-0; Burghardt, Jochen (2005). "E-Generalization Using Grammars". Artificial Intelligence. 165 (1): 1–35. arXiv:1403.8118. doi:10.1016/j.artint.2005.01.008. S2CID 5328240.
• A-, C-, AC-, ACU-theories with ordered sorts: Alpuente, Maria; Escobar, Santiago; Espert, Javier; Meseguer, Jose (2014). "A modular order-sorted equational generalization algorithm" (PDF). Information and Computation. 235: 98–136. doi:10.1016/j.ic.2014.01.006. hdl:2142/25871. Archived from the original (PDF) on 2016-03-05. Retrieved 2014-02-12.
• Purely idempotent theories: Cerna, David; Kutsia, Temur (2020). "Idempotent Anti-Unification". ACM Transactions on Computational Logic. 21 (2): 1–32. doi:10.1145/3359060. hdl:10.1145/3359060. S2CID 207861304.

• Taxonomic sorts: Frisch, Alan M.; Page, David (1990). "Generalisation with Taxonomic Information". AAAI: 755–761.; Frisch, Alan M.; Page Jr., C. David (1991). "Generalizing Atoms in Constraint Logic". Proc. Conf. on Knowledge Representation.; Frisch, A.M.; Page, C.D. (1995). "Building Theories into Instantiation". In Mellish, C.S. (ed.). Proc. 14th IJCAI. Morgan Kaufmann. pp. 1210–1216. CiteSeerX 10.1.1.32.1610.
• Feature terms: Plaza, E. (1995). "Cases as Terms: A Feature Term Approach to the Structured Representation of Cases". Proc. 1st International Conference on Case-Based Reasoning (ICCBR). LNCS. Vol. 1010. Springer. pp. 265–276. ISSN 0302-9743.
• Idestam-Almquist, Peter (Jun 1993). "Generalization under Implication by Recursive Anti-Unification". Proc. 10th Conf. on Machine Learning. Morgan Kaufmann. pp. 151–158.
• Fischer, Cornelia (May 1994), PAntUDE – An Anti-Unification Algorithm for Expressing Refined Generalizations (PDF), Research Report, vol. TM-94-04, DFKI
• A-, C-, AC-, ACU-theories with ordered sorts: see above

• Baumgartner, Alexander; Kutsia, Temur; Levy, Jordi; Villaret, Mateu (Jun 2013). Nominal Anti-Unification. Proc. RTA 2015. Vol. 36 of LIPIcs. Schloss Dagstuhl, 57-73. Software.

• Program analysis: Bulychev, Peter; Minea, Marius (2008). "Duplicate Code Detection Using Anti-Unification". Proceedings of the Spring/Summer Young Researchers' Colloquium on Software Engineering (2).; Bulychev, Peter E.; Kostylev, Egor V.; Zakharov, Vladimir A. (2009). "Anti-Unification Algorithms and their Applications in Program Analysis". {{cite journal}}: Cite journal requires |journal= (help)
• Code factoring: Cottrell, Rylan (Sep 2008), Semi-automating Small-Scale Source Code Reuse via Structural Correspondence (PDF), Univ. Calgary
• Induction proving: Heinz, Birgit (1994), Lemma Discovery by Anti-Unification of Regular Sorts, Technical Report, vol. 94–21, TU Berlin
• Information Extraction: Thomas, Bernd (1999). "Anti-Unification Based Learning of T-Wrappers for Information Extraction" (PDF). AAAI Technical Report. WS-99-11: 15–20.
• Case-based reasoning: Armengol, Eva; Plaza, Enric (2005). "Using Symbolic Descriptions to Explain Similarity on CBR". {{cite journal}}: Cite journal requires |journal= (help)
• Program synthesis: The idea of generalizing terms with respect to an equational theory can be traced back to Manna and Waldinger (1978, 1980) who desired to apply it in program synthesis. In section "Generalization", they suggest (on p. 119 of the 1980 article) to generalize reverse(l) and reverse(tail(l))<>[head(l)] to obtain reverse(l')<>m' . This generalization is only possible if the background equation u<>[]=u is considered.

Zohar Manna; Richard Waldinger (Dec 1978). A Deductive Approach to Program Synthesis (PDF) (Technical Note). SRI International. Archived from the original (PDF) on 2017-02-27. Retrieved 2017-09-29. — preprint of the 1980 article

Zohar Manna and Richard Waldinger (Jan 1980). "A Deductive Approach to Program Synthesis". ACM Transactions on Programming Languages and Systems. 2: 90–121. doi:10.1145/357084.357090. S2CID 14770735.

• Natural language processing: Amiridze, Nino; Kutsia, Temur (2018). "Anti-Unification and Natural Language Processing". Fifth Workshop on Natural Language and Computer Science, NLCS'18. EasyChair Preprints. EasyChair Report No. 203. doi:10.29007/fkrh. S2CID 49322739.