# 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. 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. 🙂

2. 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.