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?


1 Answer 1


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!).

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.