Shades of Iteration: from Elgot to Kleene

TL;DR

This paper explores the theoretical relationship between Elgot and Kleene iteration through the introduction of Elgot, Kleene, and while-monads, providing a unified algebraic framework for iteration concepts.

Contribution

It establishes a formal connection between Elgot and Kleene iteration via monads and introduces while-monads, expanding the algebraic understanding of iteration models.

Findings

Defines Elgot, Kleene, and while-monads and their relationships.

Shows that while-monads support while-loops but may not satisfy Kleene algebra laws.

Provides a unified algebraic framework for different iteration concepts.

Abstract

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.