現実的な「while文の意味」は？

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をカタカナ書きすることにしました。