クリーネ代数

集合 ${\displaystyle K}$ 上の代数系

${\displaystyle (K,+,\cdot ,{}^{*},0,1)}$

がクリーネ代数であるとは、以下を満たすことをいう。^[2]

1. ${\displaystyle (K,+,0)}$ は可換冪等モノイドである。すなわち、

   ${\displaystyle a+(b+c)=(a+b)+c,\quad a+b=b+a,\quad a+0=a,\quad a+a=a}$

   が成り立つ。

2. ${\displaystyle (K,\cdot ,1)}$ はモノイドである。すなわち、

   ${\displaystyle a(bc)=(ab)c,\quad 1a=a1=a}$

   が成り立つ。

3. 積は和に関して左右分配的であり、${\displaystyle 0}$ は積に関して吸収的である。すなわち、

   ${\displaystyle a(b+c)=ab+ac,\quad (a+b)c=ac+bc,\quad a0=0a=0}$

   が成り立つ。

4. 自然半順序

   ${\displaystyle a\leq b\iff a+b=b}$

   を導入したとき、星演算 ${\displaystyle {}^{*}}$ は

   ${\displaystyle 1+aa^{*}\leq a^{*},\qquad 1+a^{*}a\leq a^{*}}$

   および

   ${\displaystyle ax+b\leq x\Rightarrow a^{*}b\leq x,\qquad xa+b\leq x\Rightarrow ba^{*}\leq x}$

   を満たす。^[2]

最後の二つの含意は左帰納法公理・右帰納法公理と呼ばれる。これらは、星演算が反復の最小解を与えることを表現している。^[2]

冪等律 ${\displaystyle a+a=a}$ により、演算 ${\displaystyle +}$ は自然半順序 ${\displaystyle \leq }$ に関する二項上限を与える。すなわち、

${\displaystyle a\leq a+b,\qquad b\leq a+b}$

かつ

${\displaystyle a\leq c,\ b\leq c\Rightarrow a+b\leq c}$

である。したがって、クリーネ代数は半束的な順序構造と両立する半環として理解できる。^[2]

この順序論的視点は、星演算の意味を理解するうえで本質的である。言語モデルでは ${\displaystyle a\leq b}$ は言語の包含、関係モデルでは関係の包含を意味するから、${\displaystyle a^{*}}$ は有限回の反復により得られる全体を表す。^[2][4]

クリーネ代数における星演算の重要な解釈の一つは、最小前不動点としての解釈である。任意の ${\displaystyle a,b\in K}$ に対し、写像

${\displaystyle f_{a,b}(x)=ax+b}$

を考えると、左帰納法公理は

${\displaystyle ax+b\leq x\Rightarrow a^{*}b\leq x}$

を主張する。さらに ${\displaystyle 1+aa^{*}\leq a^{*}}$ から

${\displaystyle aa^{*}b+b\leq a^{*}b}$

が従うため、${\displaystyle a^{*}b}$ 自身が ${\displaystyle f_{a,b}}$ の前不動点である。したがって ${\displaystyle a^{*}b}$ は、${\displaystyle f_{a,b}}$ の前不動点全体の中で最小のものになる。右側についても同様に、${\displaystyle ba^{*}}$ は写像 ${\displaystyle x\mapsto xa+b}$ の最小前不動点である。^[2]

この見方は、星演算を単なる記号的反復ではなく、線形不等式

${\displaystyle x=ax+b}$

または

${\displaystyle x=xa+b}$

の最小解として理解するものであり、関係意味論やプログラム意味論に直結する。たとえば関係モデルでは、${\displaystyle a^{*}b}$ は遷移関係 ${\displaystyle a}$ を有限回たどって初期集合 ${\displaystyle b}$ から到達可能な全状態の集合を表す。^[2][5]

順序がさらに完備であり、積が適切な連続性を満たす場合には、

${\displaystyle a^{*}b=\sup _{n\geq 0}a^{n}b}$

という表示が成り立つ。すなわち、最小前不動点は有限反復列

${\displaystyle b,\ ab+b,\ a^{2}b+ab+b,\ \dots }$

の上限として具体化される。一般のクリーネ代数ではこの上限表示は定義の一部ではないが、星連続クリーネ代数ではこれが成立する。^[2][5]

公理から、つぎの恒等式が導かれる。^[2][4]

• ${\displaystyle 1+aa^{*}=a^{*}}$
• ${\displaystyle 1+a^{*}a=a^{*}}$
• ${\displaystyle a^{*}a^{*}=a^{*}}$
• ${\displaystyle a^{**}=a^{*}}$
• ${\displaystyle 1\leq a^{*}}$
• ${\displaystyle a\leq a^{*}}$

また、和・積・星は自然半順序に関して単調である。すなわち、${\displaystyle a\leq b}$ ならば

${\displaystyle a+c\leq b+c,\qquad ac\leq bc,\qquad ca\leq cb,\qquad a^{*}\leq b^{*}}$

が成り立つ。^[2]

クリーネ代数論の中心結果は、コーゼンによる完全性定理である。有限アルファベット ${\displaystyle \Sigma }$ 上の正規表現 ${\displaystyle e,f}$ について、つぎは同値である。^[2]

1. クリーネ代数の公理から ${\displaystyle e=f}$ が導かれる。
2. ${\displaystyle e}$ と ${\displaystyle f}$ は ${\displaystyle \Sigma }$ 上の正則言語として同一の意味をもつ。

すなわち、抽象的クリーネ代数の等式理論は、正則言語の代数における等式理論と一致する。コーゼンはこの主張を、${\displaystyle \Sigma }$ 上の正則言語の代数が生成元 ${\displaystyle \Sigma }$ 上の自由クリーネ代数であることと同値な形で述べている。^[2]

自由クリーネ代数であるとは、任意のクリーネ代数 ${\displaystyle K}$ と写像 ${\displaystyle h\colon \Sigma \to K}$ に対し、${\displaystyle h}$ を一意に拡張するクリーネ代数準同型

${\displaystyle {\hat {h}}\colon \mathrm {Reg} (\Sigma ^{*})\to K}$

が存在することをいう。これは、正規表現の各文字を ${\displaystyle K}$ の元へ送り、それを和・積・星に関して評価する操作が、正則言語代数全体へ一意に延長されることを意味する。^[2]

この普遍性により、正規表現の同値性判定は、自由クリーネ代数における語の等式判定として理解される。したがって、形式言語論の基本問題は、普遍代数的には自由対象の語の理論を調べる問題として再解釈される。^[2]

コーゼンの証明は、正規表現・有限オートマトン・行列クリーネ代数のあいだの対応を公理的に再構成することを本質としている。まず行列も再びクリーネ代数をなすことを用いて、任意の項をオートマトン的対象へ翻訳できることを示す。そこから、有限オートマトン論の古典的変換を代数的に模倣し、最終的に正規表現の等式が正則言語の一致へ還元される。^[2]

この証明で重要なのは、古典的なクリーネの定理が、単なる言語論の結果としてではなく、クリーネ代数の公理から再導出される点にある。これにより、正規表現とオートマトンの往復は、個別の集合論的構成ではなく、公理的に正当化された変換として理解される。^[2]

クリーネの古典的結果によれば、有限オートマトンで受理される言語のクラスは、空集合・空語・文字から出発して和・連接・星により生成される言語のクラスと一致する。これは通常、クリーネの定理と呼ばれる。^[1]

コーゼンはこの事実を、遷移行列上の計算と星演算を用いて抽象的クリーネ代数の完全性定理へと再編成した。したがって、有限オートマトン論は、自由クリーネ代数の具体モデルを与える理論として位置づけることができる。^[2]

1956年のクリーネの論文は、後に正規表現の基本演算と見なされる和・連接・星を用いて有限オートマトンで表現される事象を記述した。1966年、サロマーは正規表現の変形について完全公理系を与えた。1971年のコンウェイの著作は、正則代数と有限機械の理論を広く体系化した。1994年、コーゼンは抽象的クリーネ代数に対する有限公理系と完全性定理を与え、1997年以降は KAT によりプログラム検証との関係が発展した。^{[1][3][4][2][5]}

クリーネ代数の重要な変種として星連続クリーネ代数（star-continuous Kleene algebra）がある。これは、適切な順序論的意味で

${\displaystyle pq^{*}r=\sup _{n\geq 0}pq^{n}r}$

が成り立つものをいう。言語モデルや関係モデルなど、多くの自然なモデルではこの連続性が成り立ち、星演算は有限冪の増大列の上限として理解できる。これに対し、一般のクリーネ代数では、星演算は公理的に与えられる反復演算として扱われる。^[2][5]

クリーネ代数 with tests（KAT）は、クリーネ代数の内部にブール代数としてのテストを埋め込んだ拡張構造である。ここでテストは条件式、一般の元はプログラム片ないし遷移に対応する。積は逐次合成、和は非決定的選択、星は反復実行を表すため、KAT は while プログラムの代数的意味論を与える。^[5]

KAT においても、星演算の最小前不動点としての性質は中心的であり、プログラム反復の不変量推論と密接に結びつく。コーゼンはさらに、命題 Hoare 論理が KAT の等式推論に埋め込まれることを示した。^[5][6]

クリーネ代数の等式理論は決定可能であり、コーゼンはその推論問題の計算量を研究した。関連する理論では PSPACE 完全性を含む高い複雑性が現れ、KAT についても同様に計算量的困難さが知られている。^[7][6]

クリーネ代数の数学的意義は、反復という動的概念を、半環構造・順序・帰納法公理によって静的な代数理論へ翻訳した点にある。自由クリーネ代数の定理は、正則言語論を普遍代数の言葉で把握することを可能にし、最小前不動点としての星演算は、反復の意味論を順序論的に基礎づける。こうしてクリーネ代数は、形式言語論・オートマトン理論・関係意味論・プログラム検証を横断する共通基盤を提供する。^[2][4][5]