7
$\begingroup$

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?

$\endgroup$
11
$\begingroup$

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

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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