日々の流転

λ. なんか変な夢を見たような気がするが、わすれてしまった。

λ. 読書

『少女革命ウテナ 2 - 翠の想い』

大河内一楼 [著] ビーパパス・さいとう ちほ [原作] さいとう ちほ[イラスト]

『ジャングルはいつもハレのちグゥ 6』

金田一蓮十郎[著]

『テニスの王子様 12 - 無敵の男』

許斐剛[著]

λ. おたく度チェック

というのをやってみた。

(犬死にマグナムトルネードより)

さかいさんお疲れ様でした。あなたの総合おたくパワーは273パワーです！　詳細は次の通りになっています。

	結果値 (単位：パワー)
マニア度	30パワー
危険度	41パワー
萌え度	35パワー
煩悩度	42パワー
さわやか度	66パワー
迷惑度	38パワー
潜在能力	21パワー

あなたのマニア度は30パワーです! かなりマニア度は低いですね。何にもこだわらないあなたは、ある意味異常なのかもしれません。この際、色々な物事に関心を持ってみては？

あなたの危険度は41パワー。低い危険度です。人生にはスリルも大事。少し危険なくらいがいいのかも。真面目過ぎるとかえってキケンだったりするのかもしれません。反動っていうのは恐ろしいものですからね。お気を付けを。

あなたの萌え度は35パワー。全然萌えていません。あなたはおそらく「もえるって書いてみて」と言われれば「燃える」と書き、「萌える」なんて言葉は思いつきもしないでしょう。そのような生活をおくっている人にとっては知らない方がいい言葉かもしれません。あなたは十分正常ですから。

あなたのさわやか度は66パワーです。隠れオタクとして十分やっていけるレベルですね。あなたは話さえしなければオタクとバレる事はないでしょう。しかし、下手に話すとボロが出る可能性があります。隠しているのでしたら気を付けましょう。

あなたの迷惑度は38パワー。これは低いですね。あなたは今の所、世間に迷惑をかけるような事はしていませんが他人がどのような事を迷惑だと思うかわかっていません。下手をするとワイドショーや新聞に取り上げられる程の犯罪をおかす可能性すら秘めています。他人の気持ちをきちんと考えて行動しましょうね。

あなたの煩悩度は42パワー。低い煩悩度です。あなたのその無欲の精神は、オタクになるよりも聖人君子になる方がよっぽど向いています。今から方向転換を考えて、歴史の教科書に載る事を目指してみては？

あなたの潜在能力は21パワー。オタクにはなれません。あなたの潜在能力はかなり低い数値です。今はマンガやアニメが好きだったとしても、年を重ねるにしたがって興味は薄れてくるでしょう。それでいいのです。きっと一般社会の方が楽しいですよ。

λ. 日本海とか東海(동해)とか

大崩れ日記より

• 東海問題を考える
• The Sea of Japan

λ. Gimp範例教學

.

λ. お昼

みのり邸で広東麺。

λ. GIMP 1.2.3

1.3系と完全に共存出来るようになったらしい。

λ. アドゥレセンス黙示録

少女革命ウテナの劇場版を見た。

そういえば、「ウテナ」の作品群って、ストーリーのディテールは異なっていても、テーマは共通であって、しかもそこで語られている構造は根元的でかなりの普遍性を持っているんだよなぁとふと思った。

それはさておき、他の人も「テメェはサイバーフォーミュラか!!」とかツッコミながら観てたんだろうな。

λ. 文法の誤解

昨日の続き。ほっといてもアレなので、一括して処理してしまう。何故かうまく処理できなかった部分があったので、そこは手作業で。

require './tdiary.rb'

def process(paragraph)
  if /^</ =~ paragraph.body and not /\A</ =~ paragraph.body
    lines = paragraph.body.split("\n")
    for i in 0...(lines.length) do
      break if /\A</ =~ lines[i]
      lines[i] = '<p>' + lines[i].sub(/\A\s+/, '') + '</p>'
    end
    paragraph.instance_eval{
      @body = lines.join("\n")
    }
  end
end

TDiary.new(nil, nil).instance_eval{
  Dir["#{@data_path}??????"].each{|fname|
    PStore.new(fname).transaction{|db|
      db['diary'].each_value{|diary|
        diary.each_paragraph{|paragraph|
          process(paragraph)
        }
      }
    }
  }
}
Tags: tDiary 

λ. 野蛮な歴史を持つ国

毎日新聞のこの記事、実際の紙面では『さらに、米国が行動を起こす対象は、テロ組織だけでなく「大量破壊兵器を開発したり、野蛮な歴史を持つ国」も含まれると述べ、「これらの国々がテロ組織と結び付けば、自由世界は脅かされる」と警告した。』と続いているのだけど、何でオンライン版ではこの部分が落ちているのだろう。

で、おいおい。大抵の国は「野蛮な歴史」を持っている。特に現在の先進国で「野蛮な歴史」を持たない国など一国も無いと思うぞ。それから、これまで兵器を紛争地帯に散々売りつけて回ってたのは一体どこだと思ってるんだ? 何様のつもりだよ、テメェ。

こんな下らないこと書いてもしょうがないんだろうけど……

λ. サブタイプと代入

http://www15.ocn.ne.jp/~rodinia/Blog/MyJournal22.html#categorymisc5

私はOCamlの型システムについては全然知らないので勘違いしているかも知れませんが、この問題は単にその型システムが安全でないというだけのように思えます。

安全な型システムであれば、型Aが型Bのサブタイプであることの必要条件として、少なくとも、Bのインターフェース中の正(負)の位置に現れる全ての型について、Aでの対応する型がそのサブタイプ(スーパータイプ)になっていることを要求するはずです。

この例では、型 <n : <y : b>; m : a> のフィールドnが代入可能ということは、この型が setN: <y : b> -> () というメソッドを持っているのと同じとみなせるので、型 <y : b> は負の位置にも現れていると考えるべきでしょう。したがって、<n : <x : a, y : b>; m : a> が <n : <y : b>; m : a> のサブタイプであるためには、<x : a, y : b> が <y : b> のスーパータイプである必要があります。しかし、これはいくらなんでも成り立ってませんよね?　それにも関わらず <n : <x : a, y : b>; m : a> を <n : <y : b>; m : a> のサブタイプと認めてしまうような型システムであれば、実行時にエラーが起こって当然だと思います。

ちなみに、サブタイピングをサポートする関数型言語の他の例としてO'Haskellがありますが、このようなコードはちゃんと型エラーになります。(以下に出てくるCmdはIOモナドみたいなものです)

-- type constructor (kind * -> *) (variance +)
struct Y y =
   getY :: Cmd y
 
-- type constructor (kind * -> * -> *) (variance + +)
struct XY x y < Y y =
   getX :: Cmd x
 
-- type constructor (kind * -> * -> *) (variance 0 +)
struct S n m =
   getN :: Cmd n
   setN :: n -> Cmd ()
   getM :: Cmd m
 
-- OK
cast1 :: S a (XY a b) -> S a (Y b)
cast1 x = x
 
-- NG
cast2 :: S (XY a b) a -> S (Y b) a
cast2 x = x
{-
ERROR "Test.hs" (line 21): Type error in variable
*** term                : x
*** type                : S (XY a b) a
*** does not match      : S (Y b) a
-}
 
-- NG
test :: S (XY a b) a -> Y b -> Cmd ()
test x y = x.setN y
{-
ERROR "Test.hs" (line 31): Type error in function application
*** term                : (.setN)
*** type                : S a b -> a -> Cmd ()
*** constraints         : Y c < a, a = XY b c
*** because             : variable has conflicting bounds
-}

λ. オブジェクトはレコード型か？

生存記録(2005-02-12) では「レコード型との違いは、自己参照できる点だと思う」と書かれているけど、任意のレコード型Aの上に不動点結合子fix_A:(A->A)->Aが定義されている世界ならば、自己参照してるレコードなんていくらでも定義できるし、あまり本質的な違いではないような気がする。

……考えていて、ふと、オブジェクトがレコード型と同一視されるのは、メッセージが(引数の違いを無視すれば)高々有限個しか存在しないからではないかと思った。高々有限個しかないから、関数をフィールドとするレコードで表現できてしまう。では、もしメッセージが有限個ではなく、しかも何らかの代数構造(プロセス代数的な何か?)を持っていたとしたらどうだろうか?

λ. OOの型理論の本

http://www15.ocn.ne.jp/~rodinia/Blog/MyJournal22.html#categorymisc7

読んだことはないですが、最も参照されているのは "A Theory of Objects", Martin Abadi and Luca Cardelli だと思います。

λ. 第十四回圏論勉強会

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

写真

λ. 『FREAKONOMICS -- A Rogue Economist Explores the Hidden Side of Everything』

を読んでるのだが、この本面白いな。

1. What Do Schoolteachers and Sumo Wrestlers Have in Common?

州標準テストの成績評価を教師の評価とリンクさせることが教師にズルをするインセンティブを与えるという話と、相撲の勝敗構造が力士に八百長を行うインセンティブを与えるという話。 どちらについても実データを分析することで、実際にそれらが行われていたことを裏付けている。

これまで相撲には興味なかったのだけど、八百長の話を読んで相撲に興味がわいてきた。 相撲協会が八百長の存在をどんなに否定しようとも、この分析結果を見る限りでは八百長が行われていたことは疑いようがないように思える。ならば、相撲協会は八百長の存在を単に否定するのではなく、八百長のインセンティブを生じにくい制度に制度を変更するべきではないかと思う。 もっとも、この本には実際のデータや分析手法の詳細は載っていないので、詳しくは、参考文献の Winning Isn't Everything: Corruption in Sumo Wrestling を読むべきか。

あと、Paul Feldman のベーグルの話も面白い。

関連

Freakonomics Blog

著者らのブログ。

Freak-Freakonomics

ルビンシュタインの書評。『ヤバい経済学』よりもヤバい書評 - Economics Lovers Live と Freak-Freakonomics - Economics Lovers Live より。

λ. レッツゴー！陰陽師　PV

元のゲームは知らないけど、これは耳に残るな。

【追記】 ファンの作品かと思っていたら、違ったらしい。 「陰陽師」はなぜ削除されなかったのか - "豪血寺"サントラCDが発表

λ. 『戦前の少年犯罪』 管賀 江留郎

を読んだ。

関連

• 少年犯罪データベース
• 少年犯罪データベースドア

参考

• 絶望書店日記(2007-11-08)　戦後もっとも重要な本
• 絶望書店日記(2007-11-14)　ウェブ考察のためにもっとも重要な本

λ. Formal Methods Forum

昨日の PLDIrで紹介されたので登録してみた。

tmiyaさんのCoqとWhyについての発表資料「Coq and Why : Formal Verification Tools」が面白い。

• Coq_20100208a.pdf
• <URL:http://www.slideshare.net/tmiya/coq-20100208a>

Whyは 計算機言語で定理証明 (Proof Party.JP) のときにちょっと使ってみた Jahob と同じようなツール。