A functional reconstruction of anti-unification

In 1970 both Plotkin and Reynolds defined the anti-unification of a set of literal clauses, that is, atomic formulas or negated atomic formulas. They gave similar imperative anti-unification algorithms and proved the algorithms correct.

We formulate an alternative anti-unification algorithm using recursive equations and prove its correctness. This functional-style algorithm gives a modular view of anti-unification, where each equation captures a different computational aspect. Modularity makes the algorithm well-suited as a starting point for designing related algorithms. It can easily be converted into a program in a functional programming language.