4
$\begingroup$

In unification, given a set of equations, a standard problem is to compute a most general unifier (mgu). I am interested in a somewhat reversed problem. Imagine having a set of equations that do not have an mgu, like this one:

x = a
x = b

x here is a variable, whereas a and b are terms. I am interested are there any algorithms that could find a possible replacement for a and b such that the resulting equations have mgu? In the above example, that would be a -> y, b -> y, y being a variable. Lets call this a fix. I am particularly interested in most specific fixes. I could not find anything so far, but this seems like a natural problem, or not?

$\endgroup$
4
$\begingroup$

I found out that such a thing is called anti-unification. This problem was addressed by Plotkin and Reynolds. Here is a brief overview.

$\endgroup$
3
$\begingroup$

In rewrite theory, you often want confluence of your system: if $$ u_1\leftarrow t\rightarrow u_2$$

Then there is some term $v$ such that $$ u_1\rightarrow v\leftarrow u_2$$

It is possible to tell whether a set of rewrite rules is confluent by examining the critical pairs: pairs of rules $t_1\rightarrow u_1,t_2\rightarrow u_2$ and an instance $\theta$ such that

  1. $t'_1\theta = t_2\theta$
  2. $t'_1$ is a subterm of $t_1$ at position $p$.

You can then add the equation $u_1\theta = t_1[u_2\theta]_p$ to make the system confluent.

This suggest an approach to your problem: look at your equations as rewrite rules, then consider the critical pairs: they tell you which equations need to hold to make your system unifiable.

$\endgroup$

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.