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.

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

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