Decidability of the theory of a monad

Decidability of the theory of a monad

[Andrej Bauer]

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/ ]

Re: Decidability of the theory of a monad

[Thorsten Altenkirch]

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/ ]

Re: Decidability of the theory of a monad

[Steve Vickers]

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/ ]

Re: Decidability of the theory of a monad

[Sergey Goncharov]

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/ ]

Re: Decidability of the theory of a monad

[Steve Lack]

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/ ]

Re: Decidability of the theory of a monad

[Andrej Bauer]

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/ ]