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?
Asked By : bellpeace
Answered By : bellpeace
I found out that such a thing is called anti-unification. This problem was addressed by Plotkin and Reynolds. Here is a brief overview.
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/22910
0 comments:
Post a Comment
Let us know your responses and feedback