論理式の実験場を作る，
4 全数チェックへの道―― 数理的アプローチの基礎トレーニング 2藤倉 俊幸

を 3 個に固定して，すべての矢印の引き方を網羅すれば良いこ

1 前回のおさらいとになる．どんな矢印の引き方があるかは，図 1 のマトリック
ス型を見れば一目瞭然で，全部で 9 通りあることがわかる．こ前回（2006 年 11 月号）は，論理式の意味を理解するために，の 9 通りをリストすると，図 2 の左側のようになる．そして，こ与えられた論理式を真にする場合と偽にする場合を実際に作りの 9 通りを適当に組み合わせれば，一つの世界ができあがる．

出してテストする方法を説明した．しかし，たとえば，図 1 の例は，次の三本の矢印でできた世界である．

∀ x ∃ y（Q（x，y）→ Q（y，x））……………………………
（1）{ a → b，b → c，c → a }を偽にする場合を作り出せなかった．この論理式がつねに真でこのような組み合わせのすべてを作れば，3 人の世界のすべあることは，タブロー法などでだれでも証明できるし，プログてを作ることができる．組み合わせの作り方は，9 本の矢印のラム言語 Prolog で作ったプログラムなどでも証明できる．

集合の部分集合が一つの世界になるので，すべての部分集合をところが，Q（x，y）という述語を，「x は y が好き」と考えた作ればよい．つまりベキ集合を作れば，すべての世界の集合をとき，この論理式は，「すべての人（x）がそれぞれだれか（y）を生成したことになる．リスト 1 にすべての世界を生成するため愛するならば，そのだれか（y）からも愛される」という意味になの VDM++ モデルを示す．

り，これがつねに真であれば世の中から片思いがなくなってし

リスト 2 に∀ x ∃ y（Q（x，y）→ Q（y，x））の全数検査プログまう．こんなことは，にわかには信じられない．証明されてもラムを示す．この関数 alltest22 が，true だけの配列を返せ納得がいかないのでどうしようか ――というのが今回のテーマ

ば，この論理式 P22 がつねに真であることを疑う余地はなくなる．
リスト 1 とリスト 2 を見ただけでは，モデルの全体はわからである．
疑問点は，なぜつねに真になるのかということと，本当に片思いはなくなるのか，の二つである．

ないと思う．これらの関数は，前回作成した論理モデル・クラス（前回の図 12）の操作として追加することで使用できる．あるいは，論理モデル・クラスのサブクラスとして実装すれば良2 実験場の開発と反例探しい．実行結果の一部を図 3 に示す．

● 偽の場合を探すの世界までしか確認できなかった．4 人の場合は 216 個の世界を実験の結果はすべて true になった．しかし，残念ながら 3 人
まず，証明を疑ってみよう．つまり，本当は偽になる場合が検査するので VDM がやってくれなかった．結局，3 人までしか調べられなかったが，反例が出なかったことから証明を信用あるかもしれない．
前回は VDM++ を使用していろいろな場合で試してみたが，すべての場合を確認したわけではないし，もしかしたら見落とするしかないようである．

● プログラムの改良しているかもしれない．反例が一つでもあれば証明の結果を覆プログラムをくふうすれば，4 人の場合でも証明できる可能

すことができるが，すでにいろいろな場合をテスト済みなので，性があるが，3 人の世界で計算時間が 30 秒ほどかかったのと，ちからわざ残された道は力業の全数検査しかない．

4 人の次は 5 人ときりがないので，改良の方針のみを考えるこQ（x，y）の全数検査といっても，そんな途方もないことはでとにする．プログラムを改良するとすれば，ベキ集合は整数型きないので人数を制限して，3 人しかいない世界を考えることの各ビットを集合要素に対応させて 1 のビットに対応した要素にする．

だけをピックアップすれば，すべての部分集合を作ることがで3 人いるときの関係をどのように表現すれば良いか考えてみきる（前回のコラムを参照）．したがって，allRelation（k）の中る．グラフで描くと，図 1 のようにノードで人を表して矢印ででベキ集合を生成せず，部分集合を作りながら論理式の評価を関係を表すことができる．3 人いるときのすべての関係はノード行えば良さそうである．いわゆる on-the-fly 型である．それで176―― 形式仕様記述，自然言語と形式言語

Dec. 2006

Q（x，y）をどのように表現するか？
基本は矢印aQ（a，b）b

Q（c，a）

Q（b，c）cQ（x ，y）の世界をどのように表現するか?
1）グラフ2）マトリックス

aabbccabca010b001c100

Q（x ，y）は全部で9通りあることがわかる

図 1 関係をどのように表すか

3人いる場合のすべての二項関係は
3×3 = 9通り

k:= 3として
mapping : set of seq of nat1 := dunion { { [i,j] | j in set {1,...,k}} | i in set {1,...,k}};
によって生成することができる

a→aa→ba→c

power mappingによって生成できる

b→ab→bb→c

この関係のすべての組み合わせが3人で作る世界になる

c→ac→bc→c｛｝｛a→b｝，｛a→c｝，…
｛a→b，a→c｝，…
｛a→b，a→b，a→c｝，…
…
つまり，ベキ集合を作ればすべての世界を生成できる｛a, b, c｝の直積を作ったのと同じ可能な世界の数は29 =512通り

図 2 すべての関係を作り出す

リスト 1 世界を生成するプログラム
public allRelation : nat1 ==> set of seq of set of nat1
allRelation(k) ==世界における人数をk で指定する(
dcl rlst : set of seq of set of nat1 := {};dcl lst : seq of set of nat1;
dcl mapping : set of seq of nat1 := dunion { {[i,j] | j in set {1,...,k}} | i in set {1,...,k}};for all m in set power mapping do(lst := [ { } | i in set {1,...,k} & i > 0 ];for all a in set m dolst(a(1)) := lst(a(1)) union {a(2)};rlst := rlst union {lst});return rlst);

リスト 2 Q（x，y）全数テスト-- ∀ x ∃ y(Q(x,y) => Q(y,x))
public P22 : () ==> bool
P22() == return forall x in set elems model &(exists y in set elems model & (x.Q(y) => y.Q(x)) );public alltest22 : nat1 ==> seq of boolalltest22(k) ==(dcl ans : seq of bool := [];setM(k);for all lst in set allRelation(k) do(setRelation(lst);
ans := ans ^ [P22()];);
return ans;);

も，int のビット長が制約になるし，処理が複雑になるので，連載の主旨からいえばそのプログラムが正しいことを証明しなければならない．そうすると話が長くなるので，3 人の世界だけでがまんすることにする．数が多くなってしまうのは，モデル検査などの全数検査を行う手法の宿命である．

● 夏目漱石の例
コンピュータを使っていると一見，頭を使っているようだが，実は力業に頼って安直な方向に走っているのではないだろうか．
夏目漱石の場合は，3 人の世界を図 4 に示した六つの世界にまとめている．これで，「こころ」とか「三四郎」で利用する人間関係を推こうしていたのかもしれない．実は，a，b，c を区別せ>> create m1:= new QxyTest()>> print m1.alltest22(2)[ true,true,true, …,true ]論理モデル・クラスのサブクラスにした>> print m1.alltest22(3)[ true,true,true, …,true ]ここはすべてtrueになった．
ただし，3のときは30秒程度の計算時間がかかる>> print m1.alltest22(4)
C:/…/VDM/論理モデル.vpp, l. 38, c. 25:
Run-Time Error 79: Set too big for 'power'- limit is 16
4人の世界は，要素数が4×4=16個のベキ集合を作れず，実験できなかった．limit is 16だが，16はだめなのか?

ずに純粋に関係だけに着目して分類するとこうなる．グラフの同型という性質を利用して分類するのである．今考えている論

図 3 実行結果の一部

理式のテストでは，a，b，c を区別する必要はない．そのため，Dec. 2006

177