1つ前の「檜山用メモ」で書いたことに追加。だが、用語の意味を知っていれば、単独で読めるエントリーのつもり(?)。
条件Pをブール代数のメンバーだと思って、実行文EのほうをKleene代数で定式化する、というアプローチがある。
これを少し説明してみます。
ifやwhileで使う条件の全体をブール代数Bだと思って、実行文(コマンド)の全体はクリーネ代数*1Kだと思います。ブール代数の演算∧、∨、¬は普通に定義し、クリーネ代数は、x;y が順次実行、x + y がxとyのどちらかが実行される(したがって、両方のケースを考える)、x* はxを何回か(0階でもOK)繰り返し実行だと定義します。
Bのメンバーである条件pは、ガード(guard)としてKのメンバーに作用すると考えます。ガードとは、実行に先立ちチェックされる条件で、ガード条件が真でないときは、実行が中断(abort)されます。つまり、ガード付き文(guarded statement/command)p.x は、if(p) then x else Abort
のこと。AbortはNop(何もしない、Skipとも書く)とは違いますから注意! 捕捉不可能な例外みたいなもんだと思ってください。
ブール代数がガードとして作用しているクリーネ代数を“テスト付きクリーネ代数”(Kleene algebra with test; 略称KAT)と呼びます。Dexter Kozenの定義では、BがKの部分集合で、∧が;で、∨が+で実現されるようになっています。木下さん/古澤さんの論文(PDF)では、「部分集合であることは本質ではない」というコメントがあったと記憶してますが、部分集合のほうが計算は簡単です。いずれにしても、条件pをコマンドと考えたものをi(p)(i(p) = pでもよい)とすると、p.x = i(p);x という等式が成立します。
p.x の解釈(if(p) then x else Abort
)に基づくと、if(p) then x else y
は、p.x + (¬p).y と書けます。while(p) {x}
を、一回分の実行を外に出して書き換えると、if(p) then {x; while (p){x}} else Nop
ですね。while(p) {x}
をw(p, x)と略記して、KATの言葉で書けば:
w(p, x) = p.(x;w(p, x)) + (¬p).1
これは、w(p, x)を未知数とする再帰方程式です。w(p, x)を再びXと書き換えて、整理すると:
X = (i(p);x);X + (¬p)
これは、クリーネ代数のなかの線形再帰方程式なので、クリーネスターを用いて解けて、X = w(p, x) = (i(p);x)*(¬p)。これで、while文のpurely algebraicな表現が得られました。
なんてエレガントなんでしょう。って、ホントに? 確かにエレガントなんですけど、エレガントすぎて虚弱な感じがします。まず、条件の全体がブール代数になるかどうかがあやしい。p + ¬p = 1 が成立するためには、pがtotally definedじゃないといけないけど、それは保証しにくいですね。それと、先の線形再帰方程式で、p = 1(正確には、p = true, i(p) = 1)としてみると:
X = x;X
になってしまい、非自明な解は得られません。これは、無限ループはクリーネ代数のなかに適切な表現を持たないからです。
「無限ループなんて意味ないから相手にしなければいいじゃないか」という意見は却下。リアクティブ・システムを考えてみれば、無限ループじゃないと意味がないこともあるのですから。
というわけで、無限ループも含めてwhile文を解釈できて、できることなら、それでもなおalgebraicな意味論が希望なのです。極限操作が入るので、完備性のような、algebraicでない概念が必須になるのかもしれないけど。
*1:Kleeneをカタカナ書きすることにしました。