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