<p>The following category theory inspired analysis (adapted from Plotkin's <a href="http://homepages.inf.ed.ac.uk/gdp/publications/MI5_note_ind_gen.pdf">A Note on Inductive Generalization</a>) explains a sense in which unification and anti-unification are dual concepts. As notation, let's write
$$t \underset{\sigma}{\Longrightarrow} u$$
for two terms $t$ and $u$ and a substitution $\sigma$ whenever $t\sigma = u$.  The existence of such a subsitution $\sigma$ implies that $t$ is a <em>generalization</em> of $u$, and that $u$ is a <em>specialization</em> of $t$.</p>

<p>Suppose given two terms $t_1,t_2$.  A <strong>unifier</strong> of $t_1$ and $t_2$ is a term $u$ together with a pair of substitutions $\sigma_1$ and $\sigma_2$ such that
$$
t_1 \underset{\sigma_1}{\Longrightarrow} u \underset{\sigma_2}{\Longleftarrow} t_2
$$
It is a <strong>most general</strong> unifier if it is a generalization of any other unifier, that is, if for any other unifier
$$
t_1 \underset{\sigma_1'}{\Longrightarrow} u' \underset{\sigma_2'}{\Longleftarrow} t_2
$$
there is some $\sigma'$ such that
$$
u \underset{\sigma'}{\Longrightarrow} u'
$$
In other words, a most general unifier is precisely a <a href="https://en.wikipedia.org/wiki/Coproduct">coproduct</a> in the category $\mathcal{C}$ whose objects are terms and where there is a morphism $t \to u$ just in case $t \underset{\sigma}{\Longrightarrow} u$ for some $\sigma$.</p>

<p>To define anti-unification we just reverse all the arrows!  Which is to say that...</p>

<p>An <strong>anti-unifier</strong> of $t_1$ and $t_2$ is a term $u$ together with a pair of substitutions $\sigma_1$ and $\sigma_2$ such that
$$
t_1 \underset{\sigma_1}{\Longleftarrow} u \underset{\sigma_2}{\Longrightarrow} t_2
$$
It is a <strong>least general</strong> anti-unifier if it is a specialization of any other anti-unifier, that is, if for any other anti-unifier
$$
t_1 \underset{\sigma_1'}{\Longleftarrow} u' \underset{\sigma_2'}{\Longrightarrow} t_2
$$
there is some $\sigma'$ such that
$$
u' \underset{\sigma'}{\Longrightarrow} u
$$
This means that a least general anti-unifier is precisely a <a href="https://en.wikipedia.org/wiki/Product_(category_theory)">product</a> in the category $\mathcal{C}$ defined above.</p>

<hr>

<p><strong>Update:</strong> fixed the accidentally dualized terminology in the original description (thanks Yann Hamdaoui!).</p>

CC BY-SA 3.0
2016-03-17T12:02:39.150Z
Isn't the unifier the coproduct and the anti-unifier the product ?
yago
CC BY-SA 3.0
2016-03-17T15:05:37.157Z
@YannHamdaoui Whoops! Of course you're right, I guess I got caught up in the excitement of reversing arrows and reversed them one too many times ;-)
Noam Zeilberger
CC BY-SA 3.0
2016-03-18T18:59:37.697Z
Happens to me everytime :) nice answer anyway !
yago
CC BY-SA 3.0
2016-03-16T23:33:19.983Z
2016-03-17T15:12:50.497Z
2016-03-17T15:12:50.497Z
Noam Zeilberger
<p>I understand that in Unification we try to find a general solution to an equation between two terms, but what is anti-unification, and how is it different?</p>

<lo.logic>
What is the difference between unification and anti-unification?
S. Nabil
# What is the difference between unification and anti-unification?

(Asked by: username_0 on 2016-03-16)

I understand that in Unification we try to find a general solution to an equation between two terms, but what is anti-unification, and how is it different?

**Tags:** lo.logic

---

## 1 answers

### Answer by username_1 on 2016-03-16. Score: 13

The following category theory inspired analysis (adapted from Plotkin's [A Note on Inductive Generalization](http://homepages.inf.ed.ac.uk/gdp/publications/MI5_note_ind_gen.pdf)) explains a sense in which unification and anti-unification are dual concepts. As notation, let's write
$$t \underset{\sigma}{\Longrightarrow} u$$
for two terms $t$ and $u$ and a substitution $\sigma$ whenever $t\sigma = u$. The existence of such a subsitution $\sigma$ implies that $t$ is a *generalization* of $u$, and that $u$ is a *specialization* of $t$.

Suppose given two terms $t\_1,t\_2$. A **unifier** of $t\_1$ and $t\_2$ is a term $u$ together with a pair of substitutions $\sigma\_1$ and $\sigma\_2$ such that
$$
t\_1 \underset{\sigma\_1}{\Longrightarrow} u \underset{\sigma\_2}{\Longleftarrow} t\_2
$$
It is a **most general** unifier if it is a generalization of any other unifier, that is, if for any other unifier
$$
t\_1 \underset{\sigma\_1'}{\Longrightarrow} u' \underset{\sigma\_2'}{\Longleftarrow} t\_2
$$
there is some $\sigma'$ such that
$$
u \underset{\sigma'}{\Longrightarrow} u'
$$
In other words, a most general unifier is precisely a [coproduct](https://en.wikipedia.org/wiki/Coproduct) in the category $\mathcal{C}$ whose objects are terms and where there is a morphism $t \to u$ just in case $t \underset{\sigma}{\Longrightarrow} u$ for some $\sigma$.

To define anti-unification we just reverse all the arrows! Which is to say that...

An **anti-unifier** of $t\_1$ and $t\_2$ is a term $u$ together with a pair of substitutions $\sigma\_1$ and $\sigma\_2$ such that
$$
t\_1 \underset{\sigma\_1}{\Longleftarrow} u \underset{\sigma\_2}{\Longrightarrow} t\_2
$$
It is a **least general** anti-unifier if it is a specialization of any other anti-unifier, that is, if for any other anti-unifier
$$
t\_1 \underset{\sigma\_1'}{\Longleftarrow} u' \underset{\sigma\_2'}{\Longrightarrow} t\_2
$$
there is some $\sigma'$ such that
$$
u' \underset{\sigma'}{\Longrightarrow} u
$$
This means that a least general anti-unifier is precisely a [product](https://en.wikipedia.org/wiki/Product_(category_theory)) in the category $\mathcal{C}$ defined above.

---

**Update:** fixed the accidentally dualized terminology in the original description (thanks Yann Hamdaoui!).

> **Comments:**
> **username_2**: Isn't the unifier the coproduct and the anti-unifier the product ?  
> **username_1**: @YannHamdaoui Whoops! Of course you're right, I guess I got caught up in the excitement of reversing arrows and reversed them one too many times ;-)  
> **username_2**: Happens to me everytime :) nice answer anyway !  

---

