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.
翻译:迭代的概念范围涵盖了从理论上最一般的Elgot迭代到特定形式的Kleene迭代。Bloom与Esik以迭代理论的形式深入探索了Elgot迭代的基本性质,而Kleene迭代则因作为(无类型)形式体系(如自动机理论、正则表达式与Kleene代数)的核心组成部分而得到广泛普及。本文以Elgot单子与Kleene单子为工具,建立Elgot迭代与Kleene迭代之间的形式化关联。同时引入一类新型的while单子,此类单子与Kleene单子类似,可通过代数术语进行相对简洁的描述。与Elgot单子相同,while单子覆盖了能有效支持while循环的广泛模型族,但这些模型可能不满足Kleene代数定律,甚至完全无法支持Kleene迭代算子。