日々の流転

λ. Re: 超べきとTransitive collapse

わかりやすい解説ありがとうございます。 detailは理解できてませんが、イメージはすごく良くわかります。

解説を読んで、最初は超冪というのは V^κ のように値域がクラスになっているような関数空間のことかと思ったのですが、<URL:http://en.wikipedia.org/wiki/Ultrapower> をみると、ウルトラフィルタによる同値類のことなのですね。

λ. コメントスパム

久しぶりにコメントスパム喰らった。スパマは死ね。

tDiaryをバージョンアップしてスパムフィルタを導入したほうがよいのかなぁ……

【2006-07-06追記】 tDiary 2.1.4 にあげて、とりあえずURLを大量に含むコメントをスパム扱いにした。

λ. 数学の表現の媒体としてのコンピュータ

• <URL:http://homepage3.nifty.com/mogami/diary/d0606.html#26t1>
• <URL:http://homepage3.nifty.com/mogami/diary/d0606.html#29t1>

メモ色々。 (書きかけ)

数学の難しさ

<URL:http://homepage3.nifty.com/mogami/diary/d0606.html#26t2>

「数学を理解する事は難しいと思っている人もいるかも知れないが、難しいのは省略された暗黙の前提や、説明されていない記号法や演繹則を知らないということに過ぎない。」というのは本当にそうなんだろうか。例えば、ベクトルや行列に関する前提・記号法・演繹側を理解すれば線形代数の証明は追えるようになる。しかし、いくら証明を追えたとしても例えば『プログラミングのための線形代数』で解説されているようなイメージを持てなければ線形代数を理解したとは言えないように思える。また、そのようなイメージを持つまでの過程において、記号法や演繹則を理解することがそれほど大きな割合を占めているとは思えない。そもそも数学を理解するということはどういうことだろう？

それから、「上記のようなシステムによって全ての細部を記述できるようになれば、数学の証明を理解する事は将棋の棋譜から対局を再現するのと同じ程度に易しいことになるだろう。」というのには同意できない。将棋の棋譜はシーケンシャルなものなのに対して、数学の証明はより複雑な構造を持っている。形式的証明に似ているのは計算機のプログラムで、プログラムには全ての細部が記述されているが、複雑なプログラムを理解するのは将棋の棋譜から対局を再現することよりもはるかに難しい。

定理証明系

既に指摘があるが、CoqやAgdaのような定理証明系は「人間が能動的に証明する。機械は正しく無いまたは不明な部分を消極的に指摘する」という考えに基づいてはいると思う。Tactics等によってある程度自動的に証明を探索することは出来るが、あくまで人間が証明することの補助に過ぎないと思うし。

シンデレラ

ところで、平面幾何ソフト「シンデレラ」というものもあり、こいつの上で平面幾何を考えるのは結構快適。こいつは記号論理に基づいた検証ではなく、自由に動かせる要素をランダムに動かしてテストすることを繰り返すことによって検証を行っている。検証方法はQuickCheckみたいなもんだな。

λ. Evans のvague object について　矢田部俊介　稲岡大志

というスライドを読んだ。 非外延的な集合論かぁ……

【2006-07-14追記】 ytbさんによる背景説明、非外延的集合論について。

λ. 『Fermat's Last Theorem』 Simon Singh

を読み終わった。 次は何を読もうか。 お勧めの洋書の紹介きぼんぬ。

λ. 知識発見法

• ナイーブベイズとベイジアンネットワーク
• 意思決定ネットワーク
• 情報量基準
  • 最小記述長原理
  • AIC (Akaike's Information Criterion, 赤池情報量規準)

情報量基準の話はいまだによくわかんない orz

λ. 人身事故

帰りの電車が人身事故で待たされる。 イライラする一方で、その人はどんな人だったのかと思う。

λ. 蟻

λ. めがまり

良く出来てるなぁ。懐かしい。とりあえず、咲夜・うどんげ・チルノ・霊夢をこの順で倒した。キャラ二人分のライフゲージがあるせいか、ボス戦はそこまで辛くない。といっても、元のロックマン2をもう覚えてないんだけどね。技は、咲夜とチルノの技は魔理沙に、うどんげと霊夢の技はアリスに持たせた。そういえば、ロックマンのボスといえば弱点があるのがお約束のはずだけど、まだ弱点には出会ってない気がする。はて?

パスワードのメモ

●　　　　
　　　●●
●　●　　
●　　　●
●●●●　

λ. 余代数と余帰納法

2006-06-24で「coalgebra等の簡単な解説は近いうちに書こうと思います」と書いたが、このままだといつになっても書けそうにないので、とりあえず書き始めてみる。ちょっとずつ書き足していく予定。

代数と余代数

余代数は代数の双対……といっても何が何だかわかんないと思うので、まずは代数を考える。

代数は集合と演算と演算の満たす規則から構成される。例えば群。集合Gは、演算「e: G」「*: G×G->G」「_^-1: G->G」を持っていて、規則「(a*b)*c = a*(b*c)」「e*x = x」「a^-1*a = e」を満たすとき、群と呼ばれる。同様に集合Lは、演算「⊥: L」「∨: L×L→L」を持っていて、規則「a∨b = b∨a」「a∨(b∨c) = (a∨b)∨c」「a∨a = a」「a∨⊥ = a」を満たすとき、上半束と呼ばれる。これらを見ると、代数では演算はすべて値域がその集合になっていることがわかる(「演算に関して閉じている」という言い方をしたりする)。

圏論では関数の向きを逆向きにすることで双対を考えるので、値域ではなく定義域がその集合になっているような演算を集合に加えることが考えられる。これが余代数。

例) Kripkeモデル

Kripkeモデルは、ノードないしは「世界」の集合 W に、以下の二つの演算を加えた余代数と考えることが出来る。

• 各ノードからの到達可能性を定める関数 W -> ℘(W) と
• 各ノードで成り立つ原子命題の集合を定める関数 W -> ℘(A)

例) オートマトン

言語理論では言語の識別機械としてオートマトンが使われるが、Σをアルファベットの集合とすると、このオートマトンは集合 S に以下の二つの演算を加えた余代数と考えることが出来る。まあ、実際には初期状態も必要なので、この余代数自体ではなく、この余代数の要素をオートマトンと呼ぶべきかも。

• 文字を受け取って状態遷移するための関数 trans: S -> S^Σ
• 受理状態かを判断する関数 accept: S -> Bool

非決定性オートマトンにしたければ、trans: S -> S^Σ を trans: S -> ℘(S)^Σ にすれば良いし、さらにε遷移を許したければ ε: S -> ℘(S) という演算を加えればよい。

例) オートマトン (2)

後で使いたいので、もうちょっと単純なオートマトンも考えておく。 数字(自然数)を表示するディスプレイとボタン一つだけからなり、ボタンを押すと表示されている数字が切り替わるような、そんな機械があったとする。そうすると、この機械は状態の集合Sに以下の二つの演算を加えた余代数としてモデル化できる。

• 現在の数字を得る関数 value: S -> N
• ボタンを押したときに次の状態に遷移する関数 next: S -> S

始代数

余代数の例を幾つか紹介したところで話を代数に戻す。 また唐突だが、自然数全体の集合は、集合Nに以下の二つの演算を加えた代数と考えることが出来る。

• 0: N
• s: N->N

同じ種類の代数 (X, c:X, f:X->X) は他にいくらでも考えることが出来るけど、この (N,0,s) はその中でも「全ての要素が 0 と s の有限回の適用で一意に表記できる」という良い性質を持っている。これは直観的には「潰れていない(0 = s(n) が成り立ったりしない)」ことと「(0とsで表記できない)余計な要素を含んでいない」ことを意味している。

この性質があると嬉しいのは、再帰によって関数を定義することが出来、また(構造)帰納法による証明が出来る点。例えば、以下のような等式を満たす関数は唯一つするので、これによって関数hを定義することが出来る。

• h(0) = c
• h(s(n)) = f(h(n))

この等式を良く見ると、cを集合Xの要素、fをX->Xの関数として、この関数hは実は (N,0,s) から (X,c,f) への準同型になっている。圏論ではこのような「同じ種類の代数への準同型が一意に存在するような代数」のことを始代数(initial algebra)と呼ぶ。

(後で: 帰納法についても書く)

始代数の特徴とはある種の等式の集まりによって関数を定義することが出来、これはつまり「同じ種類の任意の代数への準同型が一意に存在する」ということだった。

(続く)

終余代数 (final coalgebra)

「同じ種類の任意の代数への準同型が一意に存在する」の双対を考えると、「同じ種類の任意の余代数からの準同型が一意に存在する」になる。 なんで、そんなものを考えるか。例えば、上の「オートマトン(2)」で考えた余代数だと、ある状態 s∈S から next を繰り返し適用していって表示される数字を集めると、value(s), value(next(s)), value(next(next(s)), ... という数列が出来るが、以下の二つの点から扱いにくい。

• 異なる s1,s2∈S が同じ数列を生成することがあるかもしれない。この機械を観察することでわかるのは結果の数列だけなので、観察から区別できないような状態が存在することがある。つまり、状態空間が冗長かも知れない。
• また、全ての数列が生成出来るとは限らない。つまり状態が足らないかも知れない。

これらの問題がない、ある意味理想的な余代数が終余代数(final coalgebra)で……

(続く)

λ. めがまり (2)

妖夢・幽々子・レミリア・永琳の順で倒して、 妖夢とレミリアの技は魔理沙に、幽々子と永琳の技はアリスに持たせた。 まだボスの弱点は良くわかってない。で、パチュリーステージなわけだが、紫戦でどうしても途中で落ちちゃうよ……

パスワード

●　　　
  ●　●
●　●　
●　●　
  　●●

λ. 『黒衣の下の欲望』 マルト・ブロー(Marthe Blau)著, 長島良三　堀内一郎　訳

を読んだ。 原題は『Entre Ses mains』。

λ. 面接

に行ってきた。

I took employment eligibility exam which consists of an English examination, a short essay and an interview. I was a bit nervous but I think I did well.

λ. 『ファウンデーションの彼方へ (上)』

を読んだ。

λ. 第十八回圏論勉強会

今日は圏論勉強会だった。写真。

I attended the seminar of category theory. Although it began at 8:45, I slept in till noon. Actually I had woke up at eight but then I got back to sleep...orz. Anyway I arrived at past 2:00.

Today's first topic was diagonal arguments. Cantor's diagonal arguments were generalized to Lawvere's diagonal theorem which is also called Lawvere's fixpoint theorem. The theorem is related to the works of Russel, Gödel and Tarski. The theorem was very interesting but we couldn't understand Lawvere's arguments about ‘idealization’. The next topic was map objects (expontiation). In exercises we had to prove certain isomorphisms like Y^T×S≅(Y^T)^S. The calculation was tiresome, but we could prove them by using the uniqueness property of map objects.

After the seminar we went to さくら水産.

λ. 『英語で日記を書いてみる』 石原真弓

という本を最近買ってみたので、日記の一部を英語で書いてみることにした。下手な英語を晒すのは恥ずかしいけど、これで少しは上達するといいなぁ。

λ. Rubyist SNS

参加してみた。OpenPNEってこんな感じなのね。

• <URL:http://jp.rubyist.net/sns/?m=pc&a=page_f_home&target_c_member_id=115>

λ. アーサー空白の１５年間を語る

うはwww　カプコン最高です。(あろはさんのmixi日記より)

λ. めがまり (3)

幽々子ステージを何度かプレイし、E缶を四個収集した。

紫を倒せた。やっぱ、時間がかかるとそれだけ落ちる機会も増えるので瞬殺するのが良い。まず、開始直後にフォースクライシスを三発当てて三分の一くらい削る。藍と橙はリンカネーションゴーストを使いつつ相手の位置に応じてメンタルサクリファイスと紅色マジックも使い瞬殺。紫が姿を現したら紅色マジックとリンカネーションゴーストとメンタルサクリファイスを同時に使って一気にダメージを与える。本当はフォースクライシスをもっと活用できるといいんだけどね……

萃香はだいぶ楽。小さい萃香が集まって大きな萃香になった瞬間に紅色マジックを発射し、即座にリンカネーションゴーストに切り替えて発動しながら接近。

マリサランド版魔理沙は苦手。紅色マジックで速攻でダメージを与える。八頭身になった後は更に苦手。落ちてくるブロックがどうしても避けられないときがあるし、マスタースパークと突進の判断が遅れて避けるのに失敗することもあり。E缶を一個使ってしまう。

四季映姫ステージは、変な乗り物にのったウサギが上から降りてくるところが苦手。ボスにたどり着くまでに結構ダメージを受けてしまう。四季映姫は上から降ってくる塔婆(?)を見落として大ダメージを受けてしまいがち。通常ショットとメンタルサクリファイスである程度ダメージを与えたら、あとは上海人形まかせ。またE缶を一個使ってしまう。

お次はお約束のボスラッシュだが、ボスの弱点をまだ良くわかっていないので、あっさり撃沈。しょぼーん。

E缶四個のパスワード

　　　　●
　●●　　
●　●　●
　●　　●
　●　　　

λ. 非外延的集合論

<URL:http://d.hatena.ne.jp/ytb/20060702/p1>

ビックリさせてしまって済みません。非外延的集合論は存在自体は知っていましたが、こんなところに役に立つのか、というのが新鮮でした。

λ. キミならどう書く 2.0 - ROUND 2 -

与えられた範囲の中でCollatz予想の収束までのステップ数が最大となる値を求める問題。とりあえず、Haskellで超素朴なコードで試してみたら「h 1000000」に40秒くらいかかった。

import List

g 1 = 1
g n = 1 + g (if even n then n `div` 2 else 3*n + 1)

h n = fst $ maximumBy c [(k, g k) | k <- [1..n]]
    where c (_,x) (_,y) = x `compare` y 

実行結果。

Main> h 100
97
Main> h 1000000
837799

以下のようにして100000までの値をテーブル化すると7秒まで縮んだ。 更に効率化するにはどうすれば良いだろう?

import List
import Array

tableMax = 100000  
table = array (1, tableMax) [(k, g' k) | k <- [1..tableMax]]

g n = if n <= tableMax then table ! n else g' n

g' 1 = 1
g' n = 1 + g (if even n then n `div` 2 else 3*n + 1)

h n = fst $ maximumBy c [(k, g k) | k <- [1..n]]
    where c (_,x) (_,y) = x `compare` y

λ. めがまり (4)

めがまりをクリアした。

ボスラッシュに苦戦するうちにボスの弱点がわかってきたので、ボスラッシュは弱点の技で適当に倒す。が、妖夢とレミリアが依然として苦手。生身のパチュリーはサウザンドナイブズで華麗にスルー。パチュリーマシンはフォースクライシスと紅色マジックでたこ殴り。クリアはできたけど、もうE缶残ってないよ。

もう余力が無かったので、最終ステージではあっさりゲームオーバーに。コンティニュー。小悪魔はパターンが簡単なので慣れれば楽勝。パチュリーカプセルはどの攻撃を撃ってくるのかが判別できずにダメージを受けてしまうのが嫌。パチュリーカプセルがかなり上の位置に現れた場合にはホーミングアミュレットで攻撃し、 自機のすぐ上に現れたときにはゴーストカッターでザクザク斬る。ラストのメカパチュリーは例によってフォースクライシスと紅色マジックで攻撃。攻撃はそれなりに激しいが、ある程度ダメージを与えたあとは、エネルギーを溜めての体当たり(?)が多くなり、これは魔法の箒を使えば比較的簡単にかわせるので結構楽。最終ステージはE缶まったく無しでクリア。

クリア後、攻略サイトを眺めていて、M缶やS缶の存在、それから四季映姫ステージのショートカットとかを知って、結構ショック。次の目標はノーコンティニュークリア?

λ. 「モデル検証技術の応用」

千葉商科大学政策情報学部の大矢野潤氏の講演「モデル検証技術の応用」を聴いてきた。モデル検証(model checking, モデル検査)について色々と面白い話を聴くことが出来た。Lightweight Verification という言葉が少し印象に残っている。

λ. Re: Collatz予想

無限リストでメモ化すること自体は考えたのですが、私の考えたのは再帰呼び出し毎に(!!)を使って値を取り出すもので、かなり遅かったために書きませんでした。稲葉さんのコードは面白いですね。ただ、私ならこう書くかな。

-- まったくもってこれ以上ないくらいごくごく普通の何の変哲もないinterleave
(/\/) :: [a] -> [a] -> [a]
(x:xs) /\/ ys = x : (ys /\/ xs)
[] /\/ ys     = ys

-- g!!n == 自然数(n+1)が収束するまでのステップ数
g :: [Int]
g = 1 : map (+1) (g /\/ map head (iterate (drop 6) (drop 9 g)))

-- h!!n == [1..n+1] の中で一番収束にかかるステップ数がでかいの
h :: [Int]
h = map fst $ scanl1 phi (zip [1..] g)
    where phi a@(_,gk) b@(_,gk')
              | gk' > gk  = b
              | otherwise = a

main = print h

追記

そっか、タプルの順番を入れ替えれば、scanl1に渡す関数は単にmaxで良いのか……気づかなかった。

2006-09-14 追記: 顔文字に見える件について

中置演算子を普通の関数として書くためには括弧で囲う必要があるので、こんなことになってます。しかし、まあ顔文字には見えますよね。特にこんなのとか。

Main> :t (^^)
(^^) :: (Integral b, Fractional a) => a -> b -> a
Main> 2 ^^ (-1)
0.5

λ. 『θは遊んでくれたよ』 森博嗣

を読んだ。トリックは予想通りだが、犯人の特定が少し面白かった。しかし、もはやキャラ萌え小説だよなぁ。キャラクタや先の展開が気になるから読むけど、単体で楽しむには辛くなってきたように思う。

Quotation

物理的な証拠が、仮説を少しずつ揺るぎないものにしていくだろう。事実とはこうして後から形成されるものだ。しかし、人の心の中の、その時々の葛藤かっとう)は、二度と正確に再現されることはない。たとえ、本人の口が語ったとしても、その言葉は明らかに虚構である。理由も動機もすべて、光が当てられたときに現れる影に過ぎない。光の当て方によっては、影はどちらにも現れ、形の歪ひず)み方も変わり、幾つもが同時に現れることさえある。

λ. Alephの振る舞いがわからない。

適当な背景知識と正例と負例を食わせたところ以下のようなルールを学習してくれた。Rule 1 と Rule 3 さえあれば Rule 2 は実際には不要に思えるが、何故 Rule 2 が残っているのだろう。

[theory]

[Rule 1] [Pos cover = 3 Neg cover = 0]
append(A, B, B) :-
   A=[].

[Rule 2] [Pos cover = 3 Neg cover = 0]
append(A, B, C) :-
   A=[D|E], 
   C=[D|B], 
   append(E, C, C).

[Rule 3] [Pos cover = 9 Neg cover = 0]
append(A, B, C) :-
   A=[D|E], 
   append(E, B, F), 
   C=[D|F].

背景知識

% append.b
:- mode(1,append(+list,+list,-list)).
:- mode(1,((+list) = ([-any|-list]))).
:- mode(1,((-list) = ([+any|+list]))).
:- mode(1,((+list) = ([]))).
:- mode(1,((-list) = ([]))).
:- set(i,3).
:- set(noise,0).
:- set(print,1).
:- determination(append/3,append/3).
:- determination(append/3,'='/2).

正例

% append.f
append([],[1,2,3],[1,2,3]).
append([1],[2,3],[1,2,3]).
append([1,2],[3],[1,2,3]).
append([1,2,3],[],[1,2,3]).
append([],[1,2,3,4],[1,2,3,4]).
append([1],[2,3,4],[1,2,3,4]).
append([1,2],[3,4],[1,2,3,4]).
append([1,2,3],[4],[1,2,3,4]).
append([1,2,3,4],[],[1,2,3,4]).
append([],[],[]).
append([1],[2],[1,2]).
append([2,3],[],[2,3]).

負例

% append.n
append([1],[],[]).
append([],[1],[]).
append([1,3,2],[],[1,2,3]).
append([],[1,3,2],[1,2,3]).
append([2,1],[3],[1,2,3]).
append([3,2],[1],[1,2,3]).
append([1,2],[3,4],[1,3,4]).
append([1],[2,3,4],[2,3,4]).
append([1,2,3],[4],[1,2,3]).

λ. Learning Minesweeper with Multirelational Learning. Lourdes Peña Castillo, Stefan Wrobel

を読んだ。ILPでマインスイーパーの推論規則を学習する話。

• <URL:http://citeseer.ist.psu.edu/570045.html>
• <URL:http://jp.citeulike.org/article/767959>

λ. 某F氏の机の本

トポスとかの本と、コーポレートファイナンスが並んでるのが素敵。

λ. 雑談メモ

• ホーン節に限定されない、一般のresolutionは色々難しい
  • ancestor resolution
  • factoring
  • Michael Genesereth
• Prolog based theorem proover
  • Mark E. Stickel
  • 対偶等を使ってPrologで扱える形に変換する前処理
  • 意味論の問題
  • 2008-03-27追記: SATCHMO等のことか?　⇒ SATCHMOで遊ぶ - ヒビルテ (2007-12-19)
  • 2008-05-25追記: いや、PTTP - Prolog Technology Theorem Proverのことか。
• model checking で幾何学の定理を証明?
• magic set
  • Magic sets and other strange ways to implement logic programs.
• magic set と chart parser ?
• Cocke-Younger-Kasami (CYK) algorithm
  • 2008-03-27追記: Haskellで書いてみた
• 『現代数理論理学入門』の強制法の解説はわかりやすいらしい

λ. 統計の本

某K氏に統計の本の紹介を頼んだら、この二冊を紹介された。 後で読みたい。

λ. 知識発見法レポート

先日読んだ Learning Minesweeper with Multirelational Learning に触発されて、数独で数字を埋めるための規則を学習させようとしてみたのだけど、残念ながらうまくいかなかった。

• 知識発見法レポート
• 背景知識 sudoku.b
• 正例 sudoku.f
• 負例 sudoku.n

λ. The Knaster-Tarski Theorem, Veronika Vaneková

タルスキの不動点定理の短くて分かり易い解説。

「A set operator is finitary iff it is chain-continuous」という部分が分からなかった。

(追記) finitary と set-continuity

set operator のこの finitary(有限特性) という性質の定義は class operator の set-continuous という性質の定義に似ている。

• set oprator τ: 2^X → 2^X が finitary なのは、τ(A) = ∪{τ(B) | B⊆A, B finite} を満たすとき。
• class operator τ が set-continuous なのは、τ(A) = ∪{τ(B) | B⊆A, B set} を満たすとき。

(追記) 最大不動点と余帰納的定義

ちなみに、このテキストでは帰納的な定義と最小不動点しか扱っていないが、双対を考えることにより、余帰納的な定義と最大不動点について同様のことが言える。Uを完備束、τ: U→U を単調な関数として、

• Ind(τ) = lfp(τ) = inf {A | A∈U, τ(A)≦A} = sup {τⁱ(⊥) | i∈Ord}
• Coind(τ) = gfp(τ) = sup {A | A∈U, A≦τ(A)} = inf {τⁱ(T) | i∈Ord}

λ. 『物理数学の直観的方法』 長沼 伸一郎

の、e^πi = -1 の説明のところだけ読んだ。 説明はまどろっこしいが、考え方は確かに分かり易い。

λ. 内定

先日某社から内々定の連絡がありました。これで就職活動は一応おしまいです。 お世話になった方々、応援していただいた方々、本当にありがとうございました。

λ. 『ふつうのHaskellプログラミング』読書会

I attended RHG*1 reading club and we read section 5, 6, 7 and 8.1〜8.3 of “ふつうのHaskellプログラミング”. We studied lazy evaluation, basic values, basic syntax, higher-order functions and anonymous functions. We had read to page 208.

英語の勉強にリーダーズ・ダイジェストという雑誌を教えてもらった。

BTW: ICFP Programming Contest had began and the subject seems interesting. I regret that I don't have time in this weekend.

λ. 『すべての日本人に感じてほしい魂の昭和史』 福田和也

を読んだ。 いい本だ。 中学生か高校生の時に読んでいたかったな。

Quotation

p.14

だから、歴史のもっとも大事なことは、共感ということだ。自分にとって関係のない出来事や固有名詞を覚えるということではない。あるいは他人ごととして、裁くことでもない。自分につながる、今、ここで生きている自分にとって他人事ではない事柄として、過去を振り返り、その実感のなかで、前の世代との絆を確認すること。そして、その絆のなかで、君たちの先人が、何をのぞみ、何をこころみ、そして成功したり、失敗したということを理解しようとこころみてほしい。そうすれば、君たちが生きている現代という時間が、けして薄っぺらなものでないことがわかるだろう。

p.97

絶対にとりかえしのつかないことの積み重ねが「歴史」ということなんだから。そして君たちは、みんな、その積み重ねの結果としてここにいる。

λ. 第十九回圏論勉強会

うげ、俺も腹痛い……。 会場には行ったが、人数が少なかったので、自習していた。

λ. 『陰陽ノ京〈巻の3〉』 渡瀬 草一郎

を読んだ。

Quotation

p.275-276より。

あるいは——もっと他の糸が、何処か自分たちの与り知らぬ所で、絡み合っていたのかもしれない。しかし、その糸がまるで見えぬために、この問いに対する答えを人は持つことが出来ない。(中略) それら全ての糸が、保胤にはもちろん、誰にも見えてはいない。人にとっての自然とは、そうしたものである。まるでわからないものといっても過言ではない。

λ. MAD PEOPLE β01

ちょー楽しそう。 人狼の初期のころを思い出すな。

人狼と違い市民側に能力者がなく、全員が攻撃結果から情報を得られるのが良い。CO方法とかに関する不毛な議論をする必要がないし、能力者の力量によって大きな影響を受けることもないし。ただ、情報が多いのでエイリアン側は辻褄を合わせるのが大変そうだ。

• 非公式Wiki
• mixi:MAD PEOPLE

λ. 『ファウンデーションの彼方へ〈下〉』 アイザック・アシモフ

を読んだ。 結構面白かったが、ロボット三原則とか出てきて萎えた。 俺には向いてないっぽい。

λ. 欧州で短期村に初参加

hatoさんが企画した欧州の短期村に参加してきた。いやー、短期はむずいね。二回とも寡黙吊りっぽい感じで吊られてしまった。

• 人狼@欧州 252村 皆で短期に慣れる村
• 人狼@欧州 255村 続・皆で短期に慣れる村
• 関連
  • 狼）欧州短期をしませんか (hatoさん)
  • 狼）欧州短期建てます。 (hatoさん)
  • 狼）はじめてのおうしゅう (hatoさん)

λ. 『イリアと魔法の図書館』 木島 麻貴

を読んだ。 図書館を舞台にしたファンタジーということとあと表紙に惹かれて手にとった本。ご都合主義な気がするが、子供向けのファンタジーだとこんなものなのかも。

λ. 各要素が「0または1をとる乱数」から成る長さnのリスト

勝手にどう書く0.0 より。あまり興味を惹かれるお題ではないけど、一応。

Prelude> :module +Random
Prelude Random> :module +Monad
Prelude Random Monad> xs <- liftM (take 10 . randomRs (0,1)) newStdGen
Prelude Random Monad> xs
[1,0,0,1,1,0,1,1,0,1]

λ. アルゴリズム勉強会

Some members of our research group are thinking that we need to study and improve our knowledge of computer science, as we sometimes feels lacks of basic knowledge. So we have been planning to held seminar to study algorithms in the upcoming summer vacation. Today we had the first offline meeting and chose which text to use. My opinion was to use lecture notes of Advanced Algorithms Course at MIT. But we decided to use D.Knuth's famous book “The Art of Computer Programming Volume 3: Sorting and Searching” (Japanese Edition). I was slightly unpleasant since I don't like Knuth :-P

• アルゴリズム勉強会2006 (access limited)

λ. Happy SAAD!

I heard that today is System Administrator Appreciation Day, also known as Sysadmin Day or SAAD. See <URL:http://en.wikipedia.org/wiki/System_Administrator_Appreciation_Day> for details. But who knows this day?

λ. 『4日で学ぶモデル検査』

すこし前のkmt-tさんの日記で知って生協で注文していたのを受け取った。 時相論理についての基本的な知識はあると思うので、ツールの使い方やモデル化のノウハウを知るために読むつもり。パラパラ見た感じでは中身は想像していたよりずいぶん簡単そう。読むだけならすぐ読み終わりそうだけど、後でSPINとNuSMVをインストールしてから読む。

読書記録

• 1日目
• 2日目
• 3日目
• 4日目

関連URL

• <URL:http://www.nts-book.co.jp/item/detail/summary/it/20060608_4.html>
• <URL:http://d.hatena.ne.jp/kmt-t/20060729#1154176023>

λ. Fibonacci Heaps

MIT の Advanced Algorithms, Fall 2005 の第一回の資料 Fibonacci Heaps を読んだ。二項ヒープ(Binomial Heap)は知っていたがフィボナッチヒープ(Fibonacci Heap)は知らなかったよ……

メモ

• Fibonacci heap - Wikipedia
• Soft Heap - Radium Software Development

λ. 「主人がオオアリクイに殺されて1年が過ぎました」

「主人がオオアリクイに殺されて1年が過ぎました」というしょうもないSubjectのspamが来た。オオアリクイに殺されるって、それどんな出稼ぎwww　とにかくこれを書いた奴は凄い。

Subject: 主人がオオアリクイに殺されて1年が過ぎました。
From: 久光 <original_day_sunday@yahoo.co.jp>
X-Mailer: Becky! ver. 2.22.02

いきなりのメール失礼します。
久光さやか、29歳の未亡人です。
お互いのニーズに合致しそうだと思い、連絡してみました。

自分のことを少し語ります。
昨年の夏、わけあって主人を亡くしました。
自分は…主人のことを…死ぬまで何も理解していなかったのが
とても悔やまれます。
主人はシンガポールに頻繁に旅行に向っていたのですが、
それは遊びの為の旅行ではなかったのです。
収入を得るために、私に内緒であんな危険な出稼ぎをしていたなんて。

一年が経過して、ようやく主人の死から立ち直ってきました。
ですが、お恥ずかしい話ですが、毎日の孤独な夜に、
身体の火照りが止まらなくなる時間も増えてきました。

主人の残した財産は莫大な額です。
つまり、謝礼は幾らでも出きますので、
私の性欲を満たして欲しいのです。

お返事を頂けましたら、もっと詳しい話をしたいと
考えています。連絡、待っていますね。

追記

檜山さんのところにも来ていたらしいし、結構話題になってたみたいだな。 <URL:http://d.hatena.ne.jp/m-hiyama/20060805/1154760809>

さらに追記

bogusnewsにオオアリクイ被害遺族に、ネットで支援の輪というニュースが出ていて、これも笑った。

λ. 4日で学ぶモデル検査: 1日目

「最初はSpinとNuSMVのいずれかのツールを使うことを選択し、使わないほうのツールに関する記述は読み飛ばすのが良い」といったことが書かれていたので、どちらを使うか考える。ざっと見た感じ、NuSMVの記述言語が非常に状態遷移系っぽい書き方をするのに対して、Spinの記述言語(Promera)はもっと普通の手続き言語っぽい感じの書き方をするというのが大きな違いのようだ。テキストはXSpinを使った記述がされているが、XSpinを使うためにTcl/Tkをインストールするのが面倒なので、とりあえずNuSMVの方を使うことにした。

それから、書いてある通りにやったらシステムαとランプ点灯の問題はすぐに出来た。今日の内容はまだ物足りないので、明日以降の内容に期待。

λ. Failed to buy Nintendo DS Lite.

I went to Tokyo to receive suits which I ordered the other day. On my way home, I went to Yodobashi-Camera in Akihabara to buy a Nintendo DS Lite. But it was already sold out. So I also checked Yodobashi-Camera in Yokohama. But it was sold out in there too. I was very disappointed and envied my friends who had Nintendo DS...

λ. Sheep と Lamb

「羊たちの沈黙」の原題は「The Silence Of The Lambs」で、「羊たち」と訳されていたのは Sheeps ではなく Lambs だったということに偶然気づいた。そういや、SheepとLambの違いって何だろうな、と思い検索したら、What's the difference between a sheep and a lamb? というページを見つけた。なるほど……

λ. 4日で学ぶモデル検査: 2日目

今日は2日目の内容をやる。

Mini Life Game

普通に何の問題も無く出来た。しかし、各変数についてのnextでほとんど同じことを何度も書かなくてはならないのが嫌だな。DEFINEで関数(というかパラメータを持つ定義)を定義することが出来れば良いのに。

ウサギちゃんとオオカミくん

値域全体に非決定的に遷移する変数RbSMとWoSMを乱数のように(?)使って他の変数を遷移させているのに、「へぇ」と思った。

最初にモデルと論理式をNuSMVに食わせたときに「specification !(rule U goal) is true」といきなり言われて焦ったが、単なる入力ミスで、それを直したら問題なくなった。それから、Splaceの初期状態としてbankAではなく0という状態を加えているのは何故だろう。以下のようにすれば状態0は不要に思えるが……

VAR
  RbSM : 0..2;
  WoSM : 0..2;
  Splace : {bankA, AtoB, bankB, BtoA};

ASSIGN
  init(RbSM) := {0,1,2};
  next(RbSM) := {0,1,2};

  init(WoSM) := {0,1,2};
  next(WoSM) := {0,1,2};

  init(Splace) := bankA;
  next(Splace) := case
                    Splace = bankA : AtoB;
                    Splace = AtoB  : bankB;
                    Splace = bankB : BtoA;
                    Splace = BtoA  : bankA;
                  esac;

並行システムと排他制御

runという{0,1}に非決定的に遷移する変数を使って二つのプロセスのスケジューリングを行っているのが面白い。Spinと比較すると、明示的なスケジューリングを行わなくてはいけないのは面倒くさいが、その分LTLや通常の状態遷移系のレベルでの理解が容易なのはメリットと言えるだろう。ただまあ、複雑な並行システムを扱うに向いてないだろうな*1。

モデルの記述ではnext(semaphore)の記述が誤っているように思う。「run = 1 & proc1_state = entering : 0;」は「run = 1 & proc1_state = exiting : 0;」の誤りだろうし、proc2についても同じ。それから、テキストの方ではproc1_stateがstate_p1と書かれていて、コードとテキストが合っていない。

それから、演習問題の解答例がNuSMV側だけ読んでいると唐突過ぎるように感じた。SPIN側では「あるプロセスがクリティカルセクションから出た瞬間にクリティカルセクションに入ることを繰り返す」ことが最後に問題になっていたのに対して、NuSMV側では「セマフォを獲得したまま、クリティカルセクションから出てこないプロセス」が問題になっていたので、いきなりこの解答が出てきても……

練習問題

後で書く。

λ. 軍医としての森鷗外

なんとはなしにWikipediaを眺めていて、「森鴎外」の項に以下のような記述をみつけ、「へぇ」と思った。笑い事ではないのだけど、もし中学生や高校生のころにこういったエピソードを知っていれば、単なるブンガクシャとしてではなく、その時代に生きた人間として興味を持つことが出来ただろうな、と思った。

脚気の伝染病説を主張し、のちに海軍軍医総監になる高木兼寛と対立した。あくまで自説に固執し日露戦争でも兵食に麦飯を給するのを拒んだ（自ら短編『妄想』で触れている）ため、陸軍が25万人もの脚気患者を出し、3万名近い兵士の命を犠牲にしたことに責任があるとされる（同時期、高木の指示で兵に麦飯を与えていた海軍では脚気患者は軽症者がわずかに発生したのみで、死者は無しと伝えられる）。「ロシアのどの将軍よりも多くの日本兵を殺した者」との批判すらある。

λ. 4日で学ぶモデル検査: 3日目

LTLについては既に知っているので、軽く読み、問題を解いた。 特に詰まる点は無し。昨日の練習問題は結構やりがいがあったのでちょっと拍子抜け。

λ. 研究会最終発表会など

研究室のadmin会議が朝あり、その後に研究会の最終発表会を聴いた。それから八田で打ち上げ。