while文の意味を考えてみたのだけど、難しいね。
while(P){E}において、条件Pをブール代数のメンバーだと思って、実行文EのほうをKleene代数で定式化する、というアプローチがある。実行文のほうに部分性や不定性（非決定性）を持ち込むと、条件をpureなブール代数だと思うのは無理がある。真偽値を{true, false, TOP, BOTTOM}のようにせざるを得ない気がするが、当然にややこしくなる。
実行文のほうだけ部分性・不定性を認め、条件は全域・決定的だとするのも、それなりの意義はあるだろうが、なんか不徹底の感じはまぬがれない。うまくいくところだけを切り出している印象があるのだ。
実行の作用／効果（effect）だけでは、whileの意味論は不十分だから、いっそ“走行の履歴＝状態空間の軌道”をまるごと考えてはどうか？ Eが単純（atomicな）遷移だとして、while(P){E}は、遷移Eを何度か繰り返した離散軌道（状態点列）を描く。が、while(true){E}などは、無限軌道を描く可能性がある。
X, Yが実行文だとして、XもYもキチンと終了すると仮定する。そのとき、順次結合X;while(true){E};Y の軌道は（無限軌道も許すなら）定義できる。が、意味（denotations）のcompositionalityを保つには、[-]を意味写像だとして、[X;while(true){E};Y] = [X];[while(true){E}];[Y] が成立しなくてはならない。意味側での「;」は、軌道を“繋ぐ”操作だとして、無限軌道の後に別な軌道を繋ぐ操作がうまく定義できない。
常套的手段として、単一軌道の代わりに軌道集合を考えて、軌道αと軌道βが繋げなかったら、{α};{β} = {} と定義する方法がある。が、これでいいのかよ？ むしろ、αが無限軌道なら α;β = α って感じもする。軌道集合といっても、いろいろな定式化がある。どのように軌道集合を定義したら、whileをうまく説明できるのだろう？ その前に、軌道を使うのが適切かどうか、ってこともあるし。よくわからんな。
