日々の流転

λ. 明日から新学期だと思うと気が重い。冬休み中にやろうと思っていた事がほとんど何も出来てない……

λ. bestiality

bestialityで検索してやってきても無駄です。ここに獣姦の情報はありません。

λ. acronymfinder.com

というのを知った。

λ. WString#crypt

WString#cryptは暗黙のうちにStringに変換してString#cryptを呼ぶけど、crypt(3)は抽象的な「文字」の関数ではなくバイト列の関数なので、WStringに対しても定義されているにのは少々違和感を感じるなぁ。まあ、どうでも良いことですが。

λ. 寝坊。

λ. Ruby-CPL (仮称)

型推論部分で設計ミスに気付く。引数を持たないようなClosedFunctorialExpressionはsubstitutionによって引数を増やすことが出来ない……。ぎゃー。

λ. コンパイラ構成論

レポートは木曜まで。やばい。

λ. 東方妖々夢

ようやくプレイ。ミスディレクション楽しいですね。あと、アンディレクティッド・レーザーもいい感じ。

λ. 読書

『全日本妹選手権 3』

堂高 しげる [著]

λ. チャートパージング(日本語訳)

http://www.cs.ualberta.ca/~lindek/650/papers/chartParsing.pdf の日本語訳。

λ. 代替スタイルシート

Opera7で具合いが悪いようなので、代替スタイルシートを全部外してみました。

λ. 継承(or subtyping)とvariance

なるほど。やっぱりFAQだったのですね。(Eiffel FAQ,日本語訳)でしたか。ふむふむ、理論的な解決をしているわけではなく、コンパイラによるチェックまたは実行時の例外という扱いなのですね。

それから、Satherはこの場合contravarianceなのか。

λ. 今日から学校が始まる。憂鬱。

λ. Inkscape

Inkscape is an open source SVG editor with capabilities similar to Illustrator, CorelDraw, Visio, etc. Supported SVG features include basic shapes, paths, text, alpha blending, transforms, gradients, node editing, svg-to-png export, grouping, and more.

Inkscape's main motivation is to provide the Open Source community with a fully XML, SVG, and CSS2 compliant SVG drawing tool.

メモ。tail's daily? diary より。

λ. Re: 可変長引数の関数?

あー。確かにcollectVAList要らないっすね。僕もまだまだだなぁ。

λ. 『猫の地球儀　幽の章 』, 秋山 瑞人 著, 椎名 優 イラスト

を読んだ。まさかハッピーエンドなんてことは無いだろうとは思ってたけど、そう来たかぁ……。夢を追うことと、その代償。少し考えさせられる。

λ. M2の会

みんなで修論書き等。

著作権保護期間の延長を行わないよう求める請願署名にみんなで署名。後でまとめて送る予定。 ちなみに、私自身は青空文庫に特に思い入れはないけど、著作権保護機関の延長は経済合理性を欠くと思うので、いい機会と思い署名。

FFネタ (<URL:http://mixi.jp/view_diary.pl?id=311590915&owner_id=28560>に詳しい)

• 心無い主査
• 破壊の副査
• 論文の法則が乱れる
• 修論とはいったい…… うごごご

おみくじ。「十二番小吉: 今のつらさ　先のたのしみ」。これは死亡フラグか!?

λ. “Much Ado about Two: A Pearl on Parallel Prefix Computation” by Janis Voigtländer

POPL 2008メモ1日目 - sumiiの日記(2008-01-11) より。 積読消化。

結合的な二項演算 ⊕ と入力 x1, …, xn とから x1, x1⊕x2, …, x1⊕x2⊕…⊕xn を計算するのが parallel prefix computation。 で、多相的な parallel prefix computation の関数 (α→α→α)→[α]→α の実装の正しさは、αが3値のデータ型のときだけ確かめればOKという話。

パラメトリシティ(free theorem)から正しい実装(scanl1)と結果が等しくなることを証明していて、確かにちゃんと追いかけるとそうなっているんだけど、なんだか不思議な感じ。 あと、整数全体ではなくて3値で十分であることの証明が賢いなぁと思った。 他のアルゴリズムに対しても系統的にこういうことを言えるようになると楽しそうだなぁ。

λ. PLDIr #5

PLDIの論文を読む PLDIr の第五回に参加。 今回はPLDI2001の論文が対象で、私は以下の3本の論文を紹介した。

• Design and Implementation of Generics for the .NET Common Language Runtime (著者版)
• Automatic Predicate Abstraction of C Programs (著者版)
• The Pointer Assertion Logic Engine (著者版)

Design and Implementation of Generics for the .NET Common Language Runtime は、文字通り.NETのCLRにパラメトリック多相を実装する話。 JVMや当時のCLRは多相をサポートしてないので、多相をコンパイルしようとすると性能、プリミティブ型の扱い、コンパイルの複雑さなどの問題がでる。 なので、CLRレベルでちゃんとサポートしようという話。 伝統的なコンパイル・リンク・実行というモデルではなく、CLRの動的なコード生成やJITを活用した設計になっていて、実行時にコードのspecializeを行う。 厳密な実行時型もサポートし、またプリミティブ型によるインスタンス化も性能を低下させずに実現。 vtable内に型パラメータとオープンな型のスロットを用意する点などが面白かった。

Automatic Predicate Abstraction of C Programs はソフトウェア向けモデル検査器SLAMで抽象化を行っているツールC2BPの詳しい話。 C2BPは、CプログラムPと述語の集合Eから、述語抽象化した Boolean program B(P,E) を生成する。 この Boolean program の生成は自明な話だと思っていたけど、元のプログラムのコードに対応して、どの述語の真偽がどう変化するかを判定するのは結構工夫が必要で、面白かった。

The Pointer Assertion Logic Engine は、PALE(the Pointer Assertion Logic Engine)というツールについて。 PALEは、ヒープの構造に関する性質を Pointer Assertion Logic というロジックで、アノテーション(事前条件・事後条件・不変条件)として記述し、プログラムとアノテーションを、WS2S(weak monadic second-order theory of 2 successors)に変換してMONAで検証する。 記述可能な性質は Graph types と呼ばれているもの。

以前にMONAで正規表現にマッチする例を生成したりしたけど、MONAってこんなことも出来るのか、と驚いた。 そういえば、計算機言語で定理証明 (Proof Party.JP) - ヒビルテ(2009-10-24)のときに触ってみたJahobも、決定手続きの一つとしてMONAが利用可能だったけど、同じような感じで使ってるのかなぁ。

発表資料 (PDF):

関連

• Asynchronous Exceptions in Haskell - ヒビルテ(2009-11-08)