「クリーネ代数の圏化： ちょびっと」で、クリーネ代数を幾つかの方法で圏化／無限タワー化したら面白いかもなー、と書きました。で、圏化のもとになるクリーネ代数ですが、何度も取り上げている割には定義はしたことないですね。定義は「探せばあるだろう」という前提ですが、圏化を見越した定義を改めてしておいたほうがいいかな、と思いました。
内容：
何に使えるのか／何に使いたいのか
「クリーネ代数〈Kleene algebra〉とは何か」の前に、クリーネ代数は何に使えるのか？ 僕が何に使いたいと思っていた／いるのかを説明します。僕が想定している用途は主に2つで、
- プログラム意味論
- 形式言語理論
です。今ここではプログラム意味論のほうだけ述べます。クリーネ代数は、非決定性プログラムの記述と分析に使えます。だいぶ古いですが、次の3つの記事を読むと事情はわかるでしょう。
非決定性プログラムの意味論をやりたい場合は、単なるクリーネ代数ではなくて、論理条件〈logical condition〉に相当するテストも入れたほうが便利です。これはテスト付きクリーネ代数〈Kleene algebra with tests〉です。テスト付きクリーネ代数については、次の記事で書いています。
テスト付きクリーネ代数を使えば、if文やwhile文も代数的に定義できます。ホーア論理〈Hoare logic〉を組み立てることもできます。以下の記事はホーア論理に関するものですが、テストフレームワークを実際に作っていたときに書いた記事なので、現実的な考慮が色々入っていて、理論的な筋は若干見えにくいかも知れません。
クリーネ代数とはちょっと離れますが、ホーア論理の圏論的扱いについては：
というわけで、クリーネ代数／テスト付きクリーネ代数は、プログラムの振る舞いの分析、仕様記述の手法、テストフレームワークの作り方などに具体的な示唆を与えてくれます。これが、クリーネ代数／テスト付きクリーネ代数に興味を持つ（ひとつの、しかし大きな）動機です。
クリーネ代数とは何か
クリーネ代数を一言でいえば、アフィン線形不動点方程式を扱うための代数系です。となると、アフィン線形不動点方程式とは何か、から説明を始めるべきでしょう。
次は中学校で習った1次関数です。
- f(x) = ax + b
aを比例定数〈proportionality constant | coefficient of proportionality | proportional coefficient〉、bを定数項〈constant term〉と呼びます。関数のグラフの形状から、aを傾き、bをy切片とも呼びますね。
アフィン線形関数〈affine linear {function | map | mapping}〉は1次関数の別名に過ぎません。fをアフィン線形関数として、次の形の方程式をアフィン線形不動点方程式〈affine linear fixed point equation〉と呼びます*1。
- f(x) = x
f(x)の定数項が特に1の場合は：
- ax + 1 = x
この形のアフィン線形不動点方程式の解は、比例定数aだけから決まるので、それをa*と書きます。このa*のaのクリーネスター〈Kleene star〉と呼びます。つまり、次が成立することになります。
- aa* + 1 = a*
両辺に右からbを掛けると：
- a(a*b) + b = a*b
したがって、a*b は、一般的アフィン線形不動点方程式 ax + b = x の解です。
以上のような議論ができるためには、a, b, xが所属する代数系に何が要求され、何は要求されないでしょうか？
- 足し算と掛け算がないと、1次式（アフィン線形式） ax + b が書けないので、足し算と掛け算は必要。
- しかし、引き算と割り算はなくてもよい。
- ax と xa を別に扱えば、掛け算の可換性も必要ない。
というわけで、アフィン線形不動点方程式を云々するには、足し算と（可換とは限らない）掛け算を持っている代数系が必要です。そのような代数系を半環〈semiring〉と呼びます。
クリーネ代数は、半環に、アフィン線形不動点方程式の解を与えるクリーネスターが付いたものです。が、もう少し構造が要求されます。それは実例を挙げた後で説明します。
順序構造と最小不動点
H = {x∈R | x ≧ 0}∪{∞} とします。∞はどの実数よりも大きいとします。足し算と掛け算は普通どおりですが、∞との足し算・掛け算は別途定義します。
x, yを非負実際として、
| 足す | x | ∞ |
| y | x + y | ∞ |
| ∞ | ∞ | ∞ |
x, yを正実数として、
| 掛ける | 0 | x | ∞ |
| 0 | 0 | 0 | 0 |
| y | 0 | xy | ∞ |
| ∞ | 0 | ∞ | ∞ |
この定義で、足し算・掛け算の計算法則はすべて成立します（引き算・割り算は考えない）。クリーネスターは次のように定義します。
- 0 ≦ a ＜ 1 のとき、a* := 1/(1 - a)
- 1 ≦ a のとき、a* := ∞
ここで、1/(1 - a) に引き算と割り算を使ってますが、これはクリーネスターの定義のなかで実数の引き算／割り算を使っているだけで、H上の演算として引き算／割り算を認めているわけではありません。
記号の乱用で、H = (H, +, 0, ・, 1, (-)*) と定義します。・は掛け算です。Hは足し算／掛け算／クリーネスターを持った代数系です。
今定義したクリーネスター付き半環Hにおいて、アフィン線形不動点方程式 ax + b = x の具体例として、a = 1/2, b = 1 を考えると、
- (1/2)x + 1 = x
x = 2 は不動点方程式の解ですが、x = ∞ も解です。一般に、アフィン線形不動点方程式の解はひとつとは限りません。クリーネスターa*は、ax + 1 = x の最小の解とします。最小が意味を持つためには、大小が比較可能、つまり順序構造を持つ必要があります。
クリーネ代数の要件として順序構造も追加すると：
- クリーネ代数は、足し算、掛け算、順序を持つ順序半環である必要がある。
- クリーネスターa*は、ax + 1 = x の最小の解を与える。
クリーネ代数の定義
クリーネ代数の公理を整備したのはデクスター・コゥゼン（Dexter Kozen）です。コゥゼンの定義では、足し算はベキ等、つまり a + a = a を仮定します。しかし、ベキ等性は要らない（強すぎる）でしょう。ベキ等性を要求すると、前節のHは除外されてしまいます。僕は、Hはクリーネ代数の仲間に入れてもいいと思うのです。
足し算のベキ等性は、半環上に順序を定義するために使われるのですが、足し算から誘導しなくても、順序が最初から在るとすればいいでしょう。クリーネ代数の下部構造を、ベキ等半環〈idemopotent semiring | ISR〉から順序半環〈ordered semiring | OSR〉に切り替えればいいのです。正確に言うと、0 ≦ a が成立する順序半環です。念の為、公理を書き出しておきます。以下の8番目までが半環の定義、その後は順序に関する定義です。全ての等式・不等式の前に全称限量子が付きますが、通常の習慣（悪習）にしたがって省略します。
- (a + b) + c = a + (b + c)
- 0 + a = a + 0 = a
- a + b = b + a
- (a・b)・c = a・(b・c)
- 1・a = a・1 = a
- 0・a = a・0 = 0
- a・(b + c) = a・b + a・c
- (a + b)・c = a・c + b・c
- ≦ は順序関係（全順序とは限らない）
- 0 ≦ a
- a ≦ b ⇒ a + c ≦ b + c
- a ≦ b ⇒ a・c ≦ b・c
- a ≦ b ⇒ c・a ≦ c・b
Hはこれらの公理を満たします。ZやRでは ∀a.(0 ≦ a) が成立しないので、ZやRは上記の公理は満たしません。
さて、Kは今提示した公理を満たす順序半環だとします。Kは半環なので、アフィン線形関数 f:K→K, f(x) = ax + b を考えることができます。t∈K がfの前不動点〈pre-fixed point | pre-fixpoint〉だとは、次が成立することです。
- f(t) ≦ t
最小不動点〈least fixed point〉であることは、最小前不動点〈least pre-fixed point〉であることと同じな同様に扱えるので、次の2つの条件を満たすtは最小不動点となりみなせます。
[追記]等式で定義される不動点と不等式で定義される不動点は、似た扱いはできますが、完全に同じと言うのは不適切でした。ホントに同じなら区別する必要がなくなるので。最後の節に書いたように、不等式的不動点理論と等式的不動点理論の差と関連を僕は理解してないのですが、安直に同じってのはマズイですね。[/追記][さらに追記 date="2018-10-16"]修正したけど、それはそれで別な誤解をまねきそうな気がしてきた。ウーン。補足記事を書いたほうがいいかも（書くとは言ってない）。[/さらに追記][さらにさらに追記 date="2018-10-19"]結局、補足説明を書きました。
[/さらにさらに追記]
f(x) = ax + b と展開した形で書くと：
- at + b ≦ t
- ∀x∈K.(ax + b ≦ x ⇒ t ≦ x)
aのクリーネスターa*を使えば、t = a*b で与えられるはずなので、
- a(a*b) + b ≦ a*b
- ∀x∈K.(ax + b ≦ x ⇒ a*b ≦ x)
一番目の不等式を簡略化して：
- aa* + 1 ≦ a*
- ∀x∈K.(ax + b ≦ x ⇒ a*b ≦ x)
これがクリーネスターを規定する公理です。順序半環Kと、写像 (-)*:K→K の組 (K, (-)*) が上記の2つの公理を満たすとき、右クリーネ代数〈right Kleene algebra〉と呼ぶことにします。なぜ「右」が付くのかは次節で。
可換性とベキ等性
クリーネ代数の定義では、掛け算の可換性は仮定しません。例えば、Kが非決定性プログラムの代数だとすると、掛け算はプログラムの順次結合なので、まったく可換ではありません。非可換の場合は、一次式〈アフィン線形式〉は2種類になります。
- ax + b
- xa + b
比例定数を左から掛けるバージョンと右から掛けるバージョンです。比例定数ではなくて変数の位置のほうに注目すると、上が右アフィン線形式、下を左アフィン線形式と呼びましょう。毎度注意してますが、左右の決め方は恣意的なので、二種類を区別する以外の意味は何もありません。
前節では、右アフィン線形不動点方程式に基づきクリーネ代数を定義しました。なので、右クリーネ代数です。左アフィン線形不動点方程式に基づき定義すれば、左クリーネ代数〈left Kleene algebra〉になります。左クリーネ代数を定義する公理は：
- a*a + 1 ≦ a*
- ∀x∈K.(xa + b ≦ x ⇒ ba* ≦ x)
ひとつのクリーネスター(-)*が、同時に右クリーネ代数と左クリーネ代数の構造を与えるとき、(K, (-)*) をクリーネ代数〈Kleene algebra〉と呼びます。
下部構造の順序半環が可換のとき、左右の区別はなくなるので、右クリーネ代数は左クリーネ代数にもなり、常にクリーネ代数になります。
半環の足し算がベキ等で、順序と整合している（a + b = b ⇔ a ≦ b）とき、クリーネ代数はベキ等クリーネ代数〈idempotent Kleene algebra〉です。コォゼンのオリジナルの定義によるクリーネ代数は、ベキ等クリーネ代数のことです。ベキ等性を外すとうまくいかないことも当然にあるでしょう。そのときはベキ等性を追加します*2。
コンウェイ半環
前節まででクリーネ代数の話はオシマイ。この節はオマケです。
不動点を扱うための代数系というと、コンウェイ半環〈Conway semiring〉もあります。ちなみに、コンウェイ代数〈Conway algebra〉は別な代数系を意味するので、コンウェイ半環と呼びます。
コンウェイ半環は、スターオペレータを持つ半環 L = (L, (-)*) で、次の等式を満たすものです。
- (a + b)* = (a*b)*a* --(和スター等式)
- (ab)* = 1 + a(ba)*b --(積スター等式)
和スター等式（公式）については、次の記事で説明しています。
クリーネ代数は不等号（順序）に基づく法則で規定されますが、コンウェイ半環は、完全に等式的な代数系です。この2つは別物なんですが、圏化するとクリーネ代数とコンウェイ半環の違いはハッキリしなくなります。不動点を扱う圏は、クリーネ代数の圏化とも言えるし、コンウェイ代数の圏化とも言えるような圏になります（たぶん、だいたい）。
クリーネ代数とコンウェイ半環は別だが似てるのは知ってました。が、相互関係を僕は理解してません。圏化すると、ほんとに違いが消えるのか、やっぱり別な圏になるのか？ 正確には知らないなー。気力が湧いたら考えます。
