# What is the difference between unification and anti-unification?

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?

The following category theory inspired analysis (adapted from Plotkin's A Note on Inductive Generalization) 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 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 in the category $\mathcal{C}$ defined above.

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

• Isn't the unifier the coproduct and the anti-unifier the product ?
– yago
Mar 17 '16 at 12:02
• @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 ;-) Mar 17 '16 at 15:05
• Happens to me everytime :) nice answer anyway !
– yago
Mar 18 '16 at 18:59