日々の流転

λ. 研究会

tomcatのソースを交代で読むことに。16万行くらいあるらしいのだけど、一体何にそれだけの行数を使っているのだろう?

それから、Haskellの本を輪講しようという案も出したのだけど、予想通り却下された。うぐぅ。

λ. C言語

でも、実際には変数の使いたい範囲がオーバーラップしてたりすることも多いし、ブロックにすれば美しいというわけでも無いと思うのだけどなぁ…

λ. tomcat

……と思ったが、jakarta-tomcat-3.3.1を実際に見てみると、さすがに16万行はなくて、約5万行だった。ぱっと見た感じそう悪いコードではなさそうだし、意外と手ごろかも知れないけど、Javaはやはり好きになれないなぁ。

λ. ごはん

中村さんと豊田さんとスパゲッティ屋さんへ。

λ. 睡魔結界発動中

春眠暁を覚えずってね。

λ. お花見

に行ってきまつ。

今日の花見はRubyな人のお花見で場所は代々木公園。桜は流石に見事に咲いている。携帯の写真じゃあまり綺麗じゃないかも知れないけど、文字通り華があるね。桜の季節には日本に生まれてよかったと思う。

二次会では「川の長さは川の支点と終点の長さの何倍か?」といった話や、「自然対数の底 e の概念は如何にして発見されたのか?」といった話とか、ソフトウェア技術者の資格や免許といった話とか、ずいぶん色々な話題があったのを覚えている。ソフトウェア技術者の資格/免許の話は、つまるところソフトウェア技術者の労働力市場が典型的なレモン市場になっているということではないかと思った。

あと、超越数の話なんかもあった。超越数は無茶苦茶多い。なんたって、代数的数は可算個しかなくて、それ以外の実数は全部超越数だからね。にも関わらず、発見された超越数というのは非常に少なくて、このギャップがなんとも不思議だ。また、分数の概念を拡張すると、自然対数の底 e も(拡張された意味での)代数的数となってしまうという話も面白かった。そうすると、本当に超越してる数で我々の知っているのはπくらいしかなくなってしまうとか。

(2005-08-25 追記) 「臓器は血液を流れる栄養に関して競争関係にある」というような話が出ていたが、『生物の社会進化』 p.161-p.162 には次のようにあった。

血縁性は組織化のさまざまなレベルを区別する上でも決定的である．たとえば，私たちのからだの中の細胞に関して鍵を握る事実は，その遺伝的構成がすべて等しいことである．そのため，多細胞生物の進化の初期には，各細胞は自分の被るコストよりも繁殖細胞に与える利益の方が大きい場合には常に，繁殖を見合わせるように選択された．効率をよくする相互作用は全て促進されて，自らは繁殖を行わずに，繁殖を行う生殖細胞を助けて維持させる体細胞群が急速に発達した．すべての細胞の利害は完全に一致するので，特殊化は矛盾なく進化する．腎臓と肝臓とが血流中からどれだけの栄養分を取り上げるかをめぐって互いに対立するなどということはない．双方の臓器とも，より上位の単位の繁殖上の利益を最大にするだけの量の栄養を取得するように選択されてきている．

言及リンク

• Rogue Engineer's Diary / やさぐれ日記 (2005-04-09)

λ. 郵政民営化の議論に思う

そもそも民営化が何故効率化やサービス向上に繋がるかと言えば、民間には競争があり、インセンティブが存在するからだ。したがって、競争がなければ民営化したところで大した意味はない。民営化は魔法の薬ではないのだ。

が、過去の議論や現在行われている議論を見ると、「どうやれば競争的な市場に出来るか」という最も根本的な点ではなく、民営化後の事業の形態などの末端の話ばかりが注目されているように思う。全く茶番としか言いようがない。

λ. ノイズキャンセラ付ヘッドホンを買ってみた

これまで iPod nano で使っていた ATH-CK32 BK (20061018#p01) が壊れてしまった。左耳の方が断線しているっぽい。またカナル型のイヤホンを買おうかと思ったが、どうせなので今度はノイズキャンセラ付のヘッドホンを買ってみた。買ったのはSE-MJ7NSというやつ*1。

ちょっと使ってみた限りでは、やっぱりカナル型のイヤホンの方が良かったかも、と思った。

• 当然イヤホンよりも音質は良いし、ノイズキャンセラも結構良いが、私はPodcastで音楽以外を聴くのがメインなので、ちゃんと聴ければ音質はどうでも良い。カナル型イヤホンでも電車内で聴くのに困ることは無かった。
• イヤホンに比べて持ち運びにかさばる。
• 耳が暑苦しいので、これからの季節、長時間の着用が困難。

λ. 一からホモロジー ― 数学やってない人にも分かるホモロジー入門

を読んだ。 私は「ホモロジーでは図形の不変量を考える」という事だけは聞いた事があったが、具体的にどう考えるのか知らなかったので、面白かった。

λ. みんなの論文サイト Sesame!

「みんなの論文サイト Sesame!」というサイトを知った。CiteULikeに似ているけど、CiteULikeと違ってPubMedに特化したサービスみたい。 私は生命医学系の研究をしているわけではないので、今のところ関係ないか。 ただ、「公開レベルの設定」で「全公開」「グループ内公開」「非公開」が分けられるのはCiteULikeよりも便利そう。

Sesame(セサミ)は、元生物学系研究者がその研究経験を生かし『研究者にもっと研究に専念できる環境を！』というコンセプトに基に活動をしている団体です。

その中で、本HP「みんなの論文サイト Sesame!」は研究活動に欠かせない論文「情報収集→整理→共有」をらくらく快適にすることを目的に、研究者視点から開発した、研究者のための情報管理サイトです。2007年2月からサービスをスタートしています。

λ. PPL2008のカテゴリ1論文が公開

PPL2008のプログラムのページで、カテゴリ1の論文が公開されてました。 非常に面白い話が多かったので、参加されなかった方で興味のある方は見てみると良いのではないかと思います。 ちなみに、私のも載ってます(ぼそっ

あと、カテゴリ1の論文と出版済みのカテゴリ2の論文は私のCiteULikeのブックマークにも登録してあるので、CiteULike使っている人は、よかったらこちらもどうぞ。CiteULike: msakai ppl2008

λ. 強双対性を使って線形計画を制約充足問題に還元する

Linear and Discrete Optmization の双対性に関する部分(参考: 第五週目メモ)を復習していて気になったのだけど、強双対性の条件 c^T x^* = b^T y^* って線形式で書けてしまっているのよね。 ということは主問題と双対問題の制約条件と強双対性の連言をとっても線形(QF_LRA)の範囲に収まっていて、これの解(実行可能解)を求めれば、目的関数に関する最適化をしなくても最適解が求まることになるはず。 ということで試してみた。

主問題

簡単な問題として、Linear and Discrete Optmization で最初の例として使われていた、以下の例を考える。

MAXIMIZE 
  100 x1 + 125 x2
SUBJECT TO
  3 x1 + 6 x2 <= 30
  8 x1 + 4 x2 <= 44
BOUNDS
  0 <= x1 <= 5
  0 <= x2 <= 4
END

最適解は (x1,x2)=(4,3) で、目的関数値は775。

双対問題

この問題の双対問題は以下のようになる。

MINIMIZE
  30 y1 + 44 y2 + 5 y3 + 4 y4
SUBJECT TO
  3 y1 + 8 y2 + y3 >= 100
  6 y1 + 4 y2 + y4 >= 125
BOUNDS
  0 <= y1
  0 <= y2
  0 <= y3
  0 <= y4
END

最適解は (y1,y2,y3,y4) = (50/3, 25/4, 0, 0) で、目的関数値は775。

両方を合わせたもの

MAXIMIZE 
  0 x1
SUBJECT TO
  3 x1 + 6 x2 <= 30
  8 x1 + 4 x2 <= 44
  3 y1 + 8 y2 + y3 >= 100
  6 y1 + 4 y2 + y4 >= 125
  100 x1 + 125 x2 - 30 y1 - 44 y2 - 5 y3 - 4 y4 = 0
BOUNDS
  0 <= x1 <= 5
  0 <= x2 <= 4
  0 <= y1
  0 <= y2
  0 <= y3
  0 <= y4
END

(x1,x2,y1,y2,y3,y4) = (4, 3, 50/3, 25/4, 0, 0) はこの問題の(実行可能)解で、このときの目的関数値はどちらも775。

Z3の場合

最適化機能を持たない充足可能性ソルバの例として、SMTソルバのZ3で試してみる（オンラインでも Z3 online at RiSE4Fun で試せる）。

(declare-fun x1 () Real)
(declare-fun x2 () Real)
(define-fun obj-primal () Real
  (+ (* 100.0 x1) (* 125.0 x2)))
(assert (<= (+ (* 3.0 x1) (* 6.0 x2)) 30.0))
(assert (<= (+ (* 8.0 x1) (* 4.0 x2)) 44.0))
(assert (and (<= 0.0 x1) (<= x1 5.0)))
(assert (and (<= 0.0 x2) (<= x2 4.0)))

(declare-fun y1 () Real)
(declare-fun y2 () Real)
(declare-fun y3 () Real)
(declare-fun y4 () Real)
(define-fun obj-dual () Real
  (+ (* 30.0 y1) (* 44.0 y2) (* 5.0 y3) (* 4.0 y4)))
(assert (>= (+ (* 3.0 y1) (* 8.0 y2) y3) 100.0))
(assert (>= (+ (* 6.0 y1) (* 4.0 y2) y4) 125.0))
(assert (<= 0.0 y1))
(assert (<= 0.0 y2))
(assert (<= 0.0 y3))
(assert (<= 0.0 y4))

(assert (= obj-primal obj-dual))

(check-sat) ; => sat

(get-value (obj-primal x1 x2))
; => ((obj-primal 775.0) (x1 4.0) (x2 3.0))

(get-value (obj-dual y1 y2 y3 y4))
; => ((obj-dual 775.0) (y1 (/ 50.0 3.0))
;     (y2 (/ 25.0 4.0)) (y3 0.0) (y4 0.0))

感想とか

整数上の場合だと「解が一つ見つかった後に、目的関数値がそれよりも真に良いということを表す制約を追加して、再度解き直す」ということを繰り返すことで、有界な場合には最適化を行えるのに対して、実数上だと有界であってもZeno状態みたいなことに陥って、最適解に到達できない場合があるはず。 なので、実数の場合には充足可能性ソルバでは最適化問題は解けないと思っていたけれど、こういうやり方をすれば解けるんだなぁ。 ということで面白かった。

まあ、浮動小数点数で計算するような場合には、誤差蓄積で解が見つからなくなるような場合もあるような気はするけれど。