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 = h0ss = { 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.