Shades of Iteration: from Elgot to Kleene
This work addresses foundational theoretical gaps in iteration concepts for researchers in formal methods and algebra, but it is incremental as it builds on existing theories.
The paper establishes a formal connection between Elgot iteration and Kleene iteration using monadic frameworks and introduces while-monads to model systems with while-loops that may not satisfy Kleene algebra laws.
Notions of iteration range from the arguably most general Elgot iteration to a very specific Kleene iteration. The fundamental nature of Elgot iteration has been extensively explored by Bloom and Esik in the form of iteration theories, while Kleene iteration became extremely popular as an integral part of (untyped) formalisms, such as automata theory, regular expressions and Kleene algebra. Here, we establish a formal connection between Elgot iteration and Kleene iteration in the form of Elgot monads and Kleene monads, respectively. We also introduce a novel class of while-monads, which like Kleene monads admit a relatively simple description in algebraic terms. Like Elgot monads, while-monads cover a large variety of models that meaningfully support while-loops, but may fail the Kleene algebra laws, or even fail to support a Kleen iteration operator altogether.