著者

古澤 仁 高井 利憲 Hitoshi Furusawa Toshinori Takai 鹿児島大学理学部数理情報科学科 産業技術総合研究所システム検証研究センター Department of Mathematics and Computer Science Faculty of Science Kagoshima University Research Center for Verification and Semantics AIST.

出版者

日本ソフトウェア科学会

雑誌

コンピュータソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.23, no.3, pp.14-34, 2006-07-26

参考文献数

46

---

クリーニ代数は正規言語を公理的に取り扱うための代数的枠組みである.正規表現が計算機科学のいたるところに現れることを考えると,クリーニ代数が計算機科学に現れる構造の自然なクラスの性質を公理的にとらえ得るであろうことが容易に推測されるであろう.クリーニ代数の定義は,等式とホーン節で与えられるため,ある現象をクリーニ代数においてモデル化すると,その現象が簡単な式変形によって検証できるという特徴をもつ.本稿ではクリーニ代数の基本的な性質とそのプログラム理論への応用例について紹介する.A Kleene algebra is an algebraic framework to handle regular languages. Considering that regular expressions appear everywhere in fields of computer science, it may be easy to infer that a Kleene algebra can captures properties of natural class of structures appear in computer science. Since Kleene algebras are defined by equations and Horn clauses, if a phenomenon is interpreted in Kleene algebra, reasoning of the phenomenon is performed by simple transformations of expressions. We introduce basic properties and application examples of Kleene algebras to theory of programs.