ヒビルテ(2013-03)

2013-03-15 [長年日記]

λ. TAPLの日本語訳出版します

すっかり書きそびれていたのですが、Benjamin C. Pierce の Types and Programming Languages (TAPL) の翻訳(共訳)をここしばらくしていたのですが、それがようやくこの3月に出版されることになりました。

しかもトークイベントなるものがあるので、何を喋るのか謎だけれど(^^;、興味のある方がいましたら、是非ご参加ください。

『型システム入門プログラミング言語と型の理論』ジュンク堂池袋店トークイベントのお知らせ - オーム社開発部

記憶が正しければ、原著について知ったのは、出版されたときに Benjamin C. Pierce のメールを向井先生に見せてもらって知ったのだったと思う。当時はまさかそれを自分が翻訳することになるとは思っておらず、今更ながら驚いている*1。

ただ、当時はTAPLについて特に興味を持つこともなかったし、その後、型理論系の論文を読むようになった後も、何かの機会に買ってはみたものの、結局積読になってしまっていた。TAPLに書いてあるようなことはある程度は知っているつもりだったので、あまり読む必要性を感じていなかったというのもある。が、今回自分たちで翻訳してみて、これはすごく勿体ないことをしてたなぁ、と思った。今となっては当然知っていることが多いのだけれど、知っていることについてもすごくしっかり書いてあるし、知らないこともそれなりにあった。 TAPL一冊読めば相当力が付くだろうし、TAPLを読まずにいたことで、昔の自分はずいぶん遠回りをしていたなぁと。

Tags: 型理論

*1 原著は2002年2月の出版だから、当時の自分は学部1年だったわけで、それから10年以上経っていると思うと、ずいぶん遠くまで来たなぁと思う。

[ツッコミを入れる]

2013-03-27 [長年日記]

λ. 「異様に難しいドラクエの謎解き」をモデル検査器で解く

人生を振り返る - 異様に難しいドラクエの謎解きより:

ドラクエ７のバロックの塔 (バロックタワー) の謎解き (ギミック) が異様に難しい。一応自力で解いてみたけど、手数が結構掛かってしまったので、最適なパターンが無いのか気になった。

この手の問題は、昔書いた「油売り算」と同じで、モデル検査器(Model Checker)を使うと簡単に解ける。

モデル検査器というのは何かというと、並行システムとかのような複雑な状態遷移を持つようなシステムに対して、エラー状態に到達しないだとか、デッドロックしないだとかの性質を検証するツールで、逆にそういうことが起こりうる場合には、それに至る状態遷移列を「反例」としして出力するような機能を持っている。そこで、この手の問題の場合、状態と可能な手からなる状態遷移系を考えて、ゴールとなるような状態を「エラー」として、モデル検査器にかけてあげると、ゴールに至る状態遷移列が「反例」として得られる。

ということで、モデル検査器SPINを使って6手が最短であることを確認してみる。まず、以下が検査用の状態遷移系の記述(BaroqueTower.pml)。非決定的に状態遷移を繰り返し、目的の状態になったら表明違反を発生させるように書いておくのがポイント。

/* 0:左の像, 1:上の像, 2:右の像, 3:下の像 */
byte dir[4]

/* 像を時計回りに90度回転させる */
inline rotate(n)
{
  dir[n] = (dir[n] + 1) % 4
}

/* 石から反時計回りに3つの像を回転させる */
/* 0:左上の石, 1:右上の石, 2:右下の石, 3:左下石 */
inline push_button(idx)
{
  atomic{
    rotate(idx)
    rotate((idx+3) % 4)
    rotate((idx+2) % 4)
  }
}

active proctype main()
{
  atomic {
    dir[0] = 3; /* 左の像 */
    dir[1] = 3; /* 上の像 */
    dir[2] = 0; /* 右の像 */
    dir[3] = 0; /* 下の像 */
    printf("[%d,%d,%d,%d]\n", dir[0], dir[1], dir[2], dir[3]);
  }

  /* 非決定的に色々試す */
  do
  :: atomic {
       int k;
       if
       :: true -> k = 0
       :: true -> k = 1
       :: true -> k = 2
       :: true -> k = 3
       fi;
       push_button(k);
       printf("%d -> [%d,%d,%d,%d]\n", k, dir[0], dir[1], dir[2], dir[3]);
     }

     /* 解けたら表明違反が発生するように */
     assert(! (!dir[0] && !dir[1] && !dir[2] && !dir[3]) );
  od
}

これを元に検査器を生成してコンパイルする。

% spin -a BaroqueTower.pml
% gcc -O2 -DREACH -o pan pan.c

こうして生成された検査器には「-i search for shortest path to error」というオプションがあるので、「pan -i」としてエラーに至る最短パスを探させる。結果は BaroqueTower.pml.trail というファイルに書き込まれる。

% pan -i

得られたパスの情報を元にシミュレーションさせる。

% spin -k BaroqueTower.pml.trail BaroqueTower.pml
      [3,3,0,0]
      1 -> [0,0,0,1]
      1 -> [1,1,0,2]
      2 -> [2,2,1,2]
      2 -> [3,3,2,2]
      3 -> [3,0,3,3]
      0 -> [0,0,0,0]
spin: BaroqueTower.pml:46, Error: assertion violated
spin: text of failed assertion: assert(!((((!(dir[0])&&!(dir[1]))&&!(dir[2]))&&!(dir[3]))))
spin: trail ends after 37 steps
#processes: 1
		dir[0] = 0
		dir[1] = 0
		dir[2] = 0
		dir[3] = 0
 37:	proc  0 (main) BaroqueTower.pml:32 (state 29)
1 process created

ということで、最短パス(の一つ)は「右上→右上→右下→右下→左下→左上」(1,1,2,2,3,0)で、6手未満のパスはないことが確認できる。

まあ、これくらいの規模の問題なら、モデル検査器を使わずに、自分で適当にプログラムを書いて状態遷移系を探索しても、大したことはないけれど。