At first glance Tom's canonical algebra seems as though it should be closely related to what came out of the last 26 messages of http://www.seas.upenn.edu/~sweirich/types/archive/1988/ starting with John Mitchell's question of 9 Nov 88, message 155, as to whether initiality was the right criterion for correctness of an implementation of an algebraic data type. Satish Thatte in message 174 suggested Mitch Wand's "Final Algebra Semantics" from JCSS 1979 as more appropriate, in particular Wand's main theorem that every standard conservative extension has a maximal base-conservative augment, or as I put it in 176 (= 177), "Every biconservative extension of an equational theory has a greatest base-conservative augment." I then conjectured that it could be extended to "Every extension of an equational theory has an optimal base-conservative augment", and commented that "There is only thing bothering me about all this. It seems too nice, elementary, and useful to be not already known to logicians. Anyone seen anything like this outside Wand's paper?". In message 178 Satish Thatte pointed out that my optimal augment did indeed always exist, namely as the intersection of all maximal base-conservative augments. In the final paragraph of the final message (180) in that series, with subject "final algebras", I wrote "In any event I don't see how category theory is helping here, indeed this would seem to be an instance where category theory hinders more than it helps." If Tom's construction is equivalent then I sure got that wrong. If the algebras are different it would be nice to understand what the differences and relative merits of the two are - seems to me they ought at least to be related. I wish my memory went back that far. Vaughan Tom Leinster wrote:
Dear all,
Here is a canonical, but perhaps not trivial, way of constructing an algebra for any finitary algebraic theory. Does anyone know anything about it? E.g. is there existing work on it, or an alternative description?
Take a finitary monad (T, eta, mu) on Set. We construct an algebra A for the monad in three steps:
(i) Let C be the terminal coalgebra for the endofunctor T (which exists since T is finitary).
(ii) Regard C as an algebra for the endofunctor T (via Lambek's Lemma: the structure map of C is invertible).
(iii) Turn C into an algebra A for the monad (T, eta, mu) by applying the left adjoint to the inclusion
(T, eta, mu)-Alg ----> T-Alg.
Here are two examples.
1. Fix a monoid M and let (T, eta, mu) be the theory of left M-sets. Then C is the set of infinite sequences (m_1, m_2, ...) of elements of M, and A = C/~ where ~ is generated by
(m_1, m_2, ...) ~ (m_1 ... m_n, m_{n+1}, m_{n+2}, ...)
for any natural number n and m_i in M.
2. Let (T, eta, mu) be the theory of monoids. Then C is the set of infinite planar trees in which each vertex may have any natural number of branches ascending from it (or descending, according to convention). Next, A = C/~ where ~ is generated by
s o (t_1, ..., t_n) ~ s' o (t_1, ..., t_n)
for any finite n-leafed trees s, s' and t_1, ..., t_n in C. Here "o" means "grafting": the left-hand side is the union of s and the (t_i)s, with the root of t_i glued to the i-th leaf of s.
Hence A is the set of equivalence classes of infinite trees, where two trees are equivalent if one can be obtained from the other by altering just a finite portion at its base.
This equivalence relation (or actually, the analogous one for commutative monoids) is what made me start thinking about all this.
Thanks, Tom