A canonical algebra

A canonical algebra

[Tom Leinster]

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

-- 
Tom Leinster <tl@maths.gla.ac.uk>

Re: A canonical algebra

[Vaughan Pratt]

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
>