Anti-unification#First-order syntactical anti-unification

Formally, an anti-unification approach presupposes

• An infinite set V of variables. For higher-order anti-unification, it is convenient to choose V disjoint from the set of lambda-term bound variables.
• A set T of terms such that V ⊆ T. For first-order and higher-order anti-unification, T is usually the set of first-order terms (terms built from variable and function symbols) and lambda terms (terms containing some higher-order variables), respectively.
• An equivalence relation $\backslash equiv$ on $T$, indicating which terms are considered equal. For higher-order anti-unification, usually $t\; \backslash equiv\; u$ if $t$ and $u$ are alpha equivalent. For first-order E-anti-unification, $\backslash equiv$ reflects the background knowledge about certain function symbols; for example, if $\backslash oplus$ is considered commutative, $t\; \backslash equiv\; u$ if $u$ results from $t$ by swapping the arguments of $\backslash oplus$ at some (possibly all) occurrences.E.g. $a\; \backslash oplus\; (b\; \backslash oplus\; f(x))\; \backslash equiv\; a\; \backslash oplus\; (f(x)\; \backslash oplus\; b)\; \backslash equiv\; (b\; \backslash oplus\; f(x))\; \backslash oplus\; a\; \backslash equiv\; (f(x)\; \backslash oplus\; b)\; \backslash oplus\; a$ If there is no background knowledge at all, then only literally, or syntactically, identical terms are considered equal.

{{main|Term (logic)}}

Given a set $V$ of variable symbols, a set $C$ of constant symbols and sets $F\_n$ of $n$-ary function symbols, also called operator symbols, for each natural number $n\; \backslash geq\; 1$, the set of (unsorted first-order) terms $T$ is recursively defined to be the smallest set with the following properties:{{cite book|author1=C.C. Chang |author2=H. Jerome Keisler | title=Model Theory| year=1977| volume=73| publisher=North Holland|editor1=A. Heyting |editor2=H.J. Keisler |editor3=A. Mostowski |editor4=A. Robinson |editor5=P. Suppes | series=Studies in Logic and the Foundation of Mathematics}}; here: Sect.1.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 $f(t\_1,\backslash 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.

{{main|Lambda calculus}}

{{main|Substitution (logic)}}

A substitution is a mapping $\backslash sigma:\; V\; \backslash longrightarrow\; T$ from variables to terms; the notation $\backslash \{x\_1\; \backslash mapsto\; t\_1,\; \backslash ldots,\; x\_k\; \backslash mapsto\; t\_k\; \backslash \}$ refers to a substitution mapping each variable $x\_i$ to the term $t\_i$, for $i=1,\backslash ldots,k$, and every other variable to itself. Applying that substitution to a term {{mvar|t}} is written in postfix notation as $t\; \backslash \{x\_1\; \backslash mapsto\; t\_1,\; \backslash ldots,\; x\_k\; \backslash mapsto\; t\_k\; \backslash \}$; it means to (simultaneously) replace every occurrence of each variable $x\_i$ in the term {{mvar|t}} by $t\_i$. The result {{mvar|tσ}} of applying a substitution {{mvar|σ}} to a term {{mvar|t}} is called an instance of that term {{mvar|t}}.

As a first-order example, applying the substitution $\backslash \{x\; \backslash mapsto\; h(a,y),\; z\; \backslash mapsto\; b\backslash \}$ to the term

:

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

If $\backslash 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, $f(x\_1,a,g(z\_1),y\_1)$ is a variant of $f(x\_2,a,g(z\_2),y\_2)$, since $f(x\_1,a,g(z\_1),y\_1)\; \backslash \{\; x\_1\; \backslash mapsto\; x\_2,\; y\_1\; \backslash mapsto\; y\_2,\; z\_1\; \backslash mapsto\; z\_2\backslash \}\; =\; f(x\_2,a,g(z\_2),y\_2)$ and $f(x\_2,a,g(z\_2),y\_2)\; \backslash \{x\_2\; \backslash mapsto\; x\_1,\; y\_2\; \backslash mapsto\; y\_1,\; z\_2\; \backslash mapsto\; z\_1\backslash \}\; =\; f(x\_1,a,g(z\_1),y\_1)$.

However, $f(x\_1,a,g(z\_1),y\_1)$ is not a variant of $f(x\_2,a,g(x\_2),x\_2)$, since no substitution can transform the latter term into the former one, although $\backslash \{x\_1\; \backslash mapsto\; x\_2,\; z\_1\; \backslash mapsto\; x\_2,\; y\_1\; \backslash mapsto\; x\_2\; \backslash \}$ achieves the reverse direction.

The latter term is hence properly more special than the former one.

A substitution $\backslash sigma$ is more special than, or subsumed by, a substitution $\backslash tau$ if $x\; \backslash sigma$ is more special than $x\; \backslash tau$ for each variable $x$.

For example, $\backslash \{\; x\; \backslash mapsto\; f(u),\; y\; \backslash mapsto\; f(f(u))\; \backslash \}$ is more special than $\backslash \{\; x\; \backslash mapsto\; z,\; y\; \backslash mapsto\; f(z)\; \backslash \}$, since $f(u)$ and $f(f(u))$ is more special than $z$ and $f(z)$, respectively.

An anti-unification problem is a pair $\backslash langle\; t\_1,\; t\_2\; \backslash rangle$ of terms.

A term $t$ is a common generalization, or anti-unifier, of $t\_1$ and $t\_2$ if $t\; \backslash sigma\_1\; \backslash equiv\; t\_1$ and $t\; \backslash sigma\_2\; \backslash equiv\; t\_2$ for some substitutions $\backslash sigma\_1,\; \backslash sigma\_2$.

For a given anti-unification problem, a set $S$ of anti-unifiers is called complete if each generalization subsumes some term $t\; \backslash in\; S$; the set $S$ is called minimal if none of its members subsumes another one.

The framework of first-order syntactical anti-unification is based on $T$ being the set of first-order terms (over some given set $V$ of variables, $C$ of constants and $F\_n$ of $n$-ary function symbols) and on $\backslash equiv$ being syntactic equality.

In this framework, each anti-unification problem $\backslash langle\; t\_1,\; t\_2\; \backslash rangle$ has a complete, and obviously minimal, singleton solution set $\backslash \{t\backslash \}$.

Its member $t$ is called the least general generalization (lgg) of the problem, it has an instance syntactically equal to $t\_1$ and another one syntactically equal to $t\_2$.

Any common generalization of $t\_1$ and $t\_2$ subsumes $t$.

The lgg is unique up to variants: if $S\_1$ and $S\_2$ are both complete and minimal solution sets of the same syntactical anti-unification problem, then $S\_1\; =\; \backslash \{\; s\_1\backslash \}$ and $S\_2\; =\; \backslash \{\; s\_2\; \backslash \}$ for some terms $s\_1$ and $s\_2$, that are renamings of each other.

Plotkin has given an algorithm to compute the lgg of two given terms.

It presupposes an injective mapping $\backslash phi:\; T\; \backslash times\; T\; \backslash longrightarrow\; V$, that is, a mapping assigning each pair $s,t$ of terms an own variable $\backslash phi(s,t)$, such that no two pairs share the same variable.

From a theoretical viewpoint, such a mapping exists, since both $V$ and $T\; \backslash times\; T$ are countably infinite sets; for practical purposes, $\backslash phi$ can be built up as needed, remembering assigned mappings $\backslash langle\; s,t,\backslash phi(s,t)\; \backslash rangle$ in a hash table.

The algorithm consists of two rules:

:

For example, $(0*0)\; \backslash sqcup\; (4*4)\; \backslash rightsquigarrow\; (0\; \backslash sqcup\; 4)*(0\; \backslash sqcup\; 4)\; \backslash rightsquigarrow\; \backslash phi(0,4)\; *\; \backslash phi(0,4)\; \backslash rightsquigarrow\; x*x$; 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.

{{expand section|small=no|for=explain main results from papers below, relate their approaches to each other|date=June 2020}}

• {{citation|first1=Erik|last1=Jacobsen|title=Unification and Anti-Unification|series=Technical Report|date=Jun 1991|url=http://erikjacobsen.com/pdf/unification.pdf}}
• {{citation |first1=Bjarte M. |last1=Østvold |title=A Functional Reconstruction of Anti-Unification |publisher=Norwegian Computing Center |series=NR Note |volume=DART/04/04 |date=Apr 2004 |url=https://projects.nr.no/en/nrpublication?query=/file/nr-notat-dart-04-04.pdf}}
• {{cite conference | contribution-url=https://aaai.org/papers/flairs-2002-064 | first1=Svetla | last1=Boytcheva | first2= Zdravko |last2=Markov | contribution=An Algorithm for Inducing Least Generalization Under Relative Implication | editor= | title=Proc. FLAIRS-02 | publisher=AAAI | series= | volume= | pages=322–326 | year=2002 }}
• {{cite journal|first1=Temur|last1=Kutsia|first2=Jordi|last2=Levy|first3=Mateu|last3=Villaret|title=Anti-Unification for Unranked Terms and Hedges|journal=Journal of Automated Reasoning|volume=52|number=2|pages=155–190|url=https://link.springer.com/content/pdf/10.1007%2Fs10817-013-9285-6.pdf|year=2014|doi=10.1007/s10817-013-9285-6|doi-access=free}} [http://www.risc.jku.at/projects/stout/software/antiunify.php Software.]

• One associative and commutative operation: {{citation|first1=Loic|last1=Pottier|title=Algorithms des completion et generalisation en logic du premier ordre|date=Feb 1989|url=https://www.theses.fr/1989NICE4261|type=These de doctorat }}; {{citation|first1=Loic|last1=Pottier|title=Generalisation de termes en theorie equationelle – Cas associatif-commutatif|publisher=INRIA|series=INRIA Report|volume=1056|year=1989}}
• Commutative theories: {{cite conference|first1=Franz|last1=Baader|author-link=Franz Baader| title=Unification, Weak Unification, Upper Bound, Lower Bound, and Generalization Problems|book-title=Proc. 4th Conf. on Rewriting Techniques and Applications (RTA)|publisher=Springer|series=LNCS|volume=488|pages=86–91|year=1991|doi=10.1007/3-540-53904-2_88 |url=https://link.springer.com/chapter/10.1007/3-540-53904-2_88}}
• Free monoids: {{citation|first1=A.|last1=Biere|title=Normalisierung, Unifikation und Antiunifikation in Freien Monoiden|publisher=Univ. Karlsruhe, Germany|year=1993|url=http://fmv.jku.at/papers/Biere-Diploma-Thesis-1993.pdf}}
• Regular congruence classes: {{citation|first1=Birgit|last1=Heinz|title=Anti-Unifikation modulo Gleichungstheorie und deren Anwendung zur Lemmagenerierung|publisher=TU Berlin|series=GMD Berichte|volume=261|isbn=978-3-486-23873-0|date=Dec 1995}}; {{cite journal|first1=Jochen |last1=Burghardt |title=E-Generalization Using Grammars |journal=Artificial Intelligence |volume=165 |number=1 |pages=1–35 |arxiv=1403.8118 |year=2005 |doi=10.1016/j.artint.2005.01.008 |s2cid=5328240 }}
• A-, C-, AC-, ACU-theories with ordered sorts: {{cite journal|first1=Maria|last1=Alpuente|first2=Santiago|last2=Escobar|first3=Javier|last3=Espert|first4=Jose|last4=Meseguer|title=A modular order-sorted equational generalization algorithm|journal=Information and Computation|year=2014|doi=10.1016/j.ic.2014.01.006|volume=235|pages=98–136|hdl=2142/25871|doi-access=free|hdl-access=free}}
• Purely idempotent theories: {{cite journal|first1=David|last1=Cerna|first2=Temur|last2=Kutsia|title=Idempotent Anti-Unification|journal=ACM Transactions on Computational Logic|year=2020|url=https://dl.acm.org/doi/10.1145/3359060|volume=21|number=2|pages=1–32 |doi=10.1145/3359060 |hdl=10.1145/3359060|s2cid=207861304 }}

• Taxonomic sorts: {{cite journal|first1=Alan M.|last1=Frisch|first2=David|last2=Page|title=Generalisation with Taxonomic Information|journal=AAAI|pages=755–761|year=1990}}; {{cite conference|first1=Alan M.|last1=Frisch|first2=C. David|last2=Page Jr.|title=Generalizing Atoms in Constraint Logic|url=https://books.google.com/books?id=1wwZAQAAIAAJ&dq=%22Generalizing+Atoms+in+Constraint+Logic%22&pg=PA429|book-title=Proc. Conf. on Knowledge Representation|year=1991}}; {{cite conference|first1=A.M.|last1=Frisch|first2=C.D.|last2=Page|title=Building Theories into Instantiation|editor1-first=C.S.|editor1-last=Mellish|book-title=Proc. 14th IJCAI|publisher=Morgan Kaufmann|pages=1210–1216|year=1995|citeseerx=10.1.1.32.1610 }}
• Feature terms: {{cite conference|first1=E.|last1=Plaza|title=Cases as Terms: A Feature Term Approach to the Structured Representation of Cases|book-title=Proc. 1st International Conference on Case-Based Reasoning (ICCBR)|publisher=Springer|series=LNCS|volume=1010|issn=0302-9743|pages=265–276|year=1995}}
• {{cite conference|first1=Peter|last1=Idestam-Almquist|title=Generalization under Implication by Recursive Anti-Unification|url=https://books.google.com/books?id=TrqjBQAAQBAJ&dq=%22Generalization+under+Implication+by+Recursive+Anti-Unification%22&pg=PA151|book-title=Proc. 10th Conf. on Machine Learning|publisher=Morgan Kaufmann|pages=151–158|date=Jun 1993}}
• {{citation|first1=Cornelia|last1=Fischer|title=PAntUDE – An Anti-Unification Algorithm for Expressing Refined Generalizations|publisher=DFKI|series=Research Report|volume=TM-94-04|date=May 1994|url=https://publikationen.sulb.uni-saarland.de/bitstream/20.500.11880/25109/1/TM_94_04.pdf}}
• A-, C-, AC-, ACU-theories with ordered sorts: see above

• Baumgartner, Alexander; Kutsia, Temur; Levy, Jordi; Villaret, Mateu (Jun 2013). [http://drops.dagstuhl.de/opus/volltexte/2015/5189/pdf/9.pdf Nominal Anti-Unification]. Proc. RTA 2015. Vol. 36 of LIPIcs. Schloss Dagstuhl, 57-73. [http://www.risc.jku.at/projects/stout/software/nau.php Software.]

• Program analysis:
• {{cite journal|first1=Peter|last1=Bulychev|first2=Marius|last2=Minea|title=Duplicate Code Detection Using Anti-Unification|journal=Proceedings of the Spring/Summer Young Researchers' Colloquium on Software Engineering |url=https://cyberleninka.ru/article/n/14517244|year=2008|issue=2 }};
• {{cite conference | contribution-url=https://link.springer.com/chapter/10.1007/978-3-642-11486-1_35 | first1=Peter E.|last1=Bulychev|first2=Egor V.|last2=Kostylev|first3=Vladimir A.|last3=Zakharov | contribution=Anti-Unification Algorithms and their Applications in Program Analysis | editor=Amir Pnueli and Irina Virbitskaite and Andrei Voronkov | title=Perspectives of Systems Informatics (PSI) – 7th International Andrei Ershov Memorial Conference | publisher=Springer | series=LNCS | volume=5947 | pages=413–423 | year=2009 | doi=10.1007/978-3-642-11486-1_35| isbn=978-3-642-11485-4}}
• Code factoring:
• {{citation|first1=Rylan|last1=Cottrell|title=Semi-automating Small-Scale Source Code Reuse via Structural Correspondence|publisher=Univ. Calgary|date=Sep 2008|url=https://pages.cpsc.ucalgary.ca/~denzinge/papers/fse08.pdf}}
• Induction proving:
• {{citation|first1=Birgit|last1=Heinz|title=Lemma Discovery by Anti-Unification of Regular Sorts|publisher=TU Berlin|series=Technical Report|volume=94-21|year=1994}}
• Information Extraction:
• {{cite journal|first1=Bernd|last1=Thomas|title=Anti-Unification Based Learning of T-Wrappers for Information Extraction|url=https://www.aaai.org/Papers/Workshops/1999/WS-99-11/WS99-11-003.pdf|journal=AAAI Technical Report|volume=WS-99-11|pages=15–20|year=1999}}
• Case-based reasoning:
• {{cite conference | contribution-url=https://www.researchgate.net/publication/221045334 | last1=Armengol|first2=Enric|last2=Plaza | contribution=Using Symbolic Descriptions to Explain Similarity on {CBR} | editor=Beatriz López and Joaquim Meléndez and Petia Radeva and Jordi Vitrià | title=Artificial Intelligence Research and Development, Proc. 8th Int. Conf. of the ACIA, CCIA | publisher=IOS Press | series= | volume= | pages=239–246 | year=2005 }}
• 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.
• {{cite report | url=http://www.sri.com/sites/default/files/uploads/publications/pdf/725.pdf | author1=Zohar Manna | author2=Richard Waldinger | author1-link=Zohar Manna | author2-link=Richard Waldinger | title=A Deductive Approach to Program Synthesis | institution=SRI International | type=Technical Note | number=177 | date=Dec 1978 | access-date=2017-09-29 | archive-date=2017-02-27 | archive-url=https://web.archive.org/web/20170227140017/http://www.sri.com/sites/default/files/uploads/publications/pdf/725.pdf | url-status=dead }} — preprint of the 1980 article
• {{cite journal | author=Zohar Manna and Richard Waldinger | title=A Deductive Approach to Program Synthesis | journal=ACM Transactions on Programming Languages and Systems | volume=2 | pages=90–121 | date=Jan 1980 | doi=10.1145/357084.357090 | s2cid=14770735 }}
• Natural language processing:
• {{cite journal|first1=Nino|last1=Amiridze|first2=Temur|last2=Kutsia|title=Anti-Unification and Natural Language Processing|journal=Fifth Workshop on Natural Language and Computer Science, NLCS'18|series=EasyChair Preprints |volume=EasyChair Report No. 203|year=2018|doi=10.29007/fkrh |s2cid=49322739 |doi-access=free}}

{{expand section|for=(as above)|date=June 2020}}

• Calculus of constructions:
• {{cite conference|first1=Frank|last1=Pfenning| author-link=Frank Pfenning| title=Unification and Anti-Unification in the Calculus of Constructions|book-title=Proc. 6th LICS|publisher=Springer|url=https://www.cs.cmu.edu/~fp/papers/lics91.pdf|pages=74–85|date=Jul 1991}}
• Simply typed lambda calculus (Input: Terms in the eta-long beta-normal form. Output: higher-order patterns):
• Baumgartner, Alexander; Kutsia, Temur; Levy, Jordi; Villaret, Mateu (Jun 2013). [http://drops.dagstuhl.de/opus/volltexte/2013/4057/pdf/10.pdf A Variant of Higher-Order Anti-Unification]. Proc. RTA 2013. Vol. 21 of LIPIcs. Schloss Dagstuhl, 113-127. [http://www.risc.jku.at/projects/stout/software/hoau.php Software.]
• Simply typed lambda calculus (Input: Terms in the eta-long beta-normal form. Output: Various fragments of the simply typed lambda calculus including patterns):
• {{cite conference|first1=David|last1=Cerna| first2=Temur|last2=Kutsia| title=A Generic Framework for Higher-Order Generalizations|book-title=4th International Conference on Formal Structures for Computation and Deduction, FSCD, June 24–30, 2019, Dortmund, Germany|publisher=Schloss Dagstuhl - Leibniz-Zentrum für Informatik| url=https://drops.dagstuhl.de/opus/volltexte/2019/10517/pdf/LIPIcs-FSCD-2019-10.pdf|pages=74–85|date=June 2019}}
• Restricted Higher-Order Substitutions:
• {{citation|first1=Ulrich|last1=Wagner|title=Combinatorically Restricted Higher Order Anti-Unification|publisher=TU Berlin|date=Apr 2002}}; {{citation|first1=Martin|last1=Schmidt|title=Restricted Higher-Order Anti-Unification for Heuristic-Driven Theory Projection|publisher=Univ. Osnabrück, Germany|series=PICS-Report|volume=31-2010|issn=1610-5389|date=Sep 2010|url=http://ikw.uni-osnabrueck.de/de/system/files/31-2010.pdf}}

{{reflist|group=note}}

{{Reflist}}

Category:Inductive logic programming

Category:Automated theorem proving

Category:Logic in computer science

Category:Unification (computer science)