# Anti-unification, part 3

Last time we described the classic first-order anti-unification algorithm, and reduced it from three rules to only two. Let’s work an example, the same example that we gave a while back.

```s is cons(cons(1, 2), cons(cons(1, 2), nil))
t is cons(3, cons(3, nil))
```

So our initial condition is:

```g = h0
ss = { cons(cons(1, 2), cons(cons(1, 2), nil)) / h0 }
st = { cons(3, cons(3, nil) / h0 }
```

Now we notice that rule 1 can be applied; there are two `cons` expressions both substituted for `h0`, so we move the `cons` into `g` and make the substitutions on the arguments to `cons`:

```g = cons(h1, h2)
ss = { cons(1,2) / h1,  cons(cons(1, 2), nil) / h2 }
st = { 3 / h1, cons(3, nil) / h2 }
```

Super. Now we notice that rule 1 applies again: we have `cons` expressions both substituted for `h2`, so we move the `cons` into `g`:

```g = cons(h1, cons(h3, h4))
ss = { cons(1, 2) / h1, cons(1, 2) / h3, nil / h4 }
st = { 3 / h1, 3 / h3, nil / h4 }
```

We are now in a situation where both rules apply.

Rule 1 applies because we can think of `nil` as being `nil()` — that is, a call that has exactly zero children. Thus there are two `nil` expressions both substituted for `h4`, so we can move the `nil` into `g`, and introduce zero new holes for the zero arguments.

Rule 2 applies because `h1` and `h3` are redundant.

One of the nice things about this algorithm is that it doesn’t matter what order you apply the rules in; you always make progress towards the eventual goal. Let’s apply rule 1:

```g = cons(h1, cons(h3, nil))
ss = { cons(1, 2) / h1, cons(1, 2) / h3 }
st = { 3 / h1, 3 / h3 }
```

Rule 1 no longer applies, but rule 2 does. `h1` and `h3` are still redundant. Get rid of `h1`:

```g = cons(h3, cons(h3, nil))
ss = { cons(1, 2) / h3 }
st = { 3 / h3 }
```

No more rules apply, and we’re done; we’ve successfully deduced that the most specific generalization of `s` and `t` is `cons(h3, cons(h3, nil))` and given substitutions that produce `s` and `t`.

Next time on FAIC: Let’s implement it! And maybe we’ll take a look at a few new features of C# 7 while we’re at it.