Shades of Iteration: from Elgot to Kleene

要約

反復の概念は、最も一般的なElgot反復から非常に特殊なKleene反復まで様々である。Elgot反復の基本的な性質は、BloomとEsikによって反復理論の形で広範囲に探求され、Kleene反復は、オートマトン理論、正規表現、Kleene代数などの（型付けのない）形式主義の不可欠な部分として非常に人気があった。ここでは、ElgotモナドとKleeneモナドという形で、Elgot反復とKleene反復の間の形式的な接続をそれぞれ確立している。また、Kleeneモナドと同様に、比較的簡単な代数的記述を可能にするwhileモナドという新しいクラスも紹介する。Elgotモナドと同様に、whileモナドもwhileループを有意義にサポートする様々なモデルをカバーするが、Kleene代数法則に反したり、あるいはKleen反復演算子を完全にサポートしないこともある。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, DeepL