テスト付きクリーネ代数とその使い方 - 檜山正幸のキマイラ飼育記 (はてなBlog)

テスト付きクリーネ代数（Kleene Algebra with Test; KAT）は、非決定性プログラムの分析のために、デクスター・コゥゼン（Dexter Kozen）により導入された代数構造です。このダイアリーで以前、テスト付きクリーネ代数について書いた記憶があるので日記内検索をしてみたら：

2005年7月22日：現実的な「while文の意味」は？

なんと2005年。しかも、「テスト付きクリーネ代数はイマイチだなー」という話でした。

確かに、非決定性状態遷移系のモデルとして、テスト付きクリーネ代数では不十分なことは多いのですが、そのぶん、単純で分かりやすいというメリットもあります。「用途によっては悪くない」とも思うので、あらためて紹介します。ただし、肝心のクリーネスターの説明を端折っているので、再帰や繰り返しの議論が欠けています。上記の2005年の記事や、以下の記事では再帰／繰り返しに触れています。

「プログラムの算術的計算法」の記事は、実質的にはテスト付きクリーネ代数の話と言ってもいいでしょう。

この記事の最後で例題を出しますが、これをテスト付きクリーネ代数で表現するのはけっこう面倒で、結果的に「クリーネ代数によるモデリングの問題」を指摘したことに（またしても）なったかも。

内容：

クリーネ代数
擬似コード
ブール代数、ガード条件、if文
例題：自然数の足し算の再帰的な定義
テスト付きクリーネ代数が不自然なところ

クリーネ代数

クリーネ代数は、非決定性プログラムのモデルとなる代数構造*1で、足し算と掛け算を持ちます。足し算を「+」、掛け算を「;」で表すことにします。掛け算記号は省略して、併置で代用することもあります。A, B, Cなどはクリーネ代数Kの要素だとします。

足し算 A + B は、プロラムAかBのどちらかが非決定性に実行することを意味します。AとBを同時にスタートさせて、早く終わったほうの結果を採用すると考えてもいいです（そのほうがたぶん分かりやすい）。特別なプログラムO（大文字オー、ゼロに似ている）があるとして、計算法則は以下のとおり。

(A + B) + C = A + (B + C)
O + A = A + O = A
A + B = B + A
A + A = A

まとめて言うと、足し算に関してベキ等な可換モノイドです。A + B = B のとき A ≦ B と定義すると、関係「≦」は順序関係になります。ホーア論理を展開するときなどは、この順序が重要になります。が、今回はこれ以上触れません。

掛け算 A;B は、2つのプロラムA、Bの順次実行です。特別なプログラムI（大文字アイ、イチに似ている）があるとして、計算法則は以下のとおり。

(A;B);C = A;(B;C)
I;A = A;I = A
O;A = A;O = O

掛け算は可換でもなくベキ等でもありません。

そして、左右からの分配法則が成立します。

(A + B);C = A;C + B;C
A;(B + C) = A;B + A;B

足し算のベキ等性（A + A = A）を除けば、小学校で習った自然数の計算と同じ法則性です。

クリーネ代数の眼目は、A^* と書かれるクリーネスター演算なのですが、今日は割愛します。冒頭に挙げた「プログラムの算術的計算法」の記事に、1 + A + A² + ... の形で触れています。

擬似コード

クリーネ代数の足し算は、2つ（以上）のプログラムを同時にスタートさせて、早く終わったほうの結果を採用することだと解釈して、次の擬似コード構文で書くことにします。

branch {
  A,
  B
}

「プログラムの算術的計算法 (続き＆完結）」では、choose or という擬似構文にしていました；そのココロは、コイントスでAかBを選んでどちらかを実行する -- そういう選択的実行を多数回繰り返したときの統計的な挙動を扱う立場でした。

branchは2つ（一般的には複数）のプログラムを同時に実行します。しかし、片一方の結果は捨てられるので、最初からやらなかったのと同じになります。それじゃ選択的実行と同じじゃないか、と；同じなんですが、片一方がO（破綻するプログラム）のときは、branch解釈のほうが少し分かりやすい気がします。

IとOの意味は（「プログラムの算術的計算法 (続き＆完結）」からコピー）：

I （skip）-- 空文、何もしない
O （hang） -- 先に進めないで制御不能／無反応になる

hangは無限ループだと思うといいでしょう。function hang() { while(true){} } という感じ。もっとも、これだとビジーループになるかもしれないので、function hang() { while(true){sleep(1)} } 。いや、どうせ何もしないならスリープの時間を思いっきり長くして、function hang() { sleep(FOREVER) } 、FOREVER = ∞ です。

「≡」をプログラムの同値性を示す記号だとして、クリーネ代数の計算法則（公理）のいくつかを擬似コードで書きなおしてみます。

branch {hang, A} ≡ A
branch {A, B} ≡ branch {B, A}
branch {A, A} ≡ A
skip;A ≡ A
hang;A ≡ hang
A;hang ≡ hang

branch, skip, hangの意味に従って解釈してみてください。

ブール代数、ガード条件、if文

Bはブール代数とします。p, q などはBの要素（i.e. p, q∈B）とします。論理演算and, or, notには、記号∧, ∨, ¬ を使います。trueを0, falseを1と書くこともあります。

ブール代数Bとクリーネ代数Kがあり、さらにブール代数がクリーネ代数に作用する一種のスカラー乗法「・」があるとき、(B, K, ・) はテスト付きクリーネ代数となります。スカラー乗法 (-・-):B×K→K は次の法則を満たすとします。

(p∧q)・A = p・(q・A)
(p∨q)・A = p・A + q・A
p・(A + B) = p・A + p・B
1・A = A
0・A = O

p・A の擬似コードは、 p then A としましょう。if-then-else の then です。p then A は if p then A else hang と書けますが、逆に then を使って if-then-else を定義できます。

if p then A else B ≡ branch {p then A, (not p) then B}

右辺をテスト付きクリーネ代数の式で書けば、p・A + (¬p)・B です。

p・A、擬似コードの p then A は、ガード条件pが付いたプログラムで、pが真に評価されればAが実行され、そうでないと無限ループに入って破綻します。直列実行のときにAが破綻するとプログラム全体が破綻しますが、branchのなかでの部分的破綻なら、別な選択肢（同時実行された別なスレッド／プロセス）に制御が移り実行が進行します（正確には、進行する可能性があります）。

テスト付きクリーネ代数は、「共有資源を持たず相互作用もしないマイクロプロセス」をふんだんに使ったプログラミングのモデルとして適切です。破綻したプロセスは放置して、生きているプロセスでどんどん仕事を進めてしまうのです。

例題：自然数の足し算の再帰的な定義

自然数（0を含める）に対して、1を足す演算succ（successor）、1を引く演算pred（predecessor）、ゼロかどうかを調べる述語isZeroが前もってあるとして、これらを使って自然数の普通の足し算を定義しましょう。succ(n) のような関数形式ではなくて、n.succ のようなメソッド風の記法を採用します（左から右に読めるように）。代入の記号は「:=」とします。

def (n, m).add  is {
  p := m.isZero;
  branch {
   p then n,
   not p then (n, m.pred).add.succ
 }
}

JavaScriptで普通に書くなら：

function add(n, m) {
 var p = isZero(m);
 if (p) {
   return n;
 } else {
   return succ(add(n, pred(m)));
 }
}

これを、テスト付きクリーネ代数に翻訳するには、X = N×N として、演算や述語をすべてX上で考える必要があります。例えば次のように定義します。

z:X→{0, 1}, z(n, m) = isZero(m)
I:X→X, I(n, m) = (n, m)
P:X→X, P(n, m) = (n, pred(m))
S:X→X, S(n, m) = (succ(n), m)

そして、A(n, m) = (n + m, m) となるAを次の方程式で定義します。

A = z・I + (¬z)・(P;A;S)

F(A) = z・I + (¬z)・(P;A;S) として不動点方程式の形に書けば：

A = F(A)

この方程式を、B = Map(X, {0, 1})、K = Rel(X, X) として作ったテスト付きクリーネ代数 (B, K, ・) の中で解けばいいわけです。

テスト付きクリーネ代数が不自然なところ

前節の設定では、X = N×N として、すべてをXの上で考えようとします。そのため、isZero, pred, succ を z, P, S に翻訳する必要がありました。この翻訳は明らかに任意性／恣意性があります。isZero:N→{0, 1}、pred:N→N、succ:N→N をそのまま使えたほうがいいですよね。

となると、単一の領域Xとその上の変換だけではなくて、N, N×N などを含む圏で考えたほうが自然でしょう。圏を設定すれば、型付きの写像を射として扱えます。

テスト付きクリーネ代数が不十分で使い勝手が悪い事があるのは、圏全体を使用せずに、単一の対象だけを持つ部分圏（ホムセットがクリーネ代数）に限定しているからでしょう。トレース付きモノイド圏やメイヤー加群の圏を使うと、より自然で柔軟な定式化ができるだろうと思います。

実は、メイヤー加群をベースにしてテスト付きクリーネ代数を定義する方法を試してみたんですが、これは面白いですよ。テスト付きクリーネ代数は、プリミティブな概念じゃなくて、述語やガード条件に関する性質から構成可能な代数系のようです。

*1:正規表現の代数構造と捉えることも多いですが、こここでは非決定性プログラムの話をします。