HiveBrain v1.2.0
Get Started
← Back to all entries
patternMinor

Unification --- most specific unifier

Submitted by: @import:stackexchange-cs··
0
Viewed 0 times
unifiermostunificationspecific

Problem

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?

Solution

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

Context

StackExchange Computer Science Q#22910, answer score: 4

Revisions (0)

No revisions yet.