Decidability of the theory of a monad
Consider the theory of a monad, i.e., the axioms are those of a category and a monad given as a triple: an operation T on objects, for each object A a morphism eta_A : A -> T A, and an operation lift_{A,B} which maps morphisms f : A -> T B to lift f : T A -> T B. Concretely, the axioms are (where lift f is written f* and composition is juxtaposition): id f = f f id = f (f g) h = f (g h) eta* = id f* eta = f (f* g)* = f* g* Presumably, the equational theory (with partial operations) of such a triple is decidable. Is this known? If we ignore the types and partiality, we can attempt to turn the above equations into a confluent terminating rewrite system using the Knuth-Bendix algorithm, but it gets stuck (on various orderings I tried). A more categorical way of asking the same question is: what is a concrete description of the free "monad on a category" (is this the same as "free monad" on "free category"?). With kind regards, Andrej [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
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/ ]
Dear Andrej, The free monad on a category has a well-known simple concrete description. Let Ordf be the category of finite ordinals and order-preserving maps. --> 0 --> 1 <-- 2 ... --> (This is sometimes called the algebraicist's simplicial category - it contains the topologist's simplicial category as the full subcategory of non-empty finite ordinals. Ordf is simply called Delta in Categories for the Working Mathematician.) Ordinal sum makes Ordf into a strict monoidal category. The object 1 is a monoid in this monoidal category, and in fact is the "free monoid in a monoidal category", in the sense that for any strict monoidal category C, there is a bijection between monoids in C and strict monoidal functors from Ordf to C. (There is also a non-strict version of this fact.) The free "category with a monad" on a category A is the Ordf x A, with monad having endofunctor part (n,a) |-> (n+1,a), with the obvious multiplication. More generally, the monoidal category Ordf can be regarded as a one-object 2-category mnd, and 2-functors mnd-->K for a 2-category K, are in bijection with monads in K. Freely adding a monad to an object of K can be seen as left Kan extension along the unique 2-functor 1-->mnd. Regards, Steve Lack. On 3/06/09 9:10 PM, "Andrej Bauer" <andrej.bauer@andrej.com> wrote:
Consider the theory of a monad, i.e., the axioms are those of a category and a monad given as a triple: an operation T on objects, for each object A a morphism eta_A : A -> T A, and an operation lift_{A,B} which maps morphisms f : A -> T B to lift f : T A -> T B. Concretely, the axioms are (where lift f is written f* and composition is juxtaposition):
id f = f f id = f (f g) h = f (g h) eta* = id f* eta = f (f* g)* = f* g*
Presumably, the equational theory (with partial operations) of such a triple is decidable. Is this known? If we ignore the types and partiality, we can attempt to turn the above equations into a confluent terminating rewrite system using the Knuth-Bendix algorithm, but it gets stuck (on various orderings I tried).
A more categorical way of asking the same question is: what is a concrete description of the free "monad on a category" (is this the same as "free monad" on "free category"?).
With kind regards,
Andrej
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Hi! not touching the partiality issue the answer to the question about decidability is positive. Decidability follows from the results, proved in our paper "Kleene Monads: Handling Iteration in a Framework of Generic Effects", accepted for the upcoming CALCO conference. The paper should be soon available on my homepage: http://www.informatik.uni-bremen.de/~sergey/papers_e.htm It does contain a confluent and strongly normalising rewrite system but the proof details will show up (hopefully) only in the journal version. The proofs are also included into my PhD thesis, which is under development and thus still unpublished but in case of interest I can make available some parts of it containing the proofs under discussion. Best regards, -------------------------------------- Sergey Goncharov Junior Researcher DFKI Bremen Safe and Secure Cognitive Systems Cartesium, Enrique-Schmidt-Str. 5 D-28359 Bremen phone: +49-421-218-64276 Fax: +49-421-218-9864276 mail: Sergey.Goncharov@dfki.de www.dfki.de/sks/staff/sergey -------------------------------------- ------------------------------------------------------------- Deutsches Forschungszentrum für Künstliche Intelligenz GmbH Firmensitz: Trippstadter Strasse 122, D-67663 Kaiserslautern Geschäftsführung: Prof. Dr. Dr. h.c. mult. Wolfgang Wahlster (Vorsitzender) Dr. Walter Olthoff Vorsitzender des Aufsichtsrats: Prof. Dr. h.c. Hans A. Aukes Amtsgericht Kaiserslautern, HRB 2313 ------------------------------------------------------------- [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Dear Andrej, It seems to me that the monad-on-a-category freely generated by one object should be the simplicial category Delta, following from the facts that Delta contains the universal monoid and a monad on C is a monoid in C^C - see Mac Lane Cats for Working Mathematician Section VII.5, VII.6. The object n of Delta will correspond to T^n(X) where T is the (functor for the) monad and X the generating object. If I've got that right then I would presume it's already known and proved carefully somewhere. After that, the monad-on-a-category freely generated by a category C would seem to be CxDelta. (Object (X,n) represents T^n(X), morphism (f,s): (X,m) -> (Y,n) corresponds to T^m(f);s(Y): T^m(X) -> T^m(Y) -> T^n(Y) and using naturality of T to deduce that s(Y);T^n(g) = T^m(g);s(Z) so the f's can always be shunted to the left.) Again, if I've got that right then it wouldn't surprise me to find it's already known. This would suggest that C |-> CxDelta is a monad on Cat. Then a monad on C is a structure morphism CxDelta -> C, i.e. Delta -> C^C with appropriate properties, which looks like a monoid in C^C, which we knew already. I don't know Knuth-Bendix well enough to understand the issues there. But since you mention various orderings, that reminds me of Freyd's trick in "essentially algebraic" presentations of these cartesian theories. (Amongst theories of partial operators, it is the cartesian theories that have good universal algebraic properties.) That involves ordering the operators so that, for each one, its domain of definition is defined by equations involving "earlier" operators. (Ultimately that comes down to total operators, for which no equations are needed.) Then the equations s = t are understood in the sense "if s and t are both defined, then they are equal". I don't know if that can be accommodated in Knuth-Bendix as it stands. In particular, I don't know how amenable K-B is to incorporating conditional rewrites. Conditional equations seem inevitable in cartesian theories; the essentially algebraic formulation reduces them to definedness explicitly conditional on equations, and equations implicitly conditional on definedness. You might want to look at my paper with Palmgren, which unifies them by identifying definedness with self-equality. You ask whether a free "monad on a category" is the same as a "free monad" on "free category". Of course, in using the word "free" one ought to be careful what kind of structure these are free over, but generally speaking if the forgetful functors compose then so will their left adjoints, the free functors. Best wishes, Steve. Andrej Bauer wrote:
Consider the theory of a monad, i.e., the axioms are those of a category and a monad given as a triple: an operation T on objects, for each object A a morphism eta_A : A -> T A, and an operation lift_{A,B} which maps morphisms f : A -> T B to lift f : T A -> T B. Concretely, the axioms are (where lift f is written f* and composition is juxtaposition):
id f = f f id = f (f g) h = f (g h) eta* = id f* eta = f (f* g)* = f* g*
Presumably, the equational theory (with partial operations) of such a triple is decidable. Is this known? If we ignore the types and partiality, we can attempt to turn the above equations into a confluent terminating rewrite system using the Knuth-Bendix algorithm, but it gets stuck (on various orderings I tried).
A more categorical way of asking the same question is: what is a concrete description of the free "monad on a category" (is this the same as "free monad" on "free category"?).
With kind regards,
Andrej
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Hi, Sam Lindley and Ian Stark proved that Moggi's computational Metalanguage (\lambda_ML) is decidable - this is simply typed lambda calculus with a monad. If I am not mistaken your theory can be faithfully encoded in \lambda_ML. Actually, isn't it the case that the continuation monad is actually the free monad. Hence, using this result decidability of \lambda_ML should follow from the decidability of simply typed lambda calculus. Cheers, Thorsten http://www.springerlink.com/content/y44yn0fg76dthfnn/ On 3 Jun 2009, at 12:10, Andrej Bauer wrote:
Consider the theory of a monad, i.e., the axioms are those of a category and a monad given as a triple: an operation T on objects, for each object A a morphism eta_A : A -> T A, and an operation lift_{A,B} which maps morphisms f : A -> T B to lift f : T A -> T B. Concretely, the axioms are (where lift f is written f* and composition is juxtaposition):
id f = f f id = f (f g) h = f (g h) eta* = id f* eta = f (f* g)* = f* g*
Presumably, the equational theory (with partial operations) of such a triple is decidable. Is this known? If we ignore the types and partiality, we can attempt to turn the above equations into a confluent terminating rewrite system using the Knuth-Bendix algorithm, but it gets stuck (on various orderings I tried).
A more categorical way of asking the same question is: what is a concrete description of the free "monad on a category" (is this the same as "free monad" on "free category"?).
With kind regards,
Andrej
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
participants (5)
-
Andrej Bauer -
Sergey Goncharov -
Steve Lack -
Steve Vickers -
Thorsten Altenkirch