日々の流転

λ. Y先生宅でホームパーティ。料理も素晴らしかったし、ゲームも楽しかった。

ゲームは、いつもの「上海」の他に「スコットランドヤード」と花札をやった。スコットランドヤードでは3回とも怪盗側のミスで刑事側が勝利。ミスさえしなければ怪盗側の方がかなり有利だと思うので、またやってみたいところ。花札もまあ楽しかった。花札は絵が綺麗でルールも覚えやすいので外国人にもウケが良いらしい。そういえば、Rはゲゲゲの鬼太郎の花札を持っているそうだ。それから「ロジ」もやりたかったのだけど、行方不明でちょっと残念だった。

楽しい時間をありがとう!

λ. 読書

『HELLSING(ヘルシング) 1』

平野耕太[画]

λ. 商集合 (Enumerable#/)

module Enumerable
  def /(r)
    result = Array.new
    each{|item|
      if a = result.find{|b| r.call(b.first, item)}
        a.push(item)
      else
        result.push([item])
      end
    }
    result
  end
end

(0..10) / lambda{|a,b| a%3 == b%3}
#=> [[0, 3, 6, 9], [1, 4, 7, 10], [2, 5, 8]]

λ. 寝坊。

λ. AtheOS用のjp106のkeymap

ところで、誰かjp106キーボード用のkeymap持ってませんか?

λ. File.cleanname

手元に環境が無いのできちんと確認してないけど、Plan 9 のcleanname(2)相当のつもり。

後で、akrさんのPathnameに既にsimplifyメソッドがあるのに気が付いて、少し悔しい。

λ. Cygwin上でPEACE

Cygwin なんでも掲示板より

λ. 名探偵コナン

つーか、もし崖の上から下を覗き込まれたら、それだけでバレちゃったのでは?

λ. i-know.jp

i-know.jp のアンテナを試しにちょっと使ってみる。http://i-know.jp/sakai/

ブックマークレットでアンテナに登録出来るのは存外に便利だなぁ。はてなアンテナとどっちがいいのかな。

λ. CMSC 451 Lecture 12, Myhill-Nerode minimization

メモ。マイヒル・ネロード(Myhill-Nerode)の定理 のわかりやすい説明。

λ. 花粉症?

目が痒くて仕方ない。スギ花粉ムカつく、ムカつくー。うがぁぁぁ。大体スギが多すぎるからいかんのじゃ。政府は公共事業でスギを切れちゅーに。それから、スギ花粉は環境汚染物質なので、スギに対して環境税をかけて、それを財源に花粉症対策でもしてくれ。

λ. Announce: 圏論勉強会(第五回)

そうそう。今週末は圏論勉強会の五回目がありますよ。堅苦しい集まりではないので、圏論に興味のある人は是非お気軽に御参加下さい。(初参加の方は mixi:圏論勉強会(第五回) か haskell-jpメーリングリスト で参加を表明しておくと良いと思います)

ちなみに、Session 6-9 は一度飛ばしてしまって、今回は Session 10 のブラウアーの不動点定理の話から始めるそうです。このセッションはこの本の前半最大の見せ場なので、お楽しみに!

日時 (今回はいつもと時間が違うので注意!!)

2005年3月19日(土曜) 10:00〜

場所

タイムインターメディア様 2階会議室 (地図)

テキスト

Conceptual Mathematics: A First Introduction to Categories

λ. 靖国参拝、対中戦略に有効　日米同盟強化への注意そらす　米の中国専門家見解

へぇ(3)。

λ. クライゼルの注意

かがみさんの「ロッサーの不完全性定理」で紹介されていた、「クライゼルの注意」を示してみる。

φ := ∃x. prove´(x, [0=1]) とする。

1. T ⊢ φ → (∃x. prove(x,[0=1]) ∧ (∀y≦x. ¬prove(y,[¬(0=1)]))) であるので、T ⊢ ¬(0=1) のある証明図をπとすると、T ⊢ φ → (∃x≦[π]. prove(x,[0=1])) 。
2. 一方、Tの無矛盾性より T ⊬ 0=1 なので、T ⊢ ¬∃x≦[π]. prove(x,[0=1]) 。

よって、T ⊢ ¬φ 。

最初は何故成り立つのか不思議だったけど、20070316#p01でロッサーの不完全性定理を理解したら、あとは自明だった。

λ. DDoSうざい

ここ数日、散発的にDDoSを喰らっているようなので、このページにもアクセスしにくいかも。 私はサーバ管理にはあまり詳しくないので、対処はまかせっきりなのだけど、中々大変そうだ。

λ. 第68回情報処理学会・プログラミング研究会

ytbさんが「再帰的定義を可能にする述語論理の証明支援系上の実装」という発表をするようなので、お会いしに行きたいなぁ、と思っていたが、それどころじゃないのだった。