トップ 最新 追記

日々の流転


2003-05-01 [長年日記]

λ. Bernankeの背理法

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

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

λ. シカゴ

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

シカゴ 期間限定廉価版 [DVD](ビル・コンドン) 「シカゴ」 オリジナル・サウンドトラック(サントラ/リチャード・ギア/キャサリン・ゼタ=ジョーンズ/レニー・ゼルウィガー/ダニー・エルフマン/クイーン・ラティファ・アンド・リル・キム・フィーチャリング・メイシー・グレイ/アナスタシア/クイーン・ラティファ/ジョン・C・ライリー/テイ・ディッグス)

Tags: 映画

λ. お昼

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

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

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

Quoation

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

Tags: 論文

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

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

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

Tags: ruby
本日のツッコミ(全4件) [ツッコミを入れる]

ψ はら [なぜ欝に?っていうか今「シカゴ」を見てきた帰りです。映画の日。]

ψ かもね [見てきましたか。 僕も先月、アメリカで見ました。字幕がなかったのでちょっと分かり辛かったけど。。実話な上に、Roxy..]

ψ さかい [最近毒されてるなぁと気づいたからです > 欝 それにしても映画の日はいいですよね。]

ψ さかい [実話だというのは聞いていましたが、今でもロゴTシャツが売ってるって凄いですね。 それから、ダンサーインザダークは観て..]


2003-05-03 [長年日記]

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

λ. 床屋

へ行く。

λ. いろいろ

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

λ. 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に続く。

本日のツッコミ(全6件) [ツッコミを入れる]

ψ はら [難しい。catch-throwでは書けないのですよね、、、それより何これ?(^^;]

ψ さかい [shift/resetは「部分継続」を扱うオペレータです。callccが「リターンした後の計算全体」をブロック引数に..]

ψ はら [なるほど!面白いですね。 例が難しい、、、こういうことですよね。 k = nil p reset{ 2 * shi..]

ψ さかい [そうです。 ちなみに、call/ccがスタックの全体をコピーする必要があったのに対して、shift/resetでは..]

ψ はら [この実装は等価でしょうか: def reset callcc{|k| (Thread.current[..]

ψ さかい [だと思います。 最初の実装から、 (1) meta continuation の保存と復元にスタック(Array)..]


2003-05-07 [長年日記]

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

を読んだ。

スケバン刑事(デカ) (第4巻) (白泉社文庫)(和田 慎二)

Tags:

λ. 東方妖々夢

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

Tags: 東方

λ. 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
本日のツッコミ(全1件) [ツッコミを入れる]

ψ はら [正しいみたい。reset/shiftがこの用途に向いてないことの例証かも。(^^;]


2003-05-09 [長年日記]

λ. 夕食

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


2003-05-10 [長年日記]

λ. TOEFL

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

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

素敵なお店のかわいい制服(新紀元社編集部)

を読んだ。

Tags:

λ. 1bitの情報量

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

一瞬、ちょびっ と誤読。

Tags: tom

2003-05-15 [長年日記]

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

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

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

λ. ラップトップ

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

λ. 萩野服部研

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

Tags: tom

2003-05-16 [長年日記]

λ. ホーア論理

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}

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

Tags: 向井研

λ. 夕食

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

本日のツッコミ(全3件) [ツッコミを入れる]

ψ 立石 [一応、扱えると思います。]

ψ 立石 [再帰関数Fの中身Pについて{A}P{B}を証明するときに、{A}F{B}を使えるような規則を入れます。「{A}F{B..]

ψ さかい [なるほど。これなら確かにいけそうですね。]


2003-05-18 [長年日記]

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

λ. war driving

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

λ. 昼食

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

λ. war driving その2

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

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

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

Tags: 論文

λ. バイオハザード

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

バイオハザード [DVD](ポール・アンダーソン)

Tags: 映画

2003-05-19 [長年日記]

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

λ. Proc#[]

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

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

……ダメ?

Tags: ruby

λ. 水泳

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

λ. CORBA DII/DSI

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

本日のツッコミ(全2件) [ツッコミを入れる]

ψ ささだ [ああ、なるほど。そういう見方もあるのか>Array,Hashも。 もともとまつもとさんの中で、Proc に [] ..]

ψ さかい [そうですね。まつもとさんが元々どう考えていたのかは、私も気になります。]


2003-05-20 [長年日記]

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

λ. onichan@tom.quickml.com

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

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

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

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

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

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

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

Tags: URL
本日のツッコミ(全1件) [ツッコミを入れる]

ψ かもね佑 [さかいくんへ。 今日の「たけしの誰でもピカソ」はなるべくみるといいよ。]


2003-05-23 [長年日記]

λ. 借りた本

『ハッカーズ大辞典』
エリック レイモンド (Eric S. Raymond) [著], Guy L.,Jr. Steele [イラスト], 福崎 俊博 [訳]
『テクノロジー・ウォッチング - ハイテク社会をフィールドワークする』
D.A. ノーマン (D.A. Norman) [著], 岡本 明, 藤田 克彦, 佐伯 胖, 八木 大彦, 嶋田 敦夫 [訳]
『アラン・ケイ』
アラン・C. ケイ (Alan Curtis Kay) [著], 鶴岡 雄二 [訳]
Tags:

λ. 夕食

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

λ. 連絡

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

本日のツッコミ(全1件) [ツッコミを入れる]

ψ Mari [birthday-eve、一緒に祝ってくれてありがとーね♪ 漫画も貸してくれてさんきゅ☆よみはじめたよ!麻里]


2003-05-26 [長年日記]

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

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

λ. 水泳

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


2003-05-28 [長年日記]

λ. Least Fixed Point Theory

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

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


2003-05-30 [長年日記]

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

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

を借りた。

これから論文を書く若者のために(酒井 聡樹)

Tags:

λ. トゥルークライム

.

Tags: 映画