Re: Decidability of the theory of a monad

[Thorsten Altenkirch <txa@Cs.Nott.AC.UK>]

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