Anti-unification, part 2

Last time on FAIC we learned what the first-order anti-unification problem is: given two expressions, s and t, either in the form of operators, or method calls, or syntax trees, doesn’t matter, find the most specific generalizing expression g, and substitutions for its holes that gives back s and t. Today I’ll sketch the algorithm for that in terms of function calls, and next time we’ll implement it on syntax trees.

There are papers describing the first-order anti-unification algorithm that go back to the 1970s, and they are surprisingly difficult to follow considering what a simple, straightforward algorithm it is. Rather than go through those papers in detail, rather here’s a sketch of the algorithm:

Basically the idea of the algorithm is that we start with the most general possible anti-unification, and then we gradually refine it by repeatedly applying rules that make it more specific and less redundant. When we can no longer improve things, we’re done.

So, our initial state is:

g = h0
ss = { s / h0 }
st = { t / h0 }

That is, our generalization is just a hole, and the substitutions which turn it back into s and t are just substituting each of those for the hole.

We now apply three rules that transform this state; we keep on applying rules until no more rules apply:

Rule 1: If ss contains f(s1, ... sn)/h0 and st contains f(t1, ... tn)/h0 then h0 is not specific enough.

  • Remove the substitution from ss and add substitutions s1/h1, ...sn/hn.
  • Remove the substitution from st and add t1/h1, ... tn/hn
  • Replace all the h0 in g with f(h1, ... hn)

Rule 2: If ss contains foo/h0 and foo/h1, and st has bar/h0 and bar/h1, then h0 and h1 are redundant. (For arbitrary expressions foo and bar.)

  • Remove foo/h0 and bar/h0 from their substitution sets.
  • Replace h0 in g with h1.

Rule 3: If ss and st both contain foo/h0 then h0 is unnecessary.

  • Remove the substitution from both sets.
  • Replace all h0 in g with foo.

These rules are pretty straightforward, but if we squint a little, we can simplify these even more! Rule 3 is just an optimization of repeated applications of rule 1, provided that we consider an expression like “nil” to be equivalent to “nil()”. This should make sense; a value is logically the same as a function call that takes no arguments and always returns that value. So in practice, we can eliminate rule three and just apply rules one and two.

That’s it! Increase specificity and remove redundancy; keep doing that until you cannot do it any more, and you’re done. Easy peasy. The fact that this algorithm converges on the best possible solution, and the fact that you can apply the rules in any order and still get the right result, are facts that I’m not going to prove in this space.

Next time on FAIC: We’ll work an example out by hand, just to make sure that it’s all clear.

3 thoughts on “Anti-unification, part 2

  1. Pingback: Dew Drop - November 1, 2018 (#2836) - Morning Dew

  2. Can I infer that in the case that s and t are unique, the initial state will be the final state where g remains the hole, and in the case that s and t are identical, there will be no hole to fill, in that g = s = t?

    I’m certain I’ll be needing that example in the next post to wrap my head around all of this. 🙂

  3. A pair of complex symbolic structures when subject to anti-unification produce what may be considered as a common framework in which the two original structures may be fit a specializations. This serve as a basis for lining up the structures so that they can be brought together side-by-side to produce a hybridization of the two. This is the essence of the art of Mash-Ups! Here is an excellent example of this process at work: RoboCop versus Terminator (Part 1) https://www.youtube.com/watch?v=Az8cOVAEwmM&feature=emb_logo

    Now the challenge for you is: devise a way to automate the process of hybridizing disparate elements into seamless mash-ups’ using anti-unification as the core. This can be applied more generally to any situation where you have two or more complex expressions that you want to seamlessly synthesize into a unified whole. For example, in the political world, it is a way to bring together two or more competing interest into a synthesis that may oftentimes go beyond what either contribution by itself could have achieved; by virtue of including a “corner” case that is enabled by having both components together in the same synthesis.

    It is one (of possibly several) pillars that provide nothing less than a basis for the automation of creativity itself.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s