Think Stitch
PRINCIPIA  最近の更新


双対性

数学の世界にはよく双対性という性質が現れますよね。例えば初等幾何学で点と直線を入れ替えた定理が成り立つとか。こういったものに出会うと,プラトンじゃないですけど,なんというか仮想的な世界がたくさんあってお互いが何らかの関係でつながってるような感じがして強く興味を引かれます。双対だと2つですから表裏というか影の世界というか。

論理学だと論理積と論理和の双対がよく知られています。否定による表裏の関係という意味では de Morgan の法則にその性質が現れています。

\[ \neg (p \land q) = \neg p \lor \neg q \]

これを限量子化すると存在限量と全称限量の双対になりますよね。

\[ \exists x. P(x) = \neg \forall x. \neg P(x) \]

こんなふうに表裏をひっくり返す操作(ここでは否定)で挟まれるようなパターンが出てくると面白いなあと思うのです。

他にも計算木論理(Computational Tree Logic, CTL)でも同じような双対性がありますよね。

\[ \mathsf{EF}p = \neg \mathsf{AG} \neg p \]

線型時相論理(Linear Temporal Logic, LTL)というか,一般に様相論理だとこうでしょうか。

\[ \lozenge p = \neg \square \neg p \]

プログラムの世界(といっても実際は数学ですが)でもこのようなひっくり返るパターンや挟まれるパターンが出てくるところがあったので,ちょっと書いてみます。特に結論めいたものがあるわけではない,とりとめのない単なる雑談です。

CSP の非決定的選択演算子とトレース意味論

CSP には非決定的選択の演算子があります。

\[ P \sqcap Q \]

トレース意味論だと,非決定的選択の意味はトレースの和集合として定義されます。

\[ \mathrm{traces}(P \sqcap Q) = \mathrm{traces}(P) \cup \mathrm{traces}(Q) \]

ここで記号の上下がひっくり返っているのは別に双対性のせいではなくて,単に詳細化関係の向きを一般的な慣習に合わせたかったからだと思います(勝手な推測です。調べたわけではありません)。

\[ P \sqsubseteq Q \quad \longleftrightarrow \quad \mathrm{traces}(P) \supseteq \mathrm{traces}(Q) \]

CSP の詳細化関係は非決定的選択によって次のように定義されています。

\[ P \sqsubseteq Q \quad \equiv \quad P \sqcap Q = P \]

これは次の集合の関係と整合しているわけです。

\[ P \supseteq Q \quad \equiv \quad P \cup Q = P \]

和集合 ∪ と交わり ∩ は双対ですけど,ここでは関係ありません。でも非決定的選択がトレース集合の和集合ならば,交わりに対応する演算はなんだろう?と思いますけどね :P

命令型言語の表示的意味

命令型プログラミング言語の文の意味は,状態空間 S 上の関係として表すことができますよね。わざとらしく書くとこんな感じです。文 A の意味を関係 R で表します。

\[ \mathcal{M}[\![A]\!] = R = \{(i,o) \ |\ {}_iR_o\} = \{(i,o) \ |\ (i,o) \in R \} \]

これは CSP のトレース意味論とよく似ています。表示的意味論だからあたりまえなんでしょうけど。いちいち意味関数 M[[A]] を書くのは面倒なので,誤解がない場合は省略して文と関係を同一視することにします。

1つ困るのは,エラーや無限ループの場合です。これを表す方法にはいくつかの流儀があるそうです。無限ループするだけの文を loop と書くことにすると,1つの流儀は無限ループに陥ってしまう事前状態 i にすべての状態を事後状態として対応させます。いわば,何が起こるかわからない,まったく情報がないという感じです。

\[ \mathsf{loop} = \{(i,o) \ |\ i \in S \land o \in S \} \]

もう1つの流儀は特別な値⊥を用意してエラーと無限ループを表すというものです。CSP の発散に対応するようなものでしょうか。

\[ \mathsf{loop} = \{(i,\bot) \ |\ i \in S \} \]

これはわかりやすいですけど,⊥の扱いがちょっと煩雑になって面倒なこともあります。ここではこちらの流儀を採用することにします。両方の和集合を chaos と書く人もいるようなので,CSP もその辺りを踏襲しているのかなあと思いました。

命令型言語の非決定的選択演算子

実用的なプログラミング言語だと CSP にあるような非決定的選択に対応する構成要素はありませんけど,原理的にはあり得ます。Dijkstra の guarded command には非決定的選択を表す構文があります。それに影響を受けていると思われるモデル検査ツール Spin の記述言語 Promela でも非決定的選択を表すことができます。

純粋には CSP の非決定的選択と同じように,演算子として導入することができます。これを四角で表します。文 A と B のどちらかを非決定的に選択して実行する文を A □ B で表すことにします。ふつうは少し縦長というか細い四角で表すんですけど,ここでは書けないので正方形で代用します。CSP だと外部選択に対応するのでちょっとややこしいですけどね。

非決定的演算子の意味は,関係の和集合になります。

\[ \mathcal{M}[\![A\ \square\ B]\!] = \mathcal{M}[\![A]\!] \cup \mathcal{M}[\![B]\!] \]

これは CSP の非決定的選択演算子の意味と同じです。

\[ \mathrm{traces}(P \sqcap Q) = \mathrm{traces}(P) \cup \mathrm{traces}(Q) \]

具体的に関係の要素で見てみます。ある状態 i に対して,文 A, B を実行するとそれぞれ事後状態 o1, o2 になるとします。

\[ \begin{split} A &= \{\ \ldots,\ i \mapsto o_1, \ldots \ \} \\ B &= \{\ \ldots,\ i \mapsto o_2, \ldots \ \} \\ \end{split} \]

このとき非決定的選択の意味は次のようになります。状態 i に対して2つの事後状態が対応しています。このような状況を表すために,表示的意味が関数ではなくて関係になっているわけです。

\[ A\ \square\ B = \{\ \ldots,\ i \mapsto o_1, i \mapsto o_2, \ldots \ \} \]

具体的な例だと,例えば代入文の非決定的選択などが書けます。

\[ x := 1\ \square\ x := 2 \]

これは CSP におけるイベントの非決定的選択にとても似ています。

\[ a \rightarrow P \sqcap b \rightarrow Q \]

非決定的選択が書けるようになると,例えば次のループが停止するのはどのようなときだろうかといった問題に興味がわきます。

\[ \mathrm{while}\ x > 0\ \mathrm{do}\ x := x-1\ \square\ x := x-2 \ \mathrm{od} \]

条件がこうだったらどうかとか。

\[ \mathrm{while}\ x \neq 0\ \mathrm{do}\ x := x-1\ \square\ x := x-2 \ \mathrm{od} \]

最弱事前条件と述語変換子

プログラムの正当性(詳細化関係)を確認するときには,表示的意味論を使って関係の世界に移してから検証するよりも,述語変換子を使って記号操作する方が楽です。文 A から作られる述語変換子 [A] は,プログラム変数で書かれた事後条件 R を最弱事前条件 [A]R に変換します。論理式に作用するオペレータということです。

最弱事前条件 [A]R はプログラム変数に関する論理式で,これを満たす変数の値から文 A を実行するとエラーも起こさず無限ループにもならず計算が終了して事後条件 R を満たす状態になります。関係の世界で説明すると次のようになります。右辺は事前状態 i についての論理式(述語)ということになります。

\[ [A]R \quad \longleftrightarrow \quad \forall o \in S_\bot. (i,o) \in A \Rightarrow R(o) \land o \neq \bot \]

文字通り,文 A によって事前状態 i に対応づけられる(結果として生じる)すべての事後状態 o がエラーにならず事後条件 R を満たすということです。

非決定的選択の最弱事前条件

定義に従って,任意の事後条件 R に対して非決定的選択の最弱事前条件を計算してみると次のようになります。

\[ \begin{split} [A\ \square\ B]R \quad \longleftrightarrow \quad & \forall o \in S_\bot. (i,o) \in A \cup B \Rightarrow R(o) \land o \neq \bot \\ =& \forall o \in S_\bot. (i,o) \in A \lor (i,o) \in B \Rightarrow R(o) \land o \neq \bot \\ =& (\forall o \in S_\bot. (i,o) \in A \Rightarrow R(o) \land o \neq \bot) \land \\ & (\forall o \in S_\bot. (i,o) \in B \Rightarrow R(o) \land o \neq \bot) \\ \longleftrightarrow \quad & [A]R \land [B]R \end{split} \]

まとめると次のようになります。

\[ [A\ \square\ B]R = [A]R \land [B]R \]

非決定的選択は関係の世界では和集合のようなものなのに,最弱事前条件ではひっくり返って論理積になっています。事後状態から事前状態に移るとひっくり返るということです。

このことは最弱事前条件の意味から考えると納得できるでしょう。非決定性のために1つの事前状態に複数の事後状態が対応する場合,そのすべてで事後条件 R が成り立たないと必ず R を満たすようになるとはいえないからです。

(ここでも,じゃあ和集合の反対の交わりだったらどうなんだとか思いますよねえ :P)

Weakest Liberal Preconditions

プログラムの意味を最弱事前条件で考えるときには,文がエラーを起こさず停止するかどうかと,その結果が事後条件を満たすかどうかを分けて考えるとよいそうです。実際,上の際弱事前条件だけでは文の意味を完全に表すことができません。正当性を部分正当性と完全正当性に分けて考えるのと同じです。完全正当性は部分正当性+停止性ということです。

もし文 A が停止するとしたら必ず事後条件 R を満たすというもっとも弱い事前条件を <A>R と書きます。 これを Weakest Liberal Precondition というそうです。日本語の訳語が見つかりませんでした。

\[ \langle A \rangle R \]

関係の世界で書くと次のようになります。左辺はプログラム変数に関する条件,右辺は事前状態 i に関する述語ということになります。

\[ \langle A \rangle R \quad \longleftrightarrow \quad \forall o \in S_\bot. (i,o) \in A \land o \neq \bot \Rightarrow R(o) \]

定義から次の式が成り立つことが容易にわかります。完全正当性が部分正当性と停止性の積であることを表しています。

\[ [A]R = [A]\mathsf{true} \land \langle A \rangle R \]

実際に [A]true を求めてみると,次のようにエラーあるいは無限ループにならない,したがって停止するという条件になります。

\[ [A]\mathsf{true} \quad \longleftrightarrow \quad \forall o \in S_\bot. (i,o) \in A \Rightarrow o \neq \bot \]

(じゃあ true の裏,つまり false に対する [A]false はなんだろう?とか思いますね。)

動的論理だと以下の対応があって, [A] と <A> は双対だと思うんですけど,述語変換子だとそうじゃないんですね...どういうことなんでしょ?

\[ \begin{split} \square \quad \longleftrightarrow \quad [A] \\ \lozenge \quad \longleftrightarrow \quad \langle A \rangle \end{split} \]

表示的意味を述語変換子で表す

上では述語変換子を関係で定義しましたけど,逆に文 A の表示的意味としての関係を述語変換子で表すことを考えてみます。簡単のためにプログラム変数は x 1つだけとして,状態を変数の値と同一視することにします。

最初のトライはこれでしょう?

\[ (i,o) \in A \quad \longleftrightarrow \quad [A](x=o) \qquad ? \]

これはうまくいきません。例えば次のように状態 i に状態 o とエラーが対応している場合,[A](x=o) は i に対して偽になってしまうからです。

\[ A = \{\ \ldots,\ i \mapsto o, i \mapsto \bot, \ldots \ \} \]

では liberal ならどうでしょうか?

\[ (i,o) \in A \quad \longleftrightarrow \quad \langle A \rangle (x=o) \qquad ? \]

これもだめです。状態 i に対して⊥だけが対応している場合,対応する事後状態は空ですから任意の事後状態が対応することになってしまいます。

ここで発想を転換して事後条件の否定を考えてみます。定義に照らして計算すると以下のようになります。

\[ \begin{split} \neg \langle A \rangle (x \neq o) \quad \longleftrightarrow \quad & \neg \forall o' \in S_\bot. (i,o') \in A \land o' \neq \bot \Rightarrow o \neq o' \\ =& \exists o' \in S_\bot. (i,o') \in A \land o' \neq \bot \land o = o' \\ =& (i,o) \in A \land o \neq \bot \end{split} \]

ご覧のように⊥以外の場合はこれで求められることがわかります。ここでも否定で挟まれた形が出てきました。

では⊥に対応する事前状態はどうしたら分かるかというと,これはすでに出てきました。

\[ \begin{split} \neg [A]\mathsf{true} \quad \longleftrightarrow \quad & \neg \forall o \in S_\bot. (i,o) \in A \Rightarrow o \neq \bot \\ =& \exists o \in S_\bot. (i,o) \in A \land o = \bot \\ =& (i,\bot) \in A \end{split} \]

以上の2つを合わせれば,述語変換子を使って関係を求めることができるわけです。

   §

ほんとにとりとめのない話になってしまいましたが,こんなささやかな例でも丁寧に計算してみると,期待どおりになったり,あるいは意外な結果が出て来たりと楽しいなあと思いました。

2014/03/01
© 2013,2014,2015 PRINCIPIA Limited