日々の流転

λ. Bernankeの背理法

「Bernankeの背理法だ！以上！」

つーか、Bernankeの背理法で納得してくれるくらいなら、それ以前に納得してくれてるよなぁ。とふと思う。

λ. シカゴ

見てきた。圧倒される。舞台版も見たいなぁ。

λ. お昼

カマンベール・スパゲティ

λ. 超集合論 - circularityの論理の現在 -

こないだの「ラッセルのパラドックス100年」の時の資料。

Quoation

一方，帰納法の双対である余帰納的(co-inductive)構成は，トップダウン的な確認の論理であり，対象が地に足がついているかどうかには関心がない．すなわち循環構造をも受け入れる論理である．しかしながら，その循環性の論理による統制は，帰納的構成の場合とおなじくらいに堅固である．このことは帰納法と余帰納法の間に「双対性」が成り立つことがその根拠である．ブール代数である定理が成り立てば，その双対の定理も成り立つという良く知られた双対性定理というメタ定理の類似である．余帰納法は，「悪循環」ではない，「正しい循環」のために論理といえよう．

λ. [ruby-dev:20128] Re: Array#map

明日の日本のためにも Rite お願いします。
Rite が出る → Array が Enumerable を呼ぶようになる
→ Ruby入門を改訂する → 家が建つ → 景気が良くなる 

の後に「→ (゜д゜)ウマー」という文字が頭の中で補完されて、欝。

λ. 色々せっぱ詰まってたり。ゴールデンウィークなのに……

λ. 床屋

へ行く。

λ. いろいろ

プリンセスチュチュ見忘れた。魔探偵ロキは見たのですが。

λ. call/ccによるshift/resetの表現

メモ。ぐるぐる。

def _abort(&thunk)
  v = thunk.call
  Thread.current[:__meta_continuation__].call(v)
end
 
def reset(&thunk)
  th = Thread.current
  mc = th[:__meta_continuation__]
 
  callcc{|k|
    th[:__meta_continuation__] = lambda{|v|
      th[:__meta_continuation__] = mc
      k.call(v)
    }
    _abort(&thunk)
  }
end
 
def shift(&f)
  callcc{|k|
    _abort{
      f.call(lambda{|v| reset{ k.call(v) } })
    }
  }
end
 
p 1 + reset{ 3 } #=> 4
p 1 + reset{ 2 * shift{|k| 4 } } #=> 5
p 1 + reset{ 2 * shift{|k| k[4] } } #=> 9
p 1 + reset{ 2 * shift{|k| k[k[4]] } } #=> 17

shift/reset その2に続く。

λ. 『スケバン刑事 4』, 和田 慎二

を読んだ。

λ. 東方妖々夢

中村さんのアドバイスに従ったら(?)、時符で一億点とれた。

λ. shift/reset その2

call/ccによるshift/resetの表現の続き。 shift/resetまだ良く分からないや。とりあえず、お約束のGeneratorを書いてみる。とりあえず動いてるみたいだけど、これって正しい?

class Generator
  def initialize(enum, eof = nil)
    @eof = eof
    reset{
      shift{|k| @cont = k }
      enum.each{|item|
        shift{|k| @cont = k; item }
      }
      @cont = nil
      @eof
    }
  end
 
  def read
    @cont ? @cont.call : @eof
  end
end

λ. 夕食

katapon(と書いてみるテスト)とサイゼリア。エビとキノコのグラタン、他。

λ. TOEFL

学校でTOEFLの試験を受けてくる。だるい。

λ. 『素敵なお店のかわいい制服』

を読んだ。

λ. 1bitの情報量

* 今日の一言:
「1bitの情報量は，ちょびっと」 by 服部先生
直後，時間が止まった．

一瞬、ちょびっツ と誤読。

λ. Re: わぁ，どこかで聞いたことがある人だ．

* !!!:
http://jbbs.shitaraba.com/study/bbs/read.cgi?BBS=346&KEY=1035648214&STARTEND=247-
わぁ，どこかで聞いたことがある人だ．

おぉ、確かにどっかで聞いたことのある人ですなー。というか彼はアニオタだったのかっ。ぜんぜん知らなかったYO

λ. ラップトップ

共同購入で買ったラップトップを引き渡されてきた。MS Office を一緒に買った事を研究室の人に驚かれる。

λ. 萩野服部研

新しいラップトップで発表しようと思ってたのだけど、セットアップに手間取って、結局川井さんのを借りてしまった。

λ. 安全に結合可能なアスペクトを提供するためのルール

を読んだ。Matzにっき(2003-05-14) より

λ. ホーア論理

S氏の発表に関するメモ。やっぱ loop invariant って難しい。ところで、ホーア論理では再帰とかが扱えないってホント?

【2009-10-26 追記】 立石さんのコメント通りなのだけど、『算法表現論』(木村　泉，米澤　明憲)に再帰呼び出しに関する規則があったので、ちょっと長いが引用しておく。

ここでは細かい議論には立ち入らないが，再帰的な起動を許す手続きに関しては，帰納法(induction)に類する推論が必要で，たとえば次のような規則*

D7(再帰呼び出しの規則)

    
procedure S(var x~ ; v~); Q(S),  P {T(x~ ; v~)} R ⊢ P {Q(T)} R
────────────────────────────────
P {S(x~ ; v~)} R

が使われる．ただし A⊢B は，一般にAが証明されたと仮定するとBが証明されることを意味する．よって，前提の右側は，P {T(x~; v~)} R という命題が証明されたと仮定して(帰納法の仮説)，手続きSの本体Qの中でSを起動する部分をTで置き換えたもの，すなわちQ(T)の実行に関してP{Q(T)}Rが証明されることを意味する．このような前提が成立するならば，Sをそのまま起動しても実行の直前，直後でPとRが成立する．ただし，再帰的な手続きの実行が終了することは，別に証明しなければならない．

---

* この他に，公理 P {S(x~; v~)} P (ただしx~の中の変数はPの変数として現れない)なども必要となる．

通常の帰納法や余帰納法のような条件がなく、こんな風に証明しようとしている規則をそのまま使っていいのかな?、と疑問になる。 しかし、そのような条件が必要になるのは、停止しないような場合を避けるためで、一方ここで考えているホーア論理の部分正当性ではそもそも停止しない場合のことは考えなくて良いので問題ない。

また、この規則は領域理論の不動点帰納法:

P(⊥)  ∀x. P(x)→P(f(x))  P chain-complete
──────────────────────
P(fix f)

からも得られる。

State を変数から値への関数の空間、Prog を State から平坦ドメイン State_⊥ への関数の空間として、Prog 上の述語 P(C) = {Q1}C{Q2} = ∀s:State. Q1(s)∧(C(s)≠⊥) → Q2(C(s)) を考えると、部分正当性の定義から P(⊥) は常に成り立ち、P が chain-complete であることも容易に示せるので、

∀C:Prog. {Q1}C{Q2} → {Q1}F(C){Q2}
──────────────────
{Q1}fix F{Q2}

が得られる。 これは引数を持たない(再帰呼び出しがある)サブルーチンの、部分正当性の規則とほぼ同じ。

λ. 夕食

ファカルティで「カルビ丼定食」。向井先生のおごり。ごちそうさまでした。

λ. 祖母の百ヶ日なので、家族でお墓参り。

λ. war driving

どうせなので、霊園の行き返りに Netstumbler を立ち上げていたら、 約40箇所ほどヒット。chikoさんが京都に行ったときの話から、もう少しヒットするのではないかと思ってたけど、まぁこんなもんか。傾向としては、市街地よりも住宅地の方が多かったのが少し意外だった。WEPを使っていたのは18%ほどで、SSIDにはYBBUserとかデフォルトのをそのまま使ってそうなのが多かった。

λ. 昼食

濱町で「漁師のフライ定食」。濱町の割りばしの袋に書いてある箸置の折り方は、覚えたいと思うのだけど、いつもいつのまにか忘れてしまっている。

λ. war driving その2

今度はchikaとケシと藤沢方面へ。

λ. ワイヤレスネットワークの脆弱性の実証とWEPを使う上での対策

直江さんの卒論を読み返してみたり。

λ. バイオハザード

バイオハザードのDVDをケシゴムに借りた。ミラ・ジョヴォヴィッチはいいなぁ。

λ. 菜摘ひかるさんが亡くなったという話を聞いて驚く。

λ. Proc#[]

うーむ。気持ち悪いですか。[]による手続きオブジェクトの呼出しを多用してる自分としては、何とか正当化してみたくなるなぁ。

1. ArrayやHashだって、インデックスから値への関数みたいなものだし、
2. なんといっても、M式では関数呼出しは[]だし (爆)

……ダメ?

λ. 水泳

体育で水泳をとってみた。泳ぐのはずいぶん久しぶりな気がする。人数が少なくて少し寂しかったのだけど、色々な道具を使って練習して楽しかった。明日は確実に筋肉痛。

λ. CORBA DII/DSI

libbonoboのFAQを見て、BonoboにIDispatch相当のものが無い理由を知る。

λ. 朝、バスで某I氏に遭遇。彼が友人とやっているというサイト、ARA銀行本厚木支店。

λ. onichan@tom.quickml.com

萩野服部研の「おにぃちゃん」情報を交換するためのメーリングリストを作りました。関係者で参加希望の方は以下のようなメールを送ってください。

To: onichan@tom.quickml.com
Cc: sakai@tom.sfc.keio.ac.jp
From: (参加者アドレス)

(本文に参加メッセージをご記入下さい)

λ. 快適なデスクトップアプリケーションを作ろう

X Window System上で快適なデスクトップアプリケーションを作成しようとした場合、Window Managerとの協調やフォーカスの調整、ウィンドウの装飾の有無等々様々な要素を組み合わせなければなりません。

このWikiでは、様々なWindow Manager上において、より快適なデスクトップアプリケーションを作成するための情報がもりもりと蓄積される事になっています。

勉強になるなぁ。TRPG(2003-05-20)より。

λ. Happy Birthday Ruby-GNOME2

.

λ. Bezilla.org の Paul Ashford とのインタービュー

を読んだ。

(追記) 消えているので、http://web.archive.org/web/20041021115524/http://www.jpbe.net/news/archives/000047.html を参照。

λ. 直江さんのRQLでのプレゼン資料「Wireless Security」を読み返す

λ. 借りた本

『ハッカーズ大辞典』

エリック レイモンド (Eric S. Raymond) [著], Guy L.,Jr. Steele [イラスト], 福崎 俊博 [訳]

『テクノロジー・ウォッチング - ハイテク社会をフィールドワークする』

D.A. ノーマン (D.A. Norman) [著], 岡本 明, 藤田 克彦, 佐伯 胖, 八木 大彦, 嶋田 敦夫 [訳]

『アラン・ケイ』

アラン・C. ケイ (Alan Curtis Kay) [著], 鶴岡 雄二 [訳]

λ. 夕食

バーミヤン。その後直江さんちへ。

λ. 連絡

土日は旅行に行ってくる予定です。 > 某方面

λ. クリエイティブコモンズとは

Internet Magazine 4月号の Creative Commons についての記事を今頃になって読む。

λ. 水泳

前回よりもだいぶ人数が多かった。それから、今回は筋肉痛にはならなくて済みそう。

λ. Least Fixed Point Theory

[ruby-list:35096]で紹介されていたのを思い出して、目を通してみる。それから、2000年秋の知識処理論講義資料とちょっと比較。

【2006-10-08追記】このファイルは上記のURLからは無くなっていて、しかもローカルにも保存してなかったので、見れなくなってしまった。残念。

λ. 某所のたこ焼きパーティに期待してたのだけど台風で中止らしい。

λ. 『これから論文を書く若者のために』 酒井聡樹

を借りた。

λ. トゥルークライム

.