日々の流転

λ. 於因説果

色々と反省。

λ. 夜

クタクタだったので、帰ってすぐに寝た。

λ. 『痛快すずらん通り』 花見沢 Q太郎

を読んだ。

λ. 今日の向井研 (Elementary universal mapping properties その2)

今日の発表は大失敗。うぐぅ。(発表資料)

λ. 数学的な夫婦喧嘩

というネタで笑った。QEDが超必殺技だったりして……

λ. 線形の理論

そうか、線形写像の世界では、sectionである事とretractionである事が一致してしまうのか。

λ. 夕食

マクドナルド

λ. taiikukai

秩父宮体育館でバスケ。バスケなんてやるの何年ぶりだろう。ルールもすっかり忘れてて焦る。スリーポイントシュートって何だっけ? みたいな。4分程度のミニゲームを何度かやったのだけど、4分って長いね……。ダメじゃん、俺。でも、何故か運動量が多いと思われてしまい、不思議なのだ。

関係ないけど、「姪御さん」が「メイドさん」に聞こえてしまってビックリする。久野君の影響か。

λ. 夕食

taiikukaiメンバに中村さんを加えて、藤沢のハンバーグ屋さん(?)のGruppeへ。GruppeはJパスタの下のお店で、なかなか美味しかった。
ヘルシーチキンハンバーグ

λ. スマッシュブラザーズ大会

それから帰る途中でチカと唯から召喚され、大乱闘スマッシュブラザーズDX大会に突入。それから、ビューティフル ジョー というゲームをみしてもらう。ほほぅ。最近のCAPCOMはこんなゲームを出しているのか。

帰って風呂に入ったら、もう午前4時。寝なきゃ……

λ. 面接結果

入試に受かってたことを確認。奨学金の方も予想通り落ちていた。予想を裏切ってこっちも受かっていたら最高だったのだけど、さすがに100万の給付はそんなに甘くないよな。

しかし、これで何としても来期で卒業しなくてはならなくなったな。頑張らねば!!

λ. 『白い月光 (1)』『白い月光 (2)』 花見沢 Q太郎

を読んだ。

λ. ICPC過去問: Circle and Points

例によってHaskellで瞬殺(Circle_and_Points.hs)。本番じゃHaskell使えないけどな。

あるn(≧2)点を囲むような円があるとする。このとき、円をずらすことで、それらの点を全て囲んで、かつその内の2点が円周上にくるようにすることが出来る。つまり、2点が円周上にくるような円だけを調べても一般性は失われない。(2005-07-22 追記: このことについては sheepman さんによる説明 が分りやすい)

(追記: 誤差が少し心配だったので、円周上に持ってきた二点を無条件で円に囲まれているものとして扱うよう変更した。)

それと、sumimさんがSmalltalk版を書いてくれました。Smalltalkの勉強になります。

λ. 『大学の話をしましょうか—最高学府のデバイスとポテンシャル』 森 博嗣

を読んだ。 森博嗣ならこう考えるだろうなという内容で、あまり驚きはなかった。

λ. 人狼審問 : (1569)沼地の村

プロローグの空白発言が面白くて、少し観戦していた。

関連リンク

• B1/1596村 - 人狼ファンWiki

λ. ひぐらしがなく頃に

<URL:http://mixi.jp/view_bbs.pl?id=19963685&comm_id=23799> より。 これは酷い(笑

λ. tDiaryに日表示から月表示へのリンクを

日表示からその月の日記一覧の表示に移動したいと思うことが良くあったので、簡単なプラグインを書いてみた。

# navi-this-month.rb
alias navi_this_month__orig__navi_user_day navi_user_day

def navi_user_day
  result = navi_this_month__orig__navi_user_day
  if @mode=='day'
    this_month = @date.strftime( '%Y%m' )
    result << navi_item( "#{@index}#{anchor this_month}", "#{navi_this_month}" )
  end
  result
end

def navi_this_month; "月表示"; end

λ. ソフトバンクの2009Springキャンペーン

ソフトバンクオンラインショップ 2009Springキャンペーン でJCBギフト券1000円と microSD 2GB をもらった。 が、ギフト券はともかく microSD は iPhone だから使途がない……

λ. 不動点演算子はチャーチ数での無限大?

@mametterさん が「Church numerals で無限大を考えるとしたら、Y コンビネータと同じになるのだろうか」と書いていたので、考えてみた。

普通の自然数の型は Nat = μX. X+1 で、集合の世界で考えるとこれには無限大は含まれない一方、その双対の CoNat = νX. X+1 は集合の世界で考えると自然数の集合に無限大∞を付加してやったような集合になるので、これを使って考えてやれば良いのではないかというのを最初に考えた。

ただ、チャーチ数の型 ∀X. (X⇒X)⇒X⇒X はNatのチャーチエンコーディング ∀X. (X+1⇒X)⇒X を変形したものであって、CoNatのチャーチエンコーディング ∃Y. Y×(Y⇒Y+1) = ∀X. (∀Y.Y×(Y⇒Y+1)⇒X)⇒X とは違い、そのままではうまくいかないので、結局NatとCoNatが一致するような世界で考える必要がある。領域理論的な世界ではそれが言える。

Haskellで自然数型とチャーチ数の型、それらの間の対応、そして無限大を以下のように定義する。 Haskellに対応する圏では本物の直和がないので、上の話とはちょっと違っちゃうんだけど、まあそれはそれ。

{-# LANGUAGE Rank2Types #-}

data Nat = Succ Nat | Zero
type ChurchNumeral = forall a. (a->a)->(a->a)

build :: ChurchNumeral -> Nat
build c = c Succ Zero

unbuild :: Nat -> ChurchNumeral
unbuild n s z = foldNat s z n

foldNat :: (a -> a) -> a -> Nat -> a
foldNat s z Zero = z
foldNat s z (Succ n) = s (foldNat s z n)

infinity :: Nat
infinity = Succ infinity

なお、infinity は Succ の唯一の不動点である(CoNatのfinalityから言える)。

ここで、不動点結合子を使って無限大っぽいチャーチ数を定義してみる。

infinity' :: ChurchNumeral
infinity' s z = fix s

すると、build infinity' = infinity' Succ Zero = fix Succ で、infinityはSuccの唯一の不動点なので、build infinity' = infinity となる。

逆に infinity をチャーチ数に変換してみると、unbuild infinity s z = foldNat s z infinity = foldNat s z (Succ infinity) = s (foldNat s z infinity) となるので、unbuild infinity s z は s の不動点。また、最小不動点である事も領域理論的な推論で容易に示す事ができる。

というわけで、まあ、不動点演算子はチャーチ数での無限大と言って良さそうだ。

この辺りをもっとちゃんと考えると、P.S. Mulry. Strong monads, algebras and fixed points のような話になるのだと思うけど、この論文、読もう読もうと思いつつずっと読んでなかった……