Publication
Kleene Monads: Handling Iteration in a Framework of Generic Effects
Sergey Goncharov; Lutz Schröder; Till Mossakowski
In: Alexander Kurz; Andrzej Tarlecki (Hrsg.). Algebra and Coalgebra in Computer Science. Conference on Algebra and Coalgebra in Computer Science (CALCO-09), Third International Conference, September 6-10, Udine, Italy, Pages 18-33, Lecture Notes in Computer Science (LNCS), Vol. 5728, Springer, Berlin, 9/2009.
Abstract
Monads are a well-established tool for modeling various
computational effects. They form the semantic basis of Moggi's
computational metalanguage, the metalanguage of effects for
short, which made its way into modern functional programming in the
shape of Haskell's do-notation. Standard computational idioms call
for specific classes of monads that support additional control
operations. Here, we introduce Kleene monads, which additionally
feature nondeterministic choice and Kleene star, i.e.
non-deterministic iteration, and we provide a metalanguage and a
sound calculus for Kleene monads, the metalanguage of control
and effects, which is the natural joint extension of Kleene
algebra and the metalanguage of effects. This provides a framework
for studying abstract program equality focussing on iteration and
effects. These aspects are known to have decidable equational
theories when studied in isolation. However, it is well-known that
decidability breaks easily; e.g. the Horn theory of continuous
Kleene algebras fails to be recursively enumerable. Here, we prove
several negative results for the metalanguage of control and
effects; in particular, already the equational theory of the
unrestricted metalanguage of control and effects over continuous
Kleene monads fails to be recursively enumerable. We proceed to
identify a fragment of this language which still contains both
Kleene algebra and the metalanguage of effects and for which the
natural axiomatisation is complete, and indeed the equational theory
is decidable.