日々の流転

λ. 自分が恥ずかしい。俺は一体何をやってるんだ!?　ちょっとチヤホヤされたぐらいで調子に乗るんじゃないよ。お前ぐらいのやつなんて世の中にはゴロゴロいるんだからな。

λ. WWWサーバの移行は15日に延期か。連休中の方が移行には何かと都合が良いような気がするけどね。

λ. コラテラル・ダメージ (Collateral Damage)

を見た。全然期待してなかったのだけど、思ったよりは良かった。ただ、エンタテイメントとしても、テロの背景を描くという点でも非常に中途半端。それから、ゴーディーとマウロが抱きあう最後のシーン、何故こういう場面を作ったのか不可解。このシーンには少し胸糞が悪くなった。

λ. 知識の論理と情報検索

.

λ. 年賀嬢

面白い言葉だなと思った。今は季節外れではあるけれど。

λ. 借りた本

『代数学への誘い』

佐武一郎[著]

2/24に一度借りたけど、その時は読み終わる前に返してしまったので、また借りてきた

小説すばる 2002年1月号

-

『あやつり左近』

写楽磨, 小畑 健, 山田隆司 [著]

『ストック経済を考える - 豊かな社会へのシナリオ』

野口悠紀雄[著]

『資本主義社会の幻想 - コモンセンスとしての経済学』

ポール・クルーグマン(Paul Krugman)[著] 北村行伸[訳]

λ. Enumerable

「Enumerable#include?のようなメソッドがあることを考えると、eachは単に帰納的可算であるだけでなく、有限個の列挙で終了するという、より強い性質を要求されているように思える。」と書こうとして、[ruby-dev:8534]に気が付いた。

曰く。

Enumerableは「数え上げられる」という意味です。要求しているの は each メソッドだけで、かならずしも要素数が有限である必要は ないのですが、Enumerableモジュールは要素数が有限であることを 期待しているメソッドがいくつもあります。しかし、これは Enumerableが「要素数が有限であることを要求している」のではな く、このようなメソッドがあった方が実用上便利であるというのが 理由です。

λ. 『すべてがFになる／森博嗣』神話論

「トロイの木馬」に関する解釈に絶句

λ. クリクリs

.

λ. 冷戦と米国の新世界秩序計画 −戦後日本社会を方向づけた日米同盟の源流−

.

λ. ruby-gtk

sparc-sun-solaris2.8 のlnは非常にお馬鹿さん。正直こんなパッチが必要なのは悲しい。

--- ruby-gtk.orig/extconf.rb	Wed Jan  9 05:21:22 2002
+++ ruby-gtk/extconf.rb	Sat Feb 16 03:25:28 2002
@@ -178,7 +178,7 @@
 
 all:
 		@cd src; make all
-		@if [ ! -r gtk.a ]; then ln -sf src/gtk.a gtk.a; fi
+		@if [ ! -r gtk.a ]; then ln -f -s src/gtk.a gtk.a; fi
 
 install:;	@cd src; make install
 site-install:;	@cd src; make site-install

λ. ハッカー

ハッカー集団から脱落したあとに他分野でその経験を生かしつつしっかりとした銭儲けをなしえた人物がいたとして、果たしてハッカーさんがどういう感情を持つのか、ちょっと気にはなるところではあるんですが。

例えばゲイツ様とか? (もちろん冗談だけど)

λ. ニホンちゃん

.

λ. 僕がK君を見ていてイライラするのは、彼の中に自分と同じ弱さを見てしまっているからなのだと最近気が付いた。これからは暖かく見守ってあげよう。

λ. 拡張子

ファイルの拡張子でアプリケーションに関連づけるというのは、窓OSに限らずにわりと色々な場面で使われている。でも、ディレクトリに拡張子をつけるという話は聞いたことがない。ファイルに拡張子を付けるのならば、ディレクトリにも付けるのが自然に思えるが、いったい何故だろうか?

λ. 生け垣オートマトン: XML スキーマの形式的モデル

.

λ. 資本主義経済の幻想

• 「コモンセンスとしての経済学」という副題は気に入った
• 訳はイマイチかも。p.137に「ネットで見て 〜」という部分があるけど、 一般向きの本なのだから、普通は「ネット」って「正味」って訳すんでないの?
• 「解題」は毒にも薬にもならないので余計

λ. ねじの回転 〜 FEBRUARY MOMENT

恩田陸 の「ねじの回転」が、1月号の小説すばるで完結した。

予想を裏切る終り方。いや、そうでもないか?　ともかく連載ご苦労様でしたって感じ。

λ. Classificationと情報射の圏

19日に「チャネル理論のClassificationは情報射を射とする圏をなすようだ」と書いた。証明は簡単なんだけど、このままだとClassificationや情報射の定義を忘れてしまいそうなので、Classificationと情報射の定義を含めてメモしておこう。

定義

オブジェクト(= Classification)

オブジェクト A は、

• タイプの集合 typ(A)
• トークンの集合 tok(A)
• トークンとタイプの間の関係 ⊨_A

の組。

射(= 情報射)

射 f: A→B は、α∈typ(A), b∈tok(B) について f_tok(b) ⊨_A α iff b ⊨_B f_typ(α) であるような

• f_typ: typ(A)→typ(B)
• f_tok: tok(B)→tok(A)

の組。

射の結合

射 f: A→B, g: B→C の結合 gf: A→C を、

• (gf)_typ = g_typf_typ
• (gf)_tok = f_tokg_tok

と定義する。

恒等射

恒等射 1_A: A→A を

• (1_A)_typ = 1_typ(A)
• (1_A)_tok = 1_tok(A)

と定義する。

証明

射の結合が射になることの証明

射 f: A→B, g: B→C の結合 gf: A→C が射の条件を満たしている事を示す。

• fが射であることより、
  f_tok(b) ⊨_A α iff b ⊨_B f_typ(α)
  ⇒ f_tok(g_tok(c)) ⊨_A α iff g_tok(c) ⊨_B f_typ(α) …(1)
• gが射であることより、
  g_tok(c) ⊨_B β iff c ⊨_C g_typ(β)
  ⇒ g_tok(c) ⊨_B f_typ(α) iff c ⊨_C g_typ(f_typ(α)) …(2)

(1),(2)より、
(gf)_tok(c) ⊨_A α iff c ⊨_C (gf)_typ(α)
∴ gfは射

射の結合律

f: A→B, g: B→C, h: C→D について、

• (h(gf))_typ = h_typ(g_typf_typ) = (h_typg_typ)f_typ = ((hg)f)_typ
• (h(gf))_tok = (gf)_tokh_tok = f_tokg_tokh_tok = f_tok(hg)_tok = ((hg)f)_tok

∴ h(gf) = (hg)f

1_Aが射であることの証明

1_A: A→A は、 α∈typ(A), a∈tok(A) について、定義より明らかに、

• (1_A)_tok(a) = 1_tok(A)(a) = a
• (1_A)_typ(α) = 1_typ(A)(α) = α

よって、 (1_A)_tok(a) ⊨_A α iff a ⊨_A (1_A)_typ(α) であり、1_Aは射である。

恒等射

• f: B→Aについて、
  • (1_A・f)_typ = 1_typ(A)・f_typ = f_typ
  • (1_A・f)_tok = f_tok・1_tok(A) = f_tok
  ∴ 1_A・f = f
• g: A→C について、
  • (g・1_A)_typ = g_typ・1_typ(A) = g_typ
  • (g・1_A)_tok = 1_tok(A)・g_tok = g_tok
  ∴ g・1_A = g

∴ 1_Aは恒等射

λ. たしかに適度に勘違いしてるほうが幸せだとは思うのだけど……う〜ん。

休学も割とよく考えるのだけど、自分を高めるための当面の手段として、大学に通い続ける事以上の手段が思いつかないのが悲しいところ。

λ. 1+1=2 であることを証明できる?

ユークリッド幾何学で「正三角形の内角はすべて 60 °である」が証明できるのと同様に、「1+1=2」はペアノ算術で証明できますよん。去年の12/20に書いたペアノ算術の公理から、1 + 1 = s(0) + s(0) = s(s(0) + 0) = s(s(0)) = 2

それから、「実際，ブール代数は1+1=0 となる数学の一分野です」と書いてあるけど、そうだっけ? それってブール代数ではなくて、2を法とする演算なのでは?

λ. Classificationと情報射の圏

昨日の定義だと「対象のペア (X,Y), (X',Y') が異なる ⇒ Hom(X,Y)∩Hom(X',Y')=φ」が成り立たなかった。でも、射の定義を拡張して、⊨_X と ⊨_Y の情報も含むようにすればよいだけの事。

λ. Hassan Ait-Kaci: Warren's Abstract Machine --- A Tutorial Construction

WAMの解説としてはこの本が良いと誰かに薦められた事があるのだけど、この本オンライン版があるようです。http://www.isg.sfu.ca/~hak/documents/wam.html が元々のURLらしいのだけど、アクセスでいないので……

• http://host.di.uevora.pt/~pq/clp/wambook.pdf
• http://host.di.uevora.pt/~pq/clp/wambook.ps
• http://host.di.uevora.pt/~pq/clp/wamerratum.txt

λ. 読書

『遊戯王 28』

高橋和希[著]

λ. 夜型生活中。

λ. 数学得意?

あんまし数学得意じゃないというのは言い過ぎだったけど、少なくともそれほど得意なわけではないです。(ってか、もしそんなに数学得意だったら「総合政策学部」じゃなくて「理工学部」とかに進んでましたよー)

一応大学で一年間勉強したし、数学の先生とも割と話す機会があるので、表面的な知識はそれなりにあるけど、「数学が得意」というのはそういった表面的な知識の問題ではなくて、抽象的な対象に対する思考力/洞察力とでも言うべきものだと思う。僕はそういう点で僕はまだ非常に底が浅い(はず)。

なので、「12を2πで割るだけじゃん。なぜして、めんどくさい考え方をするのだろか」と即座に気づけるZOEさんのセンスは結構羨ましいのですよー

λ. bit別冊CLOS特集号

「一方artonさんにはbit別冊CLOS特集号を借りる。CLOS萌えるねー！」というのを見て、読んでみようかと思ったのだけど、[ruby-list:12525]によれば1989年1月のbit別冊のようだ。SFCのメディアセンタにはbit別冊は1990年以降のしか置いてないしなぁ……

【追記】 復刊.com 『bit別冊 Common Lisp オブジェクトシステム -- CLOSとその周辺』

λ. 金融数理 備忘録

阿部君の発表についていけるようにこれを読んでみようかな。

λ. momonga

ruby-fdiskなんてのがあるのか。以前に作りかけたまま放置してあるruby-partedもちゃんとするかなぁ……

λ. 巡回群とか指標群とか

n位の巡回群Gの指標群G^の指標群G^^がGとcanonicalな同型な事を理解するのに苦戦。指標群の元は準同型射(つまり関数)なので考えるのが面倒くさい。というか、こういう時こそλ記法で書いて欲しいのですよ。λ記法で書き直してようやく理解できた。

λ. tDiary国際化

そういえば、tDiaryの国際化ってどうなったんだろう。Accept-Language: を見てメッセージを切り替えれば良いのかな?

λ. 群から圏へ

ふむ。群は圏の特殊化として見れるのか。

λ. Ruby/DL

疑問。Win32 API を呼び出しているサンプルがあるけど、Win32ではcdeclではなくてstdcallを使うようになってるのかな? -fno-defer-popの効果?

λ. The Y Combinator

を読んだ。lambdaが沢山で目が回りそう。

ただ気になったのは (procedure procedure) という呼び出しがあること。単純型付きλ計算なんかだと、この手の呼び出しは不可能なはずなので、そういう場合はどうするのかな?

λ. 『ギルティ ギア ゼクス PLUS アンソロジーコミック 2』

を読んだ。

『ギルティ ギア ゼクス PLUS アンソロジーコミック 2』

せんのあき, 飛吉由耶, 銭形たいむ, 北神諒, D・キッサン, 夏代篤志, あんこきくちよ, 石見翔子, 水沢充, かわんちゃ, 多田乃伸明, 破弓翔, あきづき弥, ひせきりか, 秋霞種栄, NAO, ふしみゆうり [著]

λ. 昨日から急にWindowsのフォント回りというか、GDI回りがおかしくなってしまって、困ってる。スキャンディスクをしてみると、破損クラスタがどうだとか言っていたので、何かその辺りのDLLでも壊れてしまったのかもしれない。3/5に再インストールしたばっかだっていうのに……トラブル多すぎ!

λ. できない自分を恐れず，できる自分に溺れない

すばらしい言葉だと思う。常にそうありたい。

λ. 天使な小生意気

> 萩原先生は「今日から俺は!!」が好きみたいですね（笑）

(笑)大大大好きっス。でも「天使な小生意気」はもっと好き。

おぉ。

λ. お昼

家族で近くのロイヤルホストに。

λ. Garbage Collection for Python

Reference cycles involving lists, tuples, instances, classes, dictionaries, and functions are found. Instances with __del__ methods are handled in a sane way. It is easy to add GC support to new types. GC enabled Python is binary compatible with regular Python.

基本はリファレンスカウンタだけど、工夫して循環参照を検出するようにしているらしい

λ. ブレス2隠しイベントなどいろいろ

バルバロイと一騎討ち出来るのは知らなかった。そうか、あそこの宝箱はそうやって取りに行くのか。

λ. Dictionary of Pandaemonium

.

λ. 『ちょびっツ』

を読んだ。

『ちょびっツ 1』

『ちょびっツ 2』

『ちょびっツ 3』

『ちょびっツ 4』

『ちょびっツ 5』

CLAMP [著]

λ. パソコンと言えば……

「パソコンと言えば酒井」みたいな思い込みを勝手に流布しないで欲しいものだ。> 某方面

λ. 夕飯

お寿司。サビ抜きで頼んだのに、ワサビが入っているのがあった。がびーん。

λ. 情報射

情報射って何の訳なんだろう? Information Flow: The Logic of Distributed Systems という書名からして、Infomation Flow の訳?

λ. Kazumoto's Scientific BBS

.

λ. SFC-MODEのCommunity

CommunityをNNTPで読めたら良いのにと書いたけど、過去のメッセージの親子関係を取得するのが面倒だけど、あとは割と簡単そう。NNTPの勉強を兼ねて簡単なものを作ってみよう。

λ. カリー化(?)

class Proc
  def currying(arity=nil)
    if self.arity == 0 || self.arity == 1
      return self
    elsif self.arity > 0
      arity = self.arity
    else
      arity ||= (-self.arity)-1
    end
    
    proc = lambda{|base|
      lambda{|*a|
        args = base + a
        if args.size >= arity
          call(*args)
        else
          proc.call(args)
        end
      }
    }
    
    proc.call([])
  end
end
 
if __FILE__ == $0
  add = lambda{|a,b| a+b}.currying
  succ = add[1]
  p succ[100] #=> 101
  p succ[3] #=> 4
end

【2008-02-10追記】 [ruby-dev:33676] Suggestion: Proc#curry で遠藤さんが Proc#curry として同様(?)のものを提案している。 そこで言及されている Ruby, Proc#curry - 冬通りに消え行く制服ガールは、夢物語にリアルを求めない。 - subtech のコードは随分と妙なコードではあるけれど。

λ. 未踏ソフトウェア

萩野/服部研の人は誰も応募しないのかしら。とか書いてみるテスト。

λ. 続 Y Combinator

http://www.itlabs.umn.edu/HyperNews/get/gopalan/courses/CSCI8980-fall-2001/classwork/2.htmlを見ると、MLやHaskellでもY Combinatorを一応使えるのか。でもtrickyだ。

【追記】 トリッキーと書いたが、むしろ本質の表れた定義だろう。

λ. 情報数学Ⅱ

ミニテスト。表を読み間違えてた。見栄を張って今日提出しなければ良かった。アホだな。アホすぎる。

欝だ、寝よう。

λ. 信頼や期待を裏切ることは心苦しい。信頼/期待されない事は心が楽だろうか?

λ. Channel Theory

竹内さんの「学習の経過」。情報射はInfomorphismの訳なのか。

λ. Classificationと情報射の圏

2日の定義は間違いで、⊨_A は「タイプとトークンの関係」ではなく「トークンとタイプの関係」だった。なので、修正。

λ. UMP

まずは、Terminal object, Initial object, Product, Coproduct について考えた。ちゃんと証明したわけではないけど、多分あってると思う。関係は直積の部分集合であることの注意。

Terminal object

• typ(T) = {x} (ie: singleton set)
• tok(T) = φ
• ⊨_T = φ

Initial object

• typ(I) = φ
• tok(I) = {x} (ie: singleton set)
• ⊨_I = φ

Product

projection map を p: A×B→A, q: A×B→B とすると、

• typ(A×B) = typ(A)×typ(B)
• tok(A×B) = tok(A)+tok(B)
• ⊨_A×B = {(x,y) | x = p_tok(a), a ⊨_A p_typ(y)} ∪ {(x,y) | x = q_tok(b), b ⊨_B q_typ(y)}

Coproduct

injection map を i: A→A+B, j: B→A+B とすると、

• typ(A+B) = typ(A)+typ(B)
• tok(A+B) = tok(A)×tok(B)
• ⊨_A+B = {(x,y) | y = i_typ(α), i_tok(x) ⊨_A α} ∪ {(x,y) | y = j_typ(β), j_tok(x) ⊨_B β}

λ. SFCの近くで火事があった。煙がSFCからも見えたのだけど、残念ながらこういうときに限ってデジカメを持っていなかったので、写真を撮ることが出来なかった。

λ. representable functor

representable functor をやった。Hom(X,Y)が集合だと強調されていたのはこのためだったのか。

λ. least general unifier

Prolog の unification が most general unifier で、そのdualとして least general unifier というのがあるそうだ。例によってカテゴリ論で綺麗に扱えるらしい。……と、どっかで聞いた話だと思ったら、least general unifier は帰納論理プログラミングの授業でやったんだった。

【2006-05-15追記】 least general unifier ではなく least general generalisation が正しい。

λ. 買った本

岩波判例基本六法 平成14年版

-

自然言語処理

石崎俊[著]

Software Design 2002年5月号

-

Linux Magazine 2002年6月号

-

λ. Javaではclosureの代わりに無名クラスというのがあるらしい。

λ. SFC-MODE/NNTP

上の「最近のツッコミ」は都合によりその月の分しか表示していないのだけど、例の構想についてtakotさんという方にツッコミもらった。

とりあえず、データを取ってくるコードはそれなりで、今はNNTPについて勉強中。

λ. 人間と法

法哲学の話ですらないような「話を聞かない男、地図が読めない女」の話なんてどうでも良い。もっと役に立つことを話してくれ。

λ. 今日の向井研

チャネル理論のタイプレベルのインファレンスがグローバルカットに関係しているらしい。

それから、こないだ考えたclassificationの圏のcoproductは、most general refinement なチャネルのcoreという意味があるらしい。

あと、僕はこれまでこの日記では f_typとf_tokと書いていたけど、本当はf^∧とf^∨と書くらしい。

λ. 規模が小さくてソースの読みやすいオープンソースのコンパイラってどっかに転がってないかな。

λ. 私の景気対策

What My Home Page is. の 2002/05/06(mon)02:38:01 の「私の景気対策」が素晴らしい。

Internet Archive

λ. 夢

今のうちに密かに卒論を書いておくという夢を見た。よくわからないテーマだった。

λ. monomorphismかつepimorphismはisomorphismの十分条件じゃない

monomorphismかつepimorphismはisomorphismの十分条件じゃないって事は、monomorphismであってもretractionが存在するとは限らないし、epimorphismであってもsectionが存在するとは限らないって事か。そうか、そうだよな……

λ. Java

少し勉強をはじめた。誤算があって、思ったよりも早くtomcatのソース読みの順番が回ってきそうなので。

λ. Parametric-types for Java

そういえば、以前に石原君に「Javaはstatic-typedなのにparametric-typeが無いのが嫌なんだよねぇ」と言ったら、genericityってのが入るらしいと教えてもらったのだった。なので、少し探してみたら、GJ - A Generic Java Language Extension というのを見つけた。これこれ、こーゆーのが欲しかったのよ。

それと、Parameterized Types for Java という論文を見つけた。

λ. σ-calculus

それから、Javaとは関係ないが、オブジェクト指向言語を形式化した object calculus(σ-calculusとも呼ぶらしい)という計算モデルがあるらしい。これまで、オブジェクト指向って、どうも理論的な根拠が薄弱で、宗教的というか、経験論的というか、要する胡散臭いと思ってたんだけど、ちゃんとした理屈もあるんじゃないの。

Sigma Calculus Interpreter

σ-calculusのインタプリタ。わりと面白そう。

λ. おしゃれ泥棒 (How to Steal a Million)

を見た。

λ. お勉強ノート

Atsushi Yamaguchi 氏のカテゴリー論のまとめ等がある。

λ. Rubyのこんな所は今更変えられないよねぇのこーなー

去年の11/17に書いたけど、僕も文字列の結合は「+」よりは「*」が自然だと思う。というか、むしろ繰り返しを「**」で表現したいというのが本音だけど。

λ. 借りた本

『ていうか 経済って難しいじゃないですか』

中尊寺ゆつこ[著]

『最後の特派員』

ダニエル・スティール (Daniel Steel) [著]

λ. rubyでmontague文法?

「現在取り組んでいる課題はmontague文法をRubyで表現すること」と書いてあるのをみつけて、その後どうなったのかが気になった。モンタギュー文法についてのページも興味深い。

λ. だらだら

λ. ローソンに行って、頴娃圏英検の¥5,500を払ってくる。便利になったものだ。

λ. 履修申告確認表に「至急窓口に来てください」と書かれていたのをすっかり忘れていたので、だいぶ経ってしまってたけれど窓口へ行ってみる。

λ. システムプログラミング

演習問題とか真面目に解いていると、だんだん不毛な気分になってくる。でも、授業時間中に解けないと、解答例と自分の解答を比較考察する宿題に変化するので、一応解いて回避離脱。

λ. 論文読み会 "Rethinking /dev and devices in the UNIX kernel"

加藤さんの発表。jail(2)への愛が感じられる論文でした。なんでjailにこんなにもこだわるのかと思ったら、著者はjailの作者だったらしい。ありゃまぁ。

λ. ゆっけsong

某方面へ。ゆーすけべー日記 (2002-05-13) より

λ. T-coalgebra

あう。有限状態オートマトンがcoalgebraになるという話は情報数学Ⅰでちょっとやったけど、T-coalgebraなんて知らないにょ。多分T-algebraのdualだとは思うけど、T-algebraといえばmonadの出てくるアレなわけで……

というか、いきなりそんな授業やるなんて、ずいぶん飛ばしてるなー　さすが大学院の授業(!?)

λ. yasuf's page

高校の同級生だった平川君のページ。

λ. Lawvere の不動点定理 (Lawvere's diagonal theorem)

[ruby-list:35060]で原さんが「Lawvere の不動点定理」という定理を紹介している。

どっかで見たなと思ったら、こないだまで読んでいた「Conceptual Mathematics」だった。この本の著者は F. William Lawvere と Stephen H. Schnuel だったりする。で、以下に引用。

Diagonal Theorem:

(In any category with products) If Y is an object such that there exists an object T with enough points to parameterize all the maps T→Y by means of some single map f:T×T→Y, then Y has the 'fixed point property': every endomap α:Y→Y of Y has at least one point y:1→Y for which αy=y.

関連エントリ

• 「自己言及の論理と計算」
• A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points

λ. jmk = Make in Java

jmkという文字列を見て、一瞬saimuneさんのアレかと思ってビックリした。

λ. MFモデル

国際マクロ経済学の基本モデルに「マンデル・フレミング・モデル」というのがある。このモデルでは増税や公共事業削減等の緊縮財政は円安を導く。

λ. Cと末尾再帰の除去

VC++はtail recursionの除去をしてくれるとどこかで聞いた。gccにも-foptimize-sibling-callsというオプションがあるようだ。これらは一体どうやっているんだろう?

stdcallならば、スタックフレームの巻き戻しは呼ばれた関数側で行うことになっているので、末尾の関数を呼び出す前にスタックフレームを巻き戻してしまえば良さそうだといのは分かるのだ。だけど、cdeclのようにスタックフレームの巻き戻しが呼び出し側の役割の場合は、単純な末尾再帰はともかく相互再帰等を除去できないのではないだろうか?

λ. 婷婷と話してて、彼女の所属している研究会はずいぶん研究っぽい研究をしてるなぁと思いました。それに比べて……

λ. プログラミング言語論

Pascalのポインタ演算子は「^」(ハット)だと思ってたんだけど、本来は「↑」で、Pascalの教科書ではそう書いてあるのが多いらしい。

「型は、値の集合と、その値への操作から構成される」とあるけど、そういう素朴な概念だけではなくて、他のモデルについても示して欲しかったと思った。こないだ読んだ On Understanding Types, Data Abstraction, and Polymorphism の 3. Types are Set of Values の最後の方に、retract model と second-order λ-calculus の事が少し言及されていたので、気になっている。

λ. PTQ

片山さんのPrologによる実装が登場。公開をリクエストした甲斐があった。

λ. 情報数学Ⅱ

先週失敗したので欝だ。

λ. tomcatソース読み

研究会で、発表者がいなかったので、代わりに僕が src/share/org/apache/tomcat/util/http を読んだ。場所は、Javaを知らなくても全く問題なさそうな所を選んだ。それにしても小賢しい最適化が多くてウザい。

λ. kinukoレンジャ

某所ので行われたしょーもない会話。

• 「研究会の男女比を改善するのは来期の課題ってことで」
• 「でも、使えない人が入ってきてもらってもなー」
• 「逆に、安田さんみたいな人ばっかり入ってくるってのも、どうかと」
• 「研究室のドアを開けたら、5人の安田さんが振り向いたりして?」
• 「全員色違いだったりしてね」
• 「きぬこレンジャ?」
• 「安田ブラック、安田ブルー、安田レッド、安田ピンク、安田イエロー ...」
• ...

λ. Mita Logic Seminar

今日は三田で竹内外史の「Gödel Sentence」というタイトルの講演があったのだけど、授業があったので行けなかった。残念。こういうのって何で平日が多いのだろう。

λ. ソフトウェア基礎理論

離散数学やソフトウェア基礎論理学に関するページです。東大工学部の講義「ソフトウェア基礎理論」の内容とリンクしています。たくさんあるプログラミング言語の、根底の部分についてです。ソフトウェア設計やさんはこういう論理学についての知識を身につけておくと、きっと役に立つと思います。

遠山さんの日記より。

λ. 喉が痛い。これはまた風邪をひいたかな。

λ. 米田のコラッツ予測

午前中はこれについて考えてた。「どんな数でも、それが奇数なら3倍して1を足し、偶数なら半分にするということを続けていくと最後には1なる」という例のあれ。簡単そうに見えて、難しい。これまで証明されていない(よね?)だけのことはある。

λ. お昼

スカイラーク・ガーデン

λ. Webサーバの移行

すっかり忘れていて色々と焦ったけど、今日からSFC生の個人ページのWebサーバがwww.sfc.keio.ac.jpからweb.sfc.keio.ac.jpに変更になったそうです。変更は恒久的だと思います。

λ. GDBMのフォーマットはアーキテクチャ依存

RuBBSがGDBMを使っていたのだけど、急に bad magic number とか言われて焦る。原因は、WebサーバのアーキテクチャがSolaris/sparcからLinux/ix86へ変更になった事。gdbmのフォーマットがアーキテクチャ依存だったなんて初めて知ったよ。tranDBをのconvGDBM2ASCとconvASC2GDBMを使って変換を試みるも、うまく変換してくれないようだ。仕方ないのでPStoreにダンプして対処する事に。(gdbm2pstore.rb, pstore2gdbm.rb)

λ. SuExec

CGI/SSIの実行権限がSuExecになった。それで、所有者がnobodyのファイルがあった場合の対処法に、「nobodyのファイルは削除することはできても」とあるけど、空でないnobody所有のディレクトリはどうやって消せばよいんだろう。とりあえずどけておく。UNIXは奥が深いな。

λ. 『らむだ天国』

kitajさんや、たださんも書いてるけど、これは頭から離れなくなりそう。知り合いに紹介したらかなりうけてた。

λ. ラムダが見苦しい

ところで、Haskellではλはバックスラッシュなので、沢山使うと見苦しい。「¥」に化けるともっと見苦しい。

λ. Classification と Infomorphism の圏: SubObject

いきなりだけど、fx=fy ⇒ x=y を満たす射fを monomorphism と呼ぶ。そのdualとしてepimorphismが定義される。すなわち、xf=yf ⇒ x=y を満たす射fを epimorphismと呼ぶ。

monomorphism i: S→X が存在する場合に、SがXのSubObjectであるという。このiをSのXへのinclusion mapと呼ぶ。

SubObjectは、集合論での部分集合に対応する概念なんだけど、カテゴリ論ではオブジェクトの内部について考えないので、このような定義になっている。集合の圏を考えると、この定義はSの要素を写像iによってXの要素と見なせるという事を意味する。

で、情報射 f が monomorphism になる条件は、情報射の定義から明らかに (f↑x↑=f↑y↑ ⇒ x↑=y↑) ∧ (x↓f↓=y↓f↓ ⇒ x↓=y↓) で、つまりタイプレベルの射が集合の圏でmonomorphismで、かつトークンレベルの射が集合の圏でepimorphismである事である。

ところで、集合の圏ではepimorphismであることとsectionが存在することが同値だった。なので、f↓がepimorphismであるとき、f↓s = 1_tok(A) となる section s: tok(A)→tok(B) が存在する。sx=sy ⇒ f↓sx=f↓sy ⇔ 1_tok(A)x=1_tok(A)y ⇔ x=y より、このsはmonomorphismである。

したがって、AがBのsubobjectであるとき、typ(A)は集合の圏でtyp(B)のsubobject、tok(A)は集合の圏でtok(B)のsubobjectになる。情報射を構成する写像の向きは逆だったのに、こっちは逆になっていないというのはちょっと面白かった。

λ. 原さんに敬意を表して「ヒビルテ」というタイトルにしてみる。

λ. ウルト・ヒケウ 萌え。とか書いてみるテスト。(2006-05-18追記: Googleイメージ検索でウルト ヒケウで検索しても一件も引っかからないのは非常にけしからんと思う。)

λ. ts日記の「コトの真相（私見）」が興味深い。

λ. 三田絵美子さんの日記の5/15に「数学と論理のSAもだいぶありえない。つかえない…。」と書かれていて、自分の事かと一瞬びびった。

λ. WindowsディベロッパのLinux感

COMは，なぜもっと簡単に使えるように提供されなかったのかを考えると残念でなりません(stdioに近いレベルの概念になっていればよかったのに)．

結構同感。仕方ないとも思うけど、もう少しなんとかならなかったかなぁとも思うんだよなぁ。 簡単さといっても、開発環境がテンプレートとかの機能を充実させて実現されるような「簡単さ」じゃなくて、それこそstdioを使うくらい気軽に使えるようになっていれば……

λ. x += y

C等の言語では「+」のような2項演算子について、「x = x + y」を「x += y」と略記出来る。どうせならば、演算子に限らず、YのX上の任意のアクション f: X×Y→X について「x f= y 」と書けるようにしたらどうだろうかと一瞬思った。

λ. 今日のインストール

ocaml-3.04

-

Coq-7.2

config/coq_config.mlに「\n」が入ってしまって構文エラーになってしまうので、そこだけファイルを編集してコンパイル。本当はconfigureを編集すべきなんだけど、ocamlわかんないんで。
それから、例のお馬鹿lnへの対処。

λ. Classification と Infomorphoism の圏

情報射の条件として「f↓(b) ⊨_A α iff b ⊨_B f↑(α)」というのはやはり扱いにくい。そこで、⊨_Xを tok(X)×typ(X) から Ω = {true, false} への写像 ψ_X と考えて、射の同一性で言い換えると「すべての <α,b>: X→typ(A)×tok(B) について、ψ_A <f↓b, α> = ψ_B <b, f↑α>」になる。あんま変わらないか……

情報射を構成する写像を、最初は「f_typ, f_tok」と書いて、次に「f^∧, f^∨」と書くのが正しいと知って、昨日は書き易そうだったから「f↑, f↓」と書いてみたりと、色々な書き方をしてしまったけど、どうせならtypとtokをそれぞれ集合の圏への covariant functor と contravariant functor と考えてしまって、「typ(f), tok(f)」と書くのが良さそうな気がしてきた。何でこう表記しないんだろう。

functorといえば、4.Type-Token Dualityのflipも contravariant functor で、しかも involution だよね。

λ. あと、とりあえずは ruby-parted かなあ。。。

おぉ。libparted-rubyを引き取ってくれると嬉しいなぁ。

λ. 六法全書と朝鮮語の辞書を間違えて持ってきてしまった。欝だ。

λ. 人間と法

法的に問題がある事を「瑕疵(かし)」と呼び、その対処には「無効」と「取消」という2通りがある。「無効」は絶対に無効なのだけど、「取消」は一応の有効性を認めたうえでの対処。

λ. 自然言語論

強化文脈自由文法(augmented context free grammar)というのがあるそうだ。

λ. section, retraction, monomorphism, epimorphism

今日は section, retraction, monomorphism, epimorphism の辺りについて説明した。今回は準備不足で思うようにいかなかった。板書ミスをしまくるし、どうもコワレ気味。でも、正直この辺りの話はあまりやる気がしないんだよなぁ。早く発表したい部分に辿りつけるように、次回は頑張ろう。(発表資料)

石原君の発表で、自然演繹の紹介があったのだけど、「∧」と「⇒」の除去規則が知らない形で定義されていたのが面白かった。

 A∧B
─── (E∧)
  A

 A∧B
─── (E∧)
  B

 A⇒B  A
───── (E⇒)
     B

        [A,B]
          :
          :
  A∧B    C
─────── (E∧)
       C

          [B]
           :
           :
  A⇒B  A  C
─────── (E⇒)
       C

λ. カテゴリカルロジック

ロジックを、自然演繹やシーケント計算の代わりに、カテゴリ論的に扱ってやることが出来るらしいという話を聞いた。なるほどと思った。直感的には、命題をオブジェクト、命題間の導出を射とするようなカテゴリを考えれば良いのかな。Terminal Object を恒真、Initial Object を恒偽、Productを「∧」、Coproductを「∨」、Mapping Object を「⇒」と考えて……、あれ? 「¬」は?

[2005-05-29追記] もちろん「0^A」を「¬A」と考えればよい。

λ. 夕食

家族で「さぼてん」へ。

λ. ハムナプトラ / 失われた砂漠の都

を見た。蟲が怖かった。虫の映像が全く素晴らしい。これは夢に見そうだ。でも、スカラべ(糞転がし)って肉食だっけ?

ついでに、イムホテップという名前は、"這い寄る混沌" ナイアルラトホテップ を連想する。

λ. X・Files / ファイト・ザ・フューチャー

3月に撮っておいたのを見た。主立ったキャラクタはすべて登場してるし、スモーキングマンの回想のような形でストーリーが語られるのも良かった。日曜洋画劇場でやったなかでは一番面白かったと思う。

角田さんの日記が詳しい。

λ. Ruby 程式語言 (中国語繁体字)

紅眠の愛の秘密日記より。

λ. ネットカルチャーの代表が2チャンネルというのはどうかと。

λ. カリー化

以前に、どこかのサイトでSchemeの関数を自動的にカリー化しようという話題を見掛けたのだけど、どこだったかな。多分Gauche方面だったような気がするけど、今探したら見つからなかった。

λ. プリンタ

PCに繋がっているのに「プリンタが接続されていません」と言われるようになった。他のPCに繋いでも同じ症状なので、プリンタが壊れたのだろう。あー、面倒だ。

λ. 借りた本

『日本経済起死回生トータルプラン』

石原伸晃, 塩崎恭久, 根本匠, 渡辺喜美 [著]

『英国庭園の謎』

有栖川有栖[著]

『星方遊撃隊　エンジェルリンクス　銀河爆闘編』

伊吹秀明[著] 幡池裕行[イラスト]

『R.O.D』

倉田英之[著] 羽音たらく[イラスト]

λ. 今そこにある危機

を見た。

λ. IsaViz: A Visual Authoring Tool for RDF

RDFを視覚的に記述できるツールらしい。

λ. 米田の補題

ようやく米田の補題について理解した……ような気がする。そういえば、目標は米田の補題!とか書いていたのが2月だった。もう3ヶ月も経ってしまったのか……

λ. 冬山に登りに出かける夢。家を出てバイクにまたがったら雪が降ってきた。外はもう暗くて、冷えた空気が頬に当たるのが心地好い。

λ. ウィッシュリスト

zoeさんの真似をして、Amazonでウィッシュリストを作ってみた。私に貢ぎ物を贈る際には参考にするように(笑)

λ. システムプログラミング

DDD使おうぜ。(ぼそっ

λ. 論文読み会 "Chord: A Scalable Peer-to-peer Lookup Service for Internet Applications"

.

λ. 健やかな立ち姿勢?

ネコ背直したいなー。

λ. UNIXを教える意味

「(Windowsから)逃げ出したってそこに楽園があるわけじゃないんだよ。というか、むしろ WindowsにUNIX、世の中腐ったシステムしかないんだよ。」……というのを教えるためという気もする。ちょっとだけ。

λ. Method#to_procがarityを保存してくれない

Method#to_procを呼び出すと、arityが常に-1になってしまう事に気が付いた。これはこういうものなのかな。

irb(main):001:0> RUBY_VERSION
"1.6.7"
irb(main):002:0> method(:require).arity
1
irb(main):003:0> method(:require).to_proc.arity
-1

λ. 『まほらば 1』. 小島あきら

を読んだ。

λ. 「ヘルシング」と「大同人物語」の作者が同一人物だと知ってショックを受けている今日このごろ、皆さんどのようにお過ごしでしょうか?

λ. 酒井大明神

私は「酒井大明神」らしい。大明神と権現さまはどっちが偉いのかな?

λ. Coalgebra に基づく有限オートマトン理論の再構成(概要)

を眺めてみるが……む、難い。

λ. プログラミング言語論

言語の評価が、Javaに近い言語とそれ以外でダブルスタンダードになっているような気がするのは気のせい?

λ. 情報数学Ⅱ

わけわからなくなってきた。ちゃんとした確率論の教科書を読まなくちゃついていけなさそう……

λ. 萩野先生と一緒に歩くUFO

萩野先生と一緒に歩くUFOが……*1

λ. クリスチャン

「例外がきたら、みんな神様にthrowすればよい」と某氏が言っておりました。もちろん冗談でですよ。

λ. FreePascal

{$packrecords C}を指定すると列挙型もCと同じサイズになるみたい

λ. Parted-1.6.0

のソースを見た。Partedのソースを見るのは久しぶり。PedGeometryがPedDiskへのポインタではなくちゃんとPedDeviceへのポインタを持つようになってる。

autoconf 2.50 以上が必要なのか。どうせなので Asumi を入れるか。

λ. 『計算機プログラムの構造と解釈』 第二版. Harold Abelson, Jerry Sussman, Julie Sussman [著] 和田英一[訳]

有野さんと高林さんがSICPについて書いているのをみて、読んでみたくなった。とは言っても全文をオンラインで読むほどの気力も無いので、借りてみた。

λ. 自分の関数名を取得する方法

C 言語の研修より。C言語で自分の関数名を取得する方法は __func__ かな。自身の関数ポインタを取得する方法はちょっと知らない。

λ. 秋田　禎信　「魔術士オーフェンはぐれ旅 - 我が館にさまよえ虚像」

Quotation

―「分かりません。分かりません……でも、力を持つことに意味を求めてはいけないんですか?」

λ. ストック経済論

遺産を「世話をしてくれたものにより多く」と考える比率が女性の方が高いのは何故かというクイズ。僕は「日本の平均寿命は、男性が77.10歳、女性が83.99歳であり、しかも夫婦の年齢差の平均が3歳差でしかない事が知られている。そのため、『配偶者に先立たれ子供の世話になる』という事態を、女性の方が現実的に捉えているのではないか?」と答えてみた。実際のところどうなんだろ。少し気になる。

λ. 読書

「ななか 6/17」 1

「ななか 6/17」 2

「ななか 6/17」 3

「ななか 6/17」 4

「ななか 6/17」 5

八神健[著]

λ. あなたを株化してみたら

をやってみた。

判定結果

あなたの10年後の推定株価総額は 3827 万円です。
あなたの資本金は3050万円で、 現在の株価総額は3548万円です

あなたの株に対する総合評価は aです。
ごく普通の評価が出たあなたの株は、これから先ごく普通の値動きをするでしょう。 市場動向や物価の変動により値を上げることはありますが、大きな飛躍は期待出来ません。 思いきった方向転換で一発狙うもよし。このまま堅実にいくもよし。

あなたの将来性に対する評価は aaです。
比較的将来性豊かなあなたは、ともすれば現状に満足しがちです。 異性に対するのと同じくらい情熱的に取り組めるものを見つけましょう。

あなたの人間性に対する評価は aです。
Q12でたくさんのチェックをしてこの評価になった方は多くの長所と多くの短所を持っています。 逆にあまりチェックしなかった方は、長所もなければ短所もない特徴のない方かもしれません。 いずれにせよこれからは個性の時代。魅力的な人間性を身につけるべく努力が必要です。

あなたの運に対する評価は bです。
いまいち運に恵まれないあなたは、これから先さまざまな不条理に出会うでしょう。 しかし「最悪」ではないので、「世の中もっと不運なヤツがいるんだから」と思って 精進しましょう。世の中捨てたものではありません。

各評価は最高が「aaa」以下「aa」「a」「b」の順で最低が「c」です

λ. 真夜中は別の顔

最終回。やはり「夜明けの夢」の方もNHKでそのうちやるのだろうか?

λ. Ruby-GNOME2

[ruby-ext:02081]によるとCVSレポジトリが出来たそうなので、早速取ってきてRuby/Gtkをコンパイル。こんなパッチが必要だったけど、例によってシグナル周り以外はそれなりに動いている模様。

僕のところではその問題は発生しませんでした。

λ. SFCの大学院に入りたいという人が京都から来ていた。

λ. 『蟲師 1』 漆原 友紀

を読んだ。

λ. 『7日間完成　英検1級予想問題ドリル』

を買ってみた。

λ. 今日の向井研

分解体の話、わけわからん。

手作業で簡単な圧縮データを展開してみたり。なかなか面倒だったけど、面白いかも。

Link Grammer 面白い。かかりうけ文法に似てる?

「スピーディ」。ものは言いようだ。

チャネル理論でSumが出てきたけど、この辺りはやっぱカテゴリ論的な説明の方が見通しが良いなと思った。

λ. 湘南混声合唱団のコンサートを聴きに行った。

λ. Ruby/Gtkと複数のウィンドウシステム

gtk2では異なるウィンドウシステム用のバイナリが共存できるようになっているらしいので、Ruby/Gtkでも対応する拡張ライブラリを共存させられると良さそうだ。そのためには、以下のようにしてインストールされているライブラリを列挙してやって、それぞれについて拡張ライブラリをビルドすれば良いのかな。

`pkg-config --list-all`.scan(/^(gtk\+-(\S+)-([^\s-]+))/){
  |pkg, window_system, version|
  ...
}

ただ、現在のextconf.rb/mkmf.rbの仕組みだと、単一のソースから複数の拡張ライブラリをビルドするようなのを書きにくい気がする。

そんな事しなくても、単にインストールする人にウィンドウシステムごとに「GTK_CONFIG='pkg-config gtk+-linux-fb-2.0' ruby extconf.rb && make」とかしてもらえば良いのか?　いや、共存を考えるとファイル名を変える必要があるし、ファイル名を変えると初期化用の関数の名前も変えなくちゃいけないので、Ruby/Gtkの細工はやっぱ必要か。まあいいや。後で考えよ。

requireするときの名前をどうするか?　ウィンドウシステムを明示したい場合と明示したくない場合がある。明示したくない場合は「require 'gtk2'」等とすることになるだろうけど、こいつはどの拡張ライブラリをロードするのか?

現在サポートされているのはx11/linux-fb/win32だけなので、例えば、Win32環境ならばwin32、環境変数DISPLAYが設定されていればx11、Linuxならばlinux-fbという順番で探すとか……

λ. FreeBSD-users-jp のアレ

なんというか……哀れ。でも、kitajさんやどかにゃさんも書いてるけど、この「論文」は「実存主義数学」とか、なかなかツボをついた文章で暇潰しに良さそう。

ところで、[FreeBSD-users-jp 68653]で紹介されている『エキスパートCプログラミング―知られざるCの深層』は面白そうだ。

λ. 遠雷。どことなく不安をかきたてられる。

λ. 眠い。ストック経済論のレポートが書けなくて苦しい。統計を読むことに慣れてないのがまず痛いし、歴史的な背景についての知識が足らないのも痛い。

λ. システムプログラミング

シェル作り。馬鹿にしてたけど意外と楽しいかも。リダイレクションの仕組みを知らなかったので、その辺りは勉強になった。

気がついたら盛大に寝てしまっていた。ごめんなさい。

λ. 『全日本妹選手権 2』 堂高 しげる

を読んだ。

λ. ANSI

アンシーってゆーなっ

λ. ストック経済論レポート

なんとか絞り出した。締め切り5分前くらいに書き終えて提出。時間がなかったのでLaTexに出来なかった。他にも不満だらけの代物。

でも、バランスシートを色々といじくりまわしてて、どこをどう見れば良いか勘所が少し分かってきた気がする。これを24時間くらい前までに出来ていれば、もっと自分的に納得のいくレポートを書けた気がするなぁ。

λ. 夕方まで寝てた。これでここんとろこの不足分を取り戻したぞー

λ. TinyC

こないだkjanaさんに紹介してもらった TinyC のコードにざっと目を通した。さて、どこから弄るかな……

λ. 誤変換

「総資産」を「荘子さん」と誤変換。あうあう……

λ. 続^2 Y Combinator

[ruby-list:35060]のFは、自分自身が定義域になっているようなnon-well-foundedなタイプなので考えにくくてしょうがない。

こういうのって、超集合論(hypersets)とかを知ってると、わりと楽に考えられたりするのだろうか?

λ. ところで、Y Combinator のようなトリッキーな事をしなくても同じことが出来るような仕組みを大抵の言語は持ってるのね。

Schemeではletrecを使う

(define fact
  (letrec ((f (lambda (n)
                (if (zero? n)
                    1
                    (* n (f (- n 1)))))))
    f))

Haskellのletは他の言語でのletrecに相当する

fact =
    let f n = if n == 0 then 1 else f (n - 1) * n
    in f

Common Lisp だとlabelsを使う

(defun fact (n)
  (labels
      ((f (n)
          (if (zerop n)
              1
              (* n (f (- n 1))))))
    (f n)))

Smalltalk

使ったこと無いけど、thisContextという特殊変数でブロック自身を参照できるそうだ。

λ. だるい。

λ. 数学と論理

去年やらなかった話としては、M.V.Glivenkoの定理の話があった。これは古典論理の定理に二重否定(¬¬)を付けてやると直観主義論理の定理になるという話。つまりは、古典論理を直観主義論理に「埋め込む」事が出来る。

λ. ストック経済論

株価のファンダメンタルズ理論の基礎。まあ常識でしょ。

λ. アルゴリズム論

教職を首になる三つのアルゴリズム

1. 入試情報を洩らす
2. セクハラ
3. 論文の剽窃

メフィストフェレスの円舞曲おもろい。

BNFは数学的な意味でのNormal Formでないらしい。ところで、Chomsky標準形やGreibach標準形はNormal Formなのかな?

λ. SWI-PrologとXPCEで遊ぼう!

Webアーカイブ上のもの

λ. バグが僕らを待っている おう!

……

λ. シグマ計算

「シグマ計算って〜」というような会話を耳にして、「おっ、例のσ-calculusか」と思ったら、合計を表わす∑の話だった……

λ. あろ〜むで夕食

これが話に聞く、あろ〜むか。

λ. 今日の向井研

一部のPrologの処理系はfreezeという述語を持っていて、これは lazy evaluation のために使われる。

発表資料。