Re: Decidability of the theory of a monad

[Andrej Bauer <andrej.bauer@andrej.com>]

I thank eveyone who answered my question so quickly. For reference I
post a summary of the answers.

Bill Lawvere answered that "the theory of a monad is just that of
ordinal addition of 1 on the augmented simplicial category Delta
considered as a (non-commutative) monoidal category wrt ordinal
addition." A relevant reference in this regard is his "Ordinal Sums
and Equational Doctrines" which was part of the Zurich Triples Book,
available online as TAC Reprints 18.

Similarly, Jaap van Oosten pointed out that the free "monad on a
category" on one generator is the simplicial category \Delta (nonempty
finite ordinals and monotone functions).

It follows from these observations that the theory of a monad is decidable.

Todd Wilson kindly pointed me to a thesis by Wolfgang Gehrke, see
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.47.7087 ,
which contains a complete set of rewrite rules (page 40, Proposition
20) for the theory of a monad:

id f ==> f
f id ==> f
(f g) h ==> f (g h)
eta* ==> id
f* eta ==> f
f* g* ==> (f* g)*
f* (eta g) ==> f g
f* (g* h) ==> (f* g)* h

The last two rules are extra, compared to the original equations. So
the next time you wonder whether an equation holds of a general monad,
just use the above rewrite rules on both sides of the equation.

With kind regards,

Andrej


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]