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 Seiten 18-33 Lecture Notes in Computer Science (LNCS) 5728 Springer Berlin 9/2009.


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.


Weitere Links

kleene.pdf (pdf, 224 KB )

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence