電波日記 tDiary Edition

○ [日記][学校] プロジェクト立ち上げミーティング

三浦半島の真ん中くらい、湘南国際村に来ています。

今日明日と泊りがけで、キックオフミーティング。早速喧々諤々の議論が交わされています。

○ それにしても今日は雨が降って寒いですな。朝来たときには霧の海で周りが何も見えなかった。

○ [網][技術] Load balancing with lvs

某らぼ*1に来れば動いているのが見られますよ、とか言ってみる。(ぁ

○ [学校] 発表練習

明日が中間発表本番。なのでツッコミも前回より厳しめ。

○ [仕事] バイト

今日は XML-RPC と Maven の勉強な感じ。諸事情によりライブラリ実装の中をいじる必要があったので。

Maven 超強力なんだけど、タスクのリファレンスを手元においておかないと使えない気がします。

開発者ならともかく、私みたいにローカルでビルドしたいだけの人向けには、ant の build.xml だけあればいいのにとは思ったり思わなかったりした。*1

○ とりあえずメモ。→ Maven - Available Plugins

○ [日記][学校] 修論中間発表

去年は私も通った道だなあと。

○ [日記] ヒルズ 4F

有隣堂がなくなって、青山ブックセンターになっていた。売場面積も大幅に縮小されたみたい。(通路の片側だけになっていた。)

○ [仕事] 飲み会

六本木交差点近くのカラオケ飲み屋「FIORIA」にて、所属している事業部の飲み会がありました。40 人くらい参加したのかな？

部(グループ？)対抗カラオけ大会で非常に盛り上がりました。

○ 私はひたすらカシスオレンジを飲む役をやってましたが、なんか色が毒々しかった*1。(笑

○ [日記] Mathematica 便利

昨日とりあえず局所的山場を乗り切ったので、今朝はゆっくり寝るぞと思って寝ていたらいつの間にか 15 時とかになってたわけで…。

雨の降る中をバスで学校へ。来てやることといえば、ICPC 強化合宿(来週末ですよ)の問題(というか解答例の)作成作業なわけですが。どーゆー問題か書きたいのは山々だけれども、書いたら当日おもしろくないので書きません。

○ だいぶ式いじりとか忘れてきているので、研究室の Mathematica で検証しながら進めたりしてました。

まあ複雑なものになるとちょっと表記が手計算と合わなかったりもしますが、簡単な代数方程式とか連立方程式を解かせるとかには非常に便利。項書き換え系なので一般的な形で解いてくれますしね。

○ [サーバ管理][セキュリティ] SSH attack

03:43 ごろから先ほどまで、61.195.156.132 からアタックあり。ログによるとうちのサーバ 2 台あわせて 10,000 回(!)くらいログインを試みた形跡が。

whois 情報によると発信は日本国内の企業のネットです。侵入されてんのか、あるいは会社の中に不届き者がいるか…。(おそらく前者のような気がしますけど。

○ ターゲットとなっているユーザ名は日本人の苗字っぽいものが多いです。さすがにこれは回数も多いし、悪質です。パスワード認証使っててユーザ名を苗字とかにしている人は要注意。

いい加減、パスワード認証は通らないということは最初でわかるんだからあきらめてアタックやめればいいのにと思ったりするんだけど…。

動的にファイアウォールのルールを追加したりする対策もやらなきゃだめかいのー。

○ [日記][学校][ICPC] ICPC 夏合宿 2006

今日から 3 日間の日程で、国内予選の上位チームを招いての ICPC 夏合宿です。場所は毎回恒例、代々木のオリンピック記念青少年センター。

9 時集合という話だったけど結局前日 27 時まで作業してたら寝坊してしまい、11 時すぎに学校にて合流。プリンタ*1、プロジェクターと問題文などの紙類を持って向かうことに。

オリセンも夏冬の合宿で毎回のように使っているので、もう慣れたもんです。が、入り口付近のエレベータに Schindler の文字があることを今回初めて知りました。(ほかのエレベータも、まとめてシンドラーかな？)

○ プリンタ・問題文班がついた頃にはチームがぼちぼち来ており、設定が始まっていました。

スタッフの方はそれからプリンタを設定したり PC² を立ち上げたりと、急にあわただしくなる。初日は人員が結構足りなかったので仕方ないといえば仕方ないですが。

問題の入出力データをダウンロードし忘れてきたとか、Java で書かれている出力バリデータが動かなかった*2裏では結構ハプニングも起こっていたんですよ、ぢつは。

で、結局初日の Practice Contest は開始が 30 分くらい遅れたのかな。まあそれでもなんとか、始まってしまえばある種気楽なもんです。

○ 2 時間ほどで初日の練習が終了し、その後はとりあえずチェックインと夕食を食べて、また同じ部屋に集合となりました。

いつもなら講評とかをやるのですが、今回は新顔も結構いますし、チーム同士の交流や情報交換を重要視ということで(かどーかは定かではありませんが)、いつも使っている本や練習の仕方、チームのライブラリなどを見せ合ったり等しました。

ちなみにそんな中、スタッフ部屋では問題作成をまだやってたりしました。(2 日目以降の問題に結構解答作成で結構もめたものがあって、まだこの時間になっても解答ができてなかったりしたという。なんとか当日までには仕上がったのですが。) この後部屋に帰ってもまだ解答作成が続いてたり…。

それでもなんとか 26 時すぎには就寝したかな。

○ [日記][学校][ICPC] ICPC 夏合宿 2006

2 日め。今日は本番のアジア地区予選にあわせて 10 時から Practice Contest をやるので、スタッフは 8 時おき。朝食をカフェテリア「ふじ」で食べてから部屋に。

昨日のうちにデータ等は準備してあったので、それを PC² に登録するだけ。簡単。あとはちゃんとスタッフのコードが通ることを確かめて準備完了。

○ 10 時きっかりにコンテストを開始してから 5 時間の長丁場。途中昼食をはさんだり(チームのほうはそれどころではなかったと思いますが)して、9 問 15 時までみっちりと。

スタッフは結構、ジャッジ対象が来ない間はヒマなのです。が、いつ来るかわからないので*1あまり気も抜けません。

○ 今日は終わってから研究室方面の仕事があったので学校へ。

代々木公園の駅は遠い。

○ [日記][学校][サーバ管理] 停電対応

日曜日に変電設備点検があり、建物が停電するため、サーバをとめる作業。ついでに OS のパッチあてもやってしまう。

Solaris はいつもどおりパッチクラスタをあてる。Linux は apt-get upgrade 一発で死ぬほど簡単。BSD はひさしぶりに make world した。

○ [日記][学校][ICPC] ICPC 夏合宿 2006

さて、作業が終わってオリセンに戻ると、ちょうど講評をやっているところでした。昨日の分 3 問もあわせて 12 問分一気に。

○ この日の問題で私の担当していた分は Problem C の Tetrahedra のみ。とりあえず計算式さえ立てば簡単に解ける類の問題として設定してあったのですが、解答数が少なかったのでちょっと残念。

解くまでの時間で言ったら 2 番目か 3 番目くらいを想定してたのですが、やはり 3 次元幾何ということで敬遠されたのか、参加 9 チーム中 4 チームしか解答出してくれませんでした。(でも出したところはみんな解けている。)

実は私のコードは一箇所場合わけを忘れていたのですが、NaN がでて比較でつねに false が返るため答えに影響しなかった、なんて危ない橋もあったりしましたけど。*2

○ [日記][学校][ICPC] ICPC 夏合宿 2006

3 日目(最終日)。この日も 10 時からコンテスト開始の予定。最終日はチェックアウトなどもあるので、昨日より早起き。シーツと枕カバーをたたんで返却する必要があります。

朝食を食べて部屋で準備。データはサーバ担当が昨日のうちに登録と確認まで済ませていたので特にすることなし。もめていた問題もなんとか折り合いがついたようで、一安心。

○ 10 時から 14 時まで、4 時間で 7 問。最終日は結構鬼な問題セットでした。易しい問題もあるんですけど、難しいのはとことん難しい。

でもそんな中で易しい 2 問(A, E)は 40 分くらいでみんな通してくるかと思いきや、全然サブミットが来なくて結構スタッフ部屋に衝撃が走ってました。kitsune- だけは 2 問で 40 分ということで早々と通してきたんですが、他のチームが全く送ってこないわけですよ。

全部の問題読みあわせしてたのか、それとも…何だろう？ いずれにしても、スタッフとしては、簡単な問題はさっと嗅ぎ分けて取り掛かりさっさと通してしまってほしかったところです。

○ この日は昨日までトップをひた走っていた kitsune- をはじめ東大勢が失速してしまって、かわりに東工大のΩ(というかλというか…)なチームが 1 位をゲット。CLAGGANO、Makegumi ともに沈んでしまってます。どうしたことだろう。

でもこの問題セットできっちり 5 問(C, G はまあむべなるかなというか、予想してました)解いてくるのはえらいと言えましょう。 >λ

問題 F のデータにミスが見つかって*1、コンテスト後に rejudge があったりとハプニングもありましたが。。。

○ コンテストが終わった後は、2 度目の free solving time に突入。後片付けをして、この日は講評をやらずに解散。まあしばらく時間あげるので解いてみてくださいということになっています。

ので、コードのアップ等はしばらく差し控えてます。:-) とりあえず手をつけた問題だけはバラしてもいいだろうということで、OB/OG 会の Wiki ではバラしてますが。

結局この日の問題のうちでは、B, D, E, F の 4 問に手をつけてます。偏りすぎだ。(笑

○ [日記][仕事] 仕事ゲッツ

新しい仕事が降ってきた。

○ [学校] 仕事ゲッツ

こっちでも仕事が降ってｋ(ｒｙ

来週授業で発表があるので忘れないようにせねば。

○ [日記][学校] 雷で目を覚ます朝

今日も雨。まったく鬱陶しい。外出する意欲がそがれるったらありゃしません…。

でもまあ昨日の夜に比べたらずいぶんマシかと思いつつなんとか学校にたどりついて、、、ずっと研究室で論文読んだりしてました。

○ あー、家賃もっていかななー…。

○ [学校][メモ] Modular Development of Certified Program Verifiers with a Proof Assistant (ICFP 2006)

いなば者から話振られているみたいなので、表題の論文をとりあえずざっと読んでみました。定理証明系 Coq で x86 binary program のメモリ安全性を検証するツールを実装しましたというおはなし。

First author の A. Chlipara 氏は、CCured とか PCC (Proof-Carrying Code) とかでその筋ではかなり有名な G. Necula (先生)のところの学生さんのようです。

○ で、検証器を書くわけですが、とりあえず x86 命令セットを直接いじくりまわすより、RISC ベースの簡単な言語(SAL)に落として…とやるそう。この点は確かにいなば者の指摘どおり私の修論と同じ方向性ですなあ。

私の修論は、特にそのプログラム変換の部分に注目した議論を行ったわけであります。ただともかく証明すべき性質は定式化したものの、じゃあ実際どうやって証明すんのということになると、やっぱり定理証明系の出番なのかなーと最近はずっと思っているところであって。おそらくこの論文では、そのへんも Coq で書いていると思われます。

あとはちょっとした違いではありますが、(私の) ADL の方はもうちょっと高級言語に近くて(fat pointer を持っているので、メモリ管理がちょい書きやすいと思う)、実は最近考えている Restricted ADL (fat pointer を抜いて、integer だけ扱うもの)がこの論文の SAL に相当する位置に来るのではないかと思います。

私もちょうど Coq で ADL と R-ADL の意味論を記述したりして、その間が正しく変換されることを証明しようかとか考えてはいたのだけど、そう考えるとこのへん先にやられちゃったなあという感じ。アイタタ。

○ ところで最近、コンパイラを Coq で実装したり[Leroy 2005]とか、定理証明系を使う人が増えてきたよなあと。

米研の Coq の専門家に聞いてみたら、Coq は書いた証明を用いる検証器のコードを自動生成できるんだそうです。やっぱり最終的には検証器を実行可能な形式にしてフロントエンドくっつけて、とやる必要があるので、Coq はそういう用途には非常に向いていると思うわけです。

私も使うには使ってはいるんですが、まだまだ使いこなすには至っていません。おもに使うのは Coq なんですが、Agda にもちょっと浮気したいかもね。*1

○ あとちなみに、いなば者ピックアップの "Static Typing for a Faulty Lambda Calculus" については先週火曜日の米研セミナーでサーベイしてもらいました。

結局 λ_Zap では、同じ計算を 3 こコピーして走らせるって話だったかと思います。で、ところどころに多数決が入って…という意味論ですね。

で、こうなるとどうしても思い出してしまうのが並列プログラムのバリア同期。多数決のところがちょうどバリアになっていると考えられて、それによって分離して走っている状態がひとつにまとまると*2。

λ_Zap ではこの同期の部分があらかじめ意味論に組み込まれていましたが、このへんをもう少し制限を緩めて…という風な発展を考えるとちょっと面白いんじゃないかなあといった感想。λ_Zap の 3 個のコピーでは、たかだか一つのエラーにしか対応できません。同期をとる間が長ければ長いほど間でエラーは起きやすくなると思うので、もっとこまめに同期をとってやればいいんじゃなかろうか？ というところからの発想でした。

○ [日記][食] PASTA de CoCo (御徒町・末広町)

カレーのココイチと同じ経営の、名古屋風のあんかけスパゲッティのお店。なんか久しぶりに行きました。

レジのところの張り紙によると、10 月末で御徒町店は閉店してしまうんだそうな。西新橋にも店舗があるらしいのですが、さすがにそこまで学校から歩いていくのはなあ。

○ [日記][仕事] 最近また Perl と戯れてゐる

文字列処理とかがちょこちょこかけるし、CPAN が充実しているので書くには困らないのですが、やっぱり Java とか強く型付けされた言語である程度きちんと設計したい気もする。

Perl になると型が弱いし OOP もとってつけたようなもんだし(失礼！)、きれいに書こうとすればできるのだろうけれども、そのためにはこれまで自分が知っているものとは全く異なった手法が必要になってくるように思います。

○ Perl で設計のできる Guru 求む。

○ [日記][趣味][技術] Haskell で数列

数列というのは大抵前の決まった何項かから求められるものである。つまり、TeX 風に書けば、

a_n = f(n, a_{n-1}, \cdots, a_{n-k})

ということ。

こういう定義には副作用がないので、引数を定めたら返り値はいつも同じになります。したがって memoization が非常に有効なので、前のほうから iterative に計算することが多いでしょう。Fibonacci 数列

a_{n+1} = a_n + a_{n-1}

はたとえば、

  let fib n =
    let rec iter x cur prev =
      if x >= n then cur else iter (x + 1) (cur + prev) cur
    in iter 1 1 1

みたいに書くのはよくやると思います。

Haskell では遅延評価があるので、数列の打ち切り条件が必要なくなって、有名な無限リストによる書き方

fibs = 1 : 1 : [a + a' | (a, a') <- zip fibs (tail fibs)]

ができるわけです。必要に応じて計算されるので、ともかく数列の漸化式をそのまま implement するだけでいいことになります。

すなわち、fibs の例を n を使わない k 項漸化式に一般化すると、

sequence = a(0) : ... : a(k-1) : [f es | es <- zipk sequence (tail sequence) ... (tailk-1 sequence)]
  where f (...) = ...

とかけばよい。数列の打ち切りは、take とか (!!) あたりにでも任せればよいので、非常にこういった形の数列(自己再帰的な定義を行っている関数といってもよいかもしれない)が書きやすいんだなあと認識した次第。

○ n を使う場合は、sequence を (n, a(n)) のような形のタプルにしてやれば解決します。それより前の項を accumulate するような形(k が n に依存するような)で定義される数列については scanl を使うのがいいのかな。

あとありがたいのが Integer の存在だなーと思う。