Mgu’s and universal properties

Warning, poorly-explained categorical rambling follows…

The most general unifier (mgu) of two expressions x and y is a substitution \theta for which \theta(x) = \theta(y), such that every other substitution \phi for which \phi(x) = \phi(y) can be expressed as \theta \circ \phi' for some \phi'. For example, the most general unifier of f(x,g(2)) and f(g(3), y) is [x := g(3), y := g(2)].

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 x and y is a natural number d which evenly divides both x and y, such that every other common divisor of x and y is also a divisor of d.

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?

About Brent

Assistant Professor of Computer Science at Hendrix College. Functional programmer, mathematician, teacher, pianist, follower of Jesus.
This entry was posted in math and tagged , , , . Bookmark the permalink.

9 Responses to Mgu’s and universal properties

  1. Miguel says:

    you can check “What is Unification? – A Categorical View of Substitution, Equation and Solution” by Joseph Goguen.


    • Brent says:

      Fantastic, thanks! Sounds like exactly what I’m looking for.

      • Derek Elkins says:

        I was also going to suggest that paper (and also Goguen’s “Categorical Manifesto”). The construction you found is probably the same as the one in “What is Unification?” but in the opposite category. As the “Categorical Manifesto” suggests, usually “solving equations” type of things are limits (also meets/products are limits as well.)

        • Brent says:

          Ah, OK, yes, I was surprised that what seemed most natural to me was a colimit instead of a limit. Thanks for the additional pointer to the Categorical Manifesto.

  2. Marek says:

    I have probably a stupid question. Does this categorical language got any application in real world (by this I mean real math world which includes geometry, analysis, algebra, etc.)? I mean, I’ve seen that you can express more or less any concept via category theory, but does it give you some new nontrivial results? Or is just for the sake of doing everything as general as you can no matter the real value of it (I guess that’s why people call it “abstract generalized nonsense”?). I am not trying to offend anyone, just trying to asses the categories’ worth. I like the abstract concepts myself (loving group theory, etc.), but as of yet haven’t seen any real application.


    • Brent says:

      Hi Marek,

      It’s a perfectly valid question! My take on it is that category theory, much like group theory or any other mathematical theory that abstracts out some sort of common patterns, doesn’t really have any “applications” per se. Its value lies in its power to talk about the essence of various patterns without extraneous details getting in the way, and the ability to then apply the things learned and intuition gained back to specific problems. As soon as I recognize that something is really just a particular instance of (say) and adjunction, I can immediately apply everything I know about adjunctions to gain specific insight into the given problem. It is also useful in connecting different areas of mathematics and computer science—if I realize that two *different* things are *both* instances of an adjunction, then it may give me the insight I need to see a previously unguessed connection and fundamental unity between the two apparently different areas.

      • Marek says:

        I agree that it’s certainly useful to notice that object A is object B in disguise and then just apply object A theory to study object B. I guess, what I am asking is: does category theory provide any theory for some object per se, or is it just analogies it shows us?

        As for the real mathematics: take the group theory. It is pretty abstract, but still, using representation theory of groups you can derive pretty much everything important about physics, given that you know what groups to start with (I am a physicist by the way), so that’s quite a huge application. I wondered whether category theory also provides something like that. I guess in computation one can get more results, seeing as monads are categorical theory concept, etc. I’d love to hear more about these things in your blog!

  3. Pozorvlak says:

    Marek: plenty of people are applying category theory to real-world problems. Check out the work of eg John Baez for applications to physics. Much of modern algebraic geometry (after Grothendieck) would be literally unthinkable without it. And, of course, it has extensive applications in logic and type theory.

    • Marek says:

      Thx for the suggestion. I had already tried to approach category theory in the past, but my problem was all the things I’d read were either too popular and I learned nothing really interesting, or they were too hard for me to follow. Fortunately, recently I found what I think is a great book by Lawvere and Schanuel that explains all the basic math (sets, arithmetic, geometry, etc.) with categorical language, with plenty of examples, but still everything is rigorous and mathematical. I think like I am finally getting little grasp of category theory’s basics and it’s fascinating beyond anything I expected. I mean, all of the mathematical disciplines and concepts are just one category theory with objects and maps. That’s pretty amazing :-) As for algebraic geometry, I recently stumbled upon that too. Toposes and sheaves seem great, but little too hard for someone not very familiar with category theory. Maybe sometime later I’ll try to study them a bit more.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.