2002-11-23 [長年日記]
λ. 夜まで寝てた。何やっているのだろうね、俺は。
λ. SFCにおける日記間リンク
ふと、SFC Antenna に登録されている日記のURL間のリンク関係を抽出して、ラベル付き有向グラフとしてビジュアライズしてみた(SVG,DOT)。(手元のGraphvizに日本語パッチが当たっていないので、SVGだけでスマソ)
他の日記とのリンクを持たないノードは省略してしまったのだけど、このグラフはちょっと寂しいよなぁ。日記URLかどうかの判定が厳しすぎるのかも知れないけど、ひょっとするとSFC生には日記間でリンクを張り合うような習慣はあまりないのかも知れない。
λ. Ruby-GNOME2-0.1 is released!
まずは一区切りか。後半はあまりコードを書けず、既に「過去の人」状態の私ですが、それでも何か肩の荷が降りたような感じ。
λ. 中間管理職はヴェブレン財
9/24に買った『構造改革論の誤解』に以下のような事が書いてあって、目から鱗だった。そうか!、そうだったのか!!
日本では中間管理職は、意思疏通や意思決定の媒体という「職能」において必要とされているというよりも、仕事へのインセンティブを与えるみせびらかしの(conspicuous)効果をともなう「ヴェブレン財」として機能してきた。
λ. rand
1.7では Mersenne Twister を使うようになっているのか。
まったくそのとおり >中間管理職
ITT0 って何ですか？
ITTはMartin-L\"ofの型理論です。<br>最近読んでいる Martin-L\"of 本人の<br>『Intuitionistic Type Theory』(isbn:8-8708-8105-9)<br>という本で知りました。<br>ITT_0, ITT_1, ... があって、ITT_{n+1} は ITT_n の拡張になっています。<br><br>『型理論』(isbn:4-7649-0201-X)によると、<br>Curry-Howardの同型対応によって<br>直観主義論理に基づき算術を含んでいるある論理体系に対応して、<br>構成的数学の多くはこの論理体系で形式化出来るそうです。<br><br>型システムとしては、MLやHaskellで使われているようなものしか<br>これまで知らなかったのですが、ITTもなかなか面白いです。<br># dependent type を多用するのには面食らいましたが。
ITT_0 が一番弱いのにすでに選択公理が証明できるスか。