Think Stitch
PRINCIPIA  最近の更新


最弱事前条件による命令の定義域の表現

A Theory and Practice of Program Development [Derek Andrews, Springer, 1997] という本に出ている話が面白かったのでご紹介します。

また最弱事前条件 [A]R について復習させてください。おおまかにいうと,命令 A と事後条件 R に対する最弱事前条件というのは,事前状態に関する条件のことで,その条件を満たす状態から命令 A を実行すると必ず R を満たす状態になるというものです。「必ず」とあるのは2つの意味合いがあって,1つはエラーとか無限ループに陥らないということ,もう1つは非決定性があった場合に,どの選択肢が選ばれたとしても R を満たすということです。

この2つの意味合いのうち,エラーにならない,あるいは無限ループに陥らないという部分を緩和したものを Weakest Liberal Precondition というのだそうです。こちらは記号 <A>R で表します。A の実行がエラーになったり無限ループになったりする可能性のある事前状態に対して <A>R は真になるとします。つまり「もし命令 A の実行が無事に終了したとしたら,必ず R を満たす状態になる」というやや弱い意味になります。ここでの「必ず」は非決定性のことだけをいっていることになります。

状態空間上で考えると以下のようになります。

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

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

このとき次の関係が成り立ちます。

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

[A]true は命令 A の実行が停止するという条件になります。実際に計算してみるとわかります。

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

したがって先の式の意味は,最弱事前条件を停止性と Weakest Liberal Precondition に分けてかんがえることができるという意味になります。

命令の定義域

唐突ですが,ここで ¬[A]false を計算してみます。

\[ \begin{split} \neg [A]\mathsf{false} \quad \longleftrightarrow & \quad \neg \forall o. (i,o) \in A \Rightarrow \mathsf{false} \\ =& \quad \neg \forall o. (i,o) \notin A \\ =& \quad \exists o. (i,o) \in A \\ =& \quad i \in \mathrm{dom} A \end{split} \]

なんと ¬[A]false は命令 A の定義域を表すのですね。

先の関係式:

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

を使うと次のようになります。

\[ \neg [A]\mathsf{false} = \neg [A]\mathsf{true} \lor \neg \langle A \rangle \mathsf{false} \]

ここで \[ \neg [A]\mathsf{true} \quad \longleftrightarrow \quad (i,\bot) \in A \] ですから,意味は「エラーまたは無限ループになる可能性がある」です。

¬<A>false の方を計算してみます。

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

したがって ¬<A>false の意味は「事前状態 i に対応する事後状態 o が少なくとも1つは存在する」となります。平たくいえばエラーにも無限ループにもならず正常に終了する場合があるということです。

以上の関係を図示すると次のようになります:

一般に命令 A の定義域は3つの領域に分かれることになります。X は必ずエラーまたは無限ループになるケース,Y は必ず正常に停止するケースです。Z は両者を含む場合で,エラーまたは無限ループになるか,あるいは正常に終了するかが非決定的に定まります。

そういうわけで,最弱事前条件を使うと命令の定義域を表せること,それは一般に3つの領域からなることがわかりました。

1つ補足しておくと,[A]true は停止性の条件ですけど,それは ⊥ がないというだけで定義域に含まれていることは保証していないのですね。

コメント

物理学者の朝永振一郎先生が著書「物理学とは何だろうか」の中で次のようなことを書いていらっしゃいます。

「いったん理論を数式化して(F)のような数学的形式で法則があらわされると,あと物理学はいかに能率よく進むか,という点を示すのによい例ですので,くどいようですが注をしておきましょう。つまり(F)から出発していろいろな関係が簡単に導かれる例のなかから,目ぼしいものをいくつかひろってみるのです。」

-- 物理学とは何だろうか,p.209, 物理学生への注

プログラムの意味を厳密に考えるという点でも同じことがいえるのだなあと思う例でした。

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