日々の流転

λ. Traced Premonoidal Categories - Nick Benton and Martin Hyland

スライド

メモ。 Haskell の Arrows でいう ArrowLoop クラスが、traced premonoidal category に相当する。premonoidal category 一般については Premonoidal categories and notions of computation を見よ。

λ. キチガイ将棋戦法

http://d.hatena.ne.jp/yaneurao/20050328#p1 より。

面白すぎ。将棋はしばらくやってないけど、またやりたいなぁ。

λ. unboxed 1-tuple makes sense

<URL:http://article.gmane.org/gmane.comp.lang.haskell.prime/1022> で、こんなことが書かれてあるのを見かけて驚いた。

　

Mmm, not quite. Unboxed tuples are boxed tuples restricted such that they never have to be stored on the heap, but this has no effect on semantics at all. A function returning (# Double,Double #) may still return two thunks.

Yes, this is why the unboxed 1-tuple makes sense :-)

indexArray# :: Array# a -> Int# -> (# a #)

最初、どういう意味があるのかサッパリわからなかったが、<URL:http://www.haskell.org/ghc/docs/5.00/set/primitives.html> の説明を見て、なんとなく理解できた。

Something a bit more interesting goes on when indexing arrays of boxed objects, because the result is simply the boxed object. So presumably it should be entered—we never usually return an unevaluated object! This is a pain: primitive ops aren't supposed to do complicated things like enter objects. The current solution is to return a single element unboxed tuple (see Section 7.2.2).

indexArray#       :: Array# elt -> Int# -> (# elt #)

λ. Unboxed types have kind #.

GHC では unboxed type は # という種(kind)に属していることを偶然知った。<URL:http://www.haskell.org/haskellwiki/Unboxed_type> には表題の「Unboxed types have kind #.」と書いてある。普通の型と扱いを変えるには種を変えてしまうのが確かに一番自然か。

Prelude> :set -fglasgow-exts
Prelude> :kind (# Int, Int #)
(# Int, Int #) :: (#)
Prelude> :module +GHC.Base
Prelude GHC.Base> :kind Int#
Int# :: #
Prelude GHC.Base> :kind Double#
Double# :: #

もっとも、ソースコードに「forall (a:: #). a -> a」みたいな型を書こうとするとパースエラーになってしまう。unboxed type は多相的なものではないのでエラーになるのは当然だが、パースエラーとは酷いwww

Prelude> :kind (forall (a :: *). a -> a)
(forall (a :: *). a -> a) :: *
Prelude> :kind (forall (a :: #). a -> a)
<interactive>:1:14: parse error on input `#)'
Prelude> :kind (forall (a :: # ). a -> a)
<interactive>:1:14: parse error on input `#'

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

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

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

この手の問題は、昔書いた「油売り算」と同じで、モデル検査器(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手未満のパスはないことが確認できる。

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

参考図書など