Warning, poorly-explained categorical rambling follows…
The most general unifier (mgu) of two expressions and is a substitution for which , such that every other substitution for which can be expressed as for some . For example, the most general unifier of and is .
Now, I’d seen this definition before. But just yesterday I realized what a similar flavor it has to certain other definitions in mathematics. For example:
The greatest common divisor of two natural numbers and is a natural number which evenly divides both and , such that every other common divisor of and is also a divisor of .
See the similarity? Now, I’ve studied enough category theory to know that this is an example of a “universal property”. gcd in particular is the meet operation in the divisor poset, and meets are just products in a poset category… so, naturally, I wondered whether mgu’s could also be formalized as a particular universal construction in some category. After some fiddling around, I figured out that yes, mgu’s can be thought of as coequalizers in a category of substitutions (which I guess is sort of like the Kleisli category of the free monad on the structure functor for whatever term algebra you are using?). A Google search for “mgu coequalizer” seems to suggest that I am right! I’m rather pleased that I came up with this on my own. Anyone know of a link to where this was first discussed?