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.