日々の流転

λ. 「脳心一体論と脳心異体論」 (創作日誌 2001/09/04)

ところで、波は媒質と一体ですか?

λ. default.el

そうだったんですか、勉強になります。で、~/.emacs.elに以下のように書いて解決。

(setq inhibit-default-init t)
(load "default")
(setq auto-mode-alist
      (append
       '(("\\.html$" . html-mode))
       auto-mode-alist))

λ. C#

Delphi作った人が作っただけあって面白い言語だとは思うけど、ダサイとこもあるなー。…というか、言語自体よりも、COMや.NETと結び付いているところが羨ましいんだよな。つうか、CORBAややこしいっすよ。

λ. もうショートカットを覚える必要なし (yendotより)

なにこれ…

λ. 不景気はどこから来るか (ぽへへ〜ん 03/09/2001)

不景気の定義は2期続けて産出が減少すること。まあ、世の中色々あるから、産出が増えることも減ることもあるでしょ、きっと。

λ. reach UTF-8 nirvana

UTF-8を解脱してCSIの境地に達し…無いか。(嘆息)

λ. もう秋ですね…秋といえば (/.J)

デバッグの秋はちょっと寂しいねぇ。僕は読書かな。

λ. 夢

友人たちと、どこかのテーマパークに遊びにいく。冗談で何かのクジに参加したら、偶然に偶然が重なって、約1億6千万円ほどの権利が……

すげーラッキーと思ったら、夢だったのか。あーあ。

λ. arabic in mongol

最近のmltermは使ってなかったので良く知らないのですが、mongolということはきっと左から右に改行するモードですよね。そこにアラビア文字等を埋め込む場合、単に反時計周りに90°回転させれば文字の表記方向も改行方向も合うので、下から上に書く事は無いと思います。このモードで下から上に書くとしたら、ラテン文字等(左から右に書いて、上から下に改行する)を埋め込む場合でしょう。……勘違いしてたらすいません。

この辺りの話は、以下の文献がまとまっていて良いと思います。

• 片岡裕:"国際化・多言語化の基礎と実際[前編]", Bit Vol. 29, No. 3 (1997-3).
• 片岡裕:"国際化・多言語化の基礎と実際[後編]", Bit Vol. 29, No. 4 (1997-4).

λ. コンパイル猿

進んでないなぁ。

λ. cygextras-0.3.3

当然問題なし。

λ. ORBit2-2.4.3

とりあえず必要そうなコードをstevenのORBit-0.5.17-cygwin.patchから切り張りしてコンパイルする。orbit-idl-2.exeの吐くコードがauto-importの制限に引っかかるので適当に誤魔化した。ORBit2-2.4.3-cygwin-20020906.patch

IDLから必要なファイルを生成してくれなくてコンパイルエラーになるので、Makefile.sharedの「%.h %-stubs.c %-skels.c %-common.c %-imodule.c %-skelimpl.c: $(IDL_DIR)%.idl $(IDL_COMPILER)」という行から「$(IDL_COMPILER)」を除いてみたら生成してくれた。

λ. ムーアとブッシュとフセインのある一日。

N.* D.* E.* (2004-08-31) より

λ. 『第二次大戦とは何だったのか?—戦争の世紀とその指導者たち』, 福田 和也

読了。

λ. 人狼BBS

灼燦灼丸裏kdoo王国(2004-09-03)より。うわっ、すごいなこれ。試しに幾つかの村のログを読んでみたのだけど、むちゃくちゃ奥が深いなぁ。夏休み中に1,2回プレイしてみたいところだ。

λ. 記憶（memo）する関数

「同じ変数に束縛されたものは二度計算されることはない」という性質を利用したメモ化で、同じ問題を書いてみる。memocc2.hs

参考

• [haskell-jp:695] 「情報処理」8月号 連載:Haskellプログラミング
• Representations of First order function types as terminal coalgebras

λ. ボルツマン没後100年

昨日熱力学のことを書いたが、実は今日はボルツマンの没後100年目の日だったそうだ。そして、このことは偶然見たex-constさんの雑記帳(2006-09-05)で知った。小さな偶然が二つ。

• Ludwig Boltzmann - Wikipedia, the free encyclopedia

λ. 今日の英語: represent

The Japanese government is represented at the conference.

「日本政府は会議に代表を送っている」という意味だそうな。 representってこういう使い方もするのね。 知らなかった(バカ)。

λ. Xiph QuickTime Components (XiphQT)

RubyKaigi2006の音声ファイルが Ogg Vorbis だったので、iTunesで聴くためにインストールしてみた。

λ. Constructing M-types from W-types

Containers: constructing strictly positive types の話。

先日、「W-typesによる帰納的データ型の表現」で書いたように、W-typesは整礎(wellfounded)な木のデータ型になっている。 そして、Wa:A. B(a) は関手 T(X) = Σa:A. B(a)→X の最小不動点になっている。 最小不動点があれば当然最大不動点も考えたくなるもので、それがM-types。 Ma:A. B(a) は T の最大不動点で、整礎とは限らない木のデータ型になっている。 ちなみに、名前はM-typesはW-typesの双対だから「W」を上下反転した「M」を使ったのだろうと思う*1。

で、M-typesはW-typesとは別に追加しなくてはいけないかと思ったら、実はMartin-Löf圏ではW-typesから構成することが出来るそうだ。 無限木を深さnで切ってそこをダミーの値に置き換えると有限の木になり、逆にnを大きくしていった時のそのような有限の木の極限が元の無限木と考えることが出来る。なので、元の無限木を直接扱う代わりに、そのような有限の木の族として扱う。有限の木はW-typesで表現出来るので、M-typesはW-typesで表現できると。

イデアル完備化との関係?

こういう話を聞いて連想するのは、Jiří Adámek の Final Coalgebras are Ideal Completions of Initial Algebras で……

後で書く。

Agdaによる実装

M-types.agda (作業中)

後で書く。

λ. 「型の型」問題

LL Future のスタッフ&発表者の打ち上げ*1で「型の型」についての話が出たらしい。 あろはさんのTwitterの<URL:http://twitter.com/alohakun/statuses/904102768>や、東京行ってきた - 黎明日記とそのコメント欄で、その辺りの話が出ていたので、ちょっと簡単な説明を書いてみる。

HaskellとかCCの場合

まず、Haskellの場合。 Haskellでは型の型は「種(kind)」と呼ばれていて普通の型とはレベルの異なるものになっている。つまり、型の型は普通の型ではない。

種について簡単に説明する。 例えば、Bool や Maybe Bool などの型は * という種に属する。 また、Maybeという型構築子は * に属する型を受け取って * に属する型を返す関数なので、*→* という種に属する。また、一般化薔薇木のデータ型 data GRose f a = GBranch (f (GRose f a)) で定義される型構築子 GRose は (*→*)→*→* という種に属する。 種の存在意義は型をパラメータとして受け取るような何かを型付けすることだ。 Haskellの場合にはその「何か」には、Maybe :: *→* や GRose :: (*→*)→*→* のような型構築子と、[] :: ∀a::*. [a] や map :: ∀a::*. [a]→[a] のような多相的な式との二つがある。

このようなHaskellの型システムの背景にはFωやλωと呼ばれる型理論が存在していて、Fωにさらに依存型を追加するとCC(Calculus of Construction)やλCと呼ばれる型理論になる。

ところで、型の型が種なら、種の型はなんだということになるが、CCではそれは考えないし、λCでは便宜的に定数記号 □ に属するということにしている。 何故かというと、これらの型理論では種を受け取る「何か」を扱わないから、種の型を考える意味があまりないため。

AgdaとかCoqの場合

CCのような型理論とは毛色の違う型理論もある。

例えば、Agdaの型理論では通常の型はSetに属するがSet自身はSetには属さない。その代わりSet1という型があり、これがSet1を要素かつ部分として含む。さらに、Set2はSet1を要素かつ部分として含み、Set∈Set1∈Set2∈… という風に型の宇宙が累積的階層をなしている。 ある階層に属する型を集めた全体(型の型)は、その階層自身には属さずに一つ上の階層に属するものになる。 つまり、「型の型」は同じレベルの型ではない。

一方、Coqの型理論では通常の型はSetに属してSetはTypeに属している。そして、Typeは構文的にはType自身に属する、すなわち Type∈Type なのだけど、これは文字通りの「Typeの型はType」という意味ではない。 CoqのTypeは実のところ単一の型ではなく、Type と書いたものは実際には適当な自然数αをおいて(Agdaでいうところの) Setα として解釈されている。そして、Type∈Type は実際には Setα∈Setβ と α<β という制約とを表しているのである*2。 なので、意味的にはAgdaの場合と同じで、「型の型」は同じレベルの型でない。

何故「型の型」を型にしないのか?

CCの場合にしても、AgdaやCoqの場合にしても、なんでこんなにややこしい仕組みにしているかというと、素朴に型全体の型SetもSet自身に属すると考えると、ジラールのパラドックス(Girard's paradox)*3が成り立ってしまうため。 ジラールのパラドックスが成り立ってしまうと、論理体系としては矛盾してしまうし、計算的にも強正規化性が成り立たなくなってしまって、まああんまりよろしくない。

2008-09-10追記

ytbさんが Martin-Lofの V∈V 理論とそのパラドックス - あいまいな本日の私 というエントリでジラールのパラドックスについて面白そうなことを書いているのを発見。

λ. 飲み会

• AdS/CFT対応
  • Anti de Sitter space
    • Black hole
    • 5次元の超重力理論
  • Conformed Field Theory
    • 四次元の場の理論 guage theory
  • Juan Maldacena
• 量子色力学 (Quantum Chromodynamics, QCD)
• 大栗博司 (Hirosi Ooguri)
• Atiyah-Singer の K-theory
• Mr. guage 理論 Gerard t'Hooft

ホログラフィー原理の話を知っていたら、ちょっと感動されてしまった。もっとも、私は エレガントな宇宙 や Decoding Universe でちょっと読んだくらいの知識しか知らないのだけど。

λ. 天井裏のハチの巣

以前にアブが大量発生した我が家。天井を開けたら今度はミツバチの巣が。おいしそうに見えるが、殺虫剤を撒いてしまったので、蜂蜜は食べられない。

【追記】 取り外したらこんな感じに。やっぱりおいしそうだ……