Back from a short holidays in the White Mountains (NH), snoeshowing and cross-country skying. We stayed at a delightful little bed and breakfast near Gorham, the Mt Washington Bed and Breakfast. I highly recommend it. (Tell Mary Ann that Riccardo sent you.)
I hold a logic discussion group, and this semester we are slowly working our way to Plotkin and Power's work on equational characterizations of effects, an alternative to Moggi's monadic approach based on Power's Freyd categories. Perhaps I will get to talk about this later.
Anyways, we started last month by looking at Lawvere theories, Lawvere's 1960s approach to universal algebra via category theory. The idea is pretty simple. An algebraic structure can be defined by a underlying set A along with a set of equations over the elements of the set. This can be represented rather simply using a category who objects are products of A, that is, A^0, A^1, A^2, ..., and where arrows between elements are operations, including all projections. We can encode the equations by stating that some diagrams commute.
Let's look at a simple example, groups. A group is traditionally described as a tuple (G,*,-,e), where G is a set (the elements of the group), * is a binary operation G x G -> G, - is a unary operation G -> G, and e is a constant (or nullary operation) which we can represent as 1 -> G, where 1 is any one-element set, subject to the following equations:
- x * (y * z) = (x * y) * z
- x * e = x = e * x
- x * (-x) = e = (-x) * x
The Lawvere theory for groups, call it LG, is basically the category with object a^0=1,a^1,a^2,... (for some unspecified object a), and taking arrows to include all projections, and three arrows * : a^2 -> a, - : a -> a, and e : 1 -> a, subject to the following diagrams commuting: (it's a pain to draw diagrams in confluence, so I shan't do it...)
- * o < * , id_a > = * o < id_a , * >
- * o < e , id_a > = * o < id_a , e >
- * o < id_a , - > = e o 1
- * o < - , id_a > = e o 1
(where id_a : a -> a is the identity arrow, o is arrow composition, and <f,g> is the usual product of arrows).
An actual group (i.e., a model for the theory) can be taken to be a functor from the category LG to the category of sets. This functor will map the basic object a of LG to some set G (representing the elements of the group) and the functor properties will ensure that the elements of the set will satisfy the group equations. (Try it!) In other words, a group is a functor LG -> Set.
A good introduction to this is Steve Awodey lecture notes on categorical logic, specifically section 2.1 here:
- S. Awodey, A. Bauer, Lecture Notes: Introduction to Categorical Logic
Now, one question I had at some point is how does this handle algebraic structures defined by implications (that is, Horn clauses). Think of these as conditional equalities. The main example of this that I encounter is Kleene algebras, axiomatized as follows, using Kozen's axiomatization. Recall that a Kleene algebra is an algebra with signature ( K , . , + , 0 , 1 , * ), where ( K , . , + , 0 , 1 ) is an idempotent semiring, and * is a unary operation subject to the following:
- 1 + x.(x*) <= x*
- a + (x*).x <= x*
- if a.x <= x, then (a*).x <= x
- if x.a <= x, then x.(a*) <= x
(Here, x <= y is defined to be x + y = y, which is a partial order when you have an idempotent semiring.) Note that these equations are conditional, that is, the last two equations are really implications. How do you model this using the framework of Lawvere?
The set of models for an equational theory that uses conditional equations form a quasivariety. (In contrast, the set of models for an equational theory that uses only unconditional equations form a variety; quasivarieties, as the name implies, are almost varieties, but not quite.) The following paper, that appeared in Journal of Algebra 208 (1998), 379-398, seems to hint at the appropriate Lawvere development for quasivarieties, although it is quite technical:
- J. Adamek, H.-E. Porst, Algebraic Theories of Quasivarieties
What I am still not sure of, though, is how to concretely give a description of a theory, given a specific equational theory. In particular, given the axiomatization of Kleene algebras given above, can we concretely describe the category LK in the Adamek-Porst framework that plays the role of Lawvere theory, and for which the functors LK -> Set are exactly the Kleene algebras?