クリーネ代数（クリーネだいすう、）は、冪等半環に反復を表す単項演算 を付加した代数的構造であり、正規表現・正則言語・有限オートマトン・二項関係・プログラム意味論に現れる反復的現象を統一的に記述する。現代的定式化では、和 により誘導される自然半順序のもとで、星演算が特定の帰納法公理を満たす冪等半環として定義される。正則言語の代数はその標準的モデルであり、コーゼンの完全性定理によれば、抽象的クリーネ代数の等式理論は正規表現の意味論と一致する。
この概念の起源はクリーネの正規事象の理論にあり、サロマーが正規表現の変形体系を公理化し、コンウェイが正則代数の観点から体系化したのち、コーゼンが抽象的クリーネ代数に対する有限公理系と完全性定理を与えた。以後、クリーネ代数は形式言語論のみならず、関係意味論、動的論理、プログラム検証、Kleene algebra with tests などの研究領域へ拡張された。
定義 集合 上の代数系
がクリーネ代数であるとは、以下を満たすことをいう。
は可換冪等モノイドである。すなわち、
が成り立つ。 はモノイドである。すなわち、
が成り立つ。 積は和に関して左右分配的であり、 は積に関して吸収的である。すなわち、
が成り立つ。 自然半順序
を導入したとき、星演算 は
および
を満たす。
最後の二つの含意は左帰納法公理・右帰納法公理と呼ばれる。これらは、星演算が反復の最小解を与えることを表現している。
自然半順序 冪等律 により、演算 は自然半順序 に関する二項上限を与える。すなわち、
かつ
である。したがって、クリーネ代数は半束的な順序構造と両立する半環として理解できる。
この順序論的視点は、星演算の意味を理解するうえで本質的である。言語モデルでは は言語の包含、関係モデルでは関係の包含を意味するから、 は有限回の反復により得られる全体を表す。
星演算と最小前不動点 クリーネ代数における星演算の重要な解釈の一つは、最小前不動点としての解釈である。任意の に対し、写像
を考えると、左帰納法公理は
を主張する。さらに から
が従うため、 自身が の前不動点である。したがって は、 の前不動点全体の中で最小のものになる。右側についても同様に、 は写像 の最小前不動点である。
この見方は、星演算を単なる記号的反復ではなく、線形不等式
または
の最小解として理解するものであり、関係意味論やプログラム意味論に直結する。たとえば関係モデルでは、 は遷移関係 を有限回たどって初期集合 から到達可能な全状態の集合を表す。
順序がさらに完備であり、積が適切な連続性を満たす場合には、
という表示が成り立つ。すなわち、最小前不動点は有限反復列
の上限として具体化される。一般のクリーネ代数ではこの上限表示は定義の一部ではないが、星連続クリーネ代数ではこれが成立する。
基本性質 公理から、つぎの恒等式が導かれる。
また、和・積・星は自然半順序に関して単調である。すなわち、 ならば
が成り立つ。
標準的モデル 正則言語 有限アルファベット に対し、正則言語全体の集合は、和を和集合、積を言語の連接、 を空言語、 を空語のみからなる言語、星を通常のクリーネ閉包として定めることでクリーネ代数をなす。これは最も基本的なモデルであり、クリーネの定理の意味論的基盤を与える。
二項関係 集合 上の二項関係全体は、和を和集合、積を関係の合成、 を空関係、 を恒等関係、星を反射推移閉包として定めることでクリーネ代数になる。ここで は、0回以上の 遷移による到達可能性を表す。
行列 任意のクリーネ代数 に対し、 上の正方行列全体は、成分ごとの和と通常の行列積により再びクリーネ代数をなす。これは有限オートマトンの遷移行列表示と直結し、完全性定理の証明でも中心的役割を果たす。
完全性定理 クリーネ代数論の中心結果は、コーゼンによる完全性定理である。有限アルファベット 上の正規表現 について、つぎは同値である。
クリーネ代数の公理から が導かれる。 と は 上の正則言語として同一の意味をもつ。
すなわち、抽象的クリーネ代数の等式理論は、正則言語の代数における等式理論と一致する。コーゼンはこの主張を、 上の正則言語の代数が生成元 上の自由クリーネ代数であることと同値な形で述べている。
自由クリーネ代数としての正則言語 自由クリーネ代数であるとは、任意のクリーネ代数 と写像 に対し、 を一意に拡張するクリーネ代数準同型
が存在することをいう。これは、正規表現の各文字を の元へ送り、それを和・積・星に関して評価する操作が、正則言語代数全体へ一意に延長されることを意味する。
この普遍性により、正規表現の同値性判定は、自由クリーネ代数における語の等式判定として理解される。したがって、形式言語論の基本問題は、普遍代数的には自由対象の語の理論を調べる問題として再解釈される。
証明戦略の概略 コーゼンの証明は、正規表現・有限オートマトン・行列クリーネ代数のあいだの対応を公理的に再構成することを本質としている。まず行列も再びクリーネ代数をなすことを用いて、任意の項をオートマトン的対象へ翻訳できることを示す。そこから、有限オートマトン論の古典的変換を代数的に模倣し、最終的に正規表現の等式が正則言語の一致へ還元される。
この証明で重要なのは、古典的なクリーネの定理が、単なる言語論の結果としてではなく、クリーネ代数の公理から再導出される点にある。これにより、正規表現とオートマトンの往復は、個別の集合論的構成ではなく、公理的に正当化された変換として理解される。
正規表現と有限オートマトン クリーネの古典的結果によれば、有限オートマトンで受理される言語のクラスは、空集合・空語・文字から出発して和・連接・星により生成される言語のクラスと一致する。これは通常、クリーネの定理と呼ばれる。
コーゼンはこの事実を、遷移行列上の計算と星演算を用いて抽象的クリーネ代数の完全性定理へと再編成した。したがって、有限オートマトン論は、自由クリーネ代数の具体モデルを与える理論として位置づけることができる。
歴史 1956年のクリーネの論文は、後に正規表現の基本演算と見なされる和・連接・星を用いて有限オートマトンで表現される事象を記述した。1966年、サロマーは正規表現の変形について完全公理系を与えた。1971年のコンウェイの著作は、正則代数と有限機械の理論を広く体系化した。1994年、コーゼンは抽象的クリーネ代数に対する有限公理系と完全性定理を与え、1997年以降は KAT によりプログラム検証との関係が発展した。
星連続クリーネ代数 クリーネ代数の重要な変種として星連続クリーネ代数（star-continuous Kleene algebra）がある。これは、適切な順序論的意味で
が成り立つものをいう。言語モデルや関係モデルなど、多くの自然なモデルではこの連続性が成り立ち、星演算は有限冪の増大列の上限として理解できる。これに対し、一般のクリーネ代数では、星演算は公理的に与えられる反復演算として扱われる。
クリーネ代数 with tests クリーネ代数 with tests（KAT）は、クリーネ代数の内部にブール代数としてのテストを埋め込んだ拡張構造である。ここでテストは条件式、一般の元はプログラム片ないし遷移に対応する。積は逐次合成、和は非決定的選択、星は反復実行を表すため、KAT は while プログラムの代数的意味論を与える。
KAT においても、星演算の最小前不動点としての性質は中心的であり、プログラム反復の不変量推論と密接に結びつく。コーゼンはさらに、命題 Hoare 論理が KAT の等式推論に埋め込まれることを示した。
決定可能性と計算量 クリーネ代数の等式理論は決定可能であり、コーゼンはその推論問題の計算量を研究した。関連する理論では PSPACE 完全性を含む高い複雑性が現れ、KAT についても同様に計算量的困難さが知られている。
数学的意義 クリーネ代数の数学的意義は、反復という動的概念を、半環構造・順序・帰納法公理によって静的な代数理論へ翻訳した点にある。自由クリーネ代数の定理は、正則言語論を普遍代数の言葉で把握することを可能にし、最小前不動点としての星演算は、反復の意味論を順序論的に基礎づける。こうしてクリーネ代数は、形式言語論・オートマトン理論・関係意味論・プログラム検証を横断する共通基盤を提供する。
脚注
参考文献
関連項目 クリーネ閉包 正規表現 正則言語 有限オートマトン 冪等半環 二項関係 ホーア論理 プログラム意味論 不動点