日々の流転

λ. いつものメンバで伊豆方面へ。途中「眺望亭 なが澤」という所で昼飯を食べて、それから城ヵ崎と伊豆高原ペンギン博物館等へ。最後にSEASIDE SPAという所で温泉に。こういうのは久しぶりで、一日とても楽しかった。

• ペンギンの写真1
• ペンギンの写真2

λ. The Haskell 98 Foreign Function Interface 1.0: An Addendum to the Haskell 98 Report

幾つか確認したいことがあったので、一通り目を通す。

ただ、System Compliance Status でGHCとHugsが「conforms to the standard.」というのは嘘っぽいなぁ。どっちも現時点ではForeign.C.StringでUnicodeとlocaleのencodingを変換していない。

λ. 入学式

朝早くて大変だった。でも、僕が着いたときにはまだほとんど来ていなくて、前から2番目の列になってしまった。8:40までに入場ということだったんだが、時間になってもまだ半分も埋まっていない。こんなことならもっとゆっくり来れば良かったかも。

式辞で安西先生は「志」を強調していた。「自分に志はあるだろうか?」と考えて憂鬱になったりもしたけれど、お話自体はよいお話だったと思う。これからのことを考えるとプレッシャーを感じる。入学式は結局正味三十分くらいで終わった。学部の卒業式もこれくらい短いと良かったのだが。

ところで、三田に来るのは学部の入学手続きの時以来なので、ずいぶん久し振りだ。時間もあるので、キャンパスを少しゆっくり周る。そして思う。ここには伝統がある。そして伝統に裏付けられた自信が感じられる。それが心地よい。SFCは三田と比べるとなんというか「人工的」で、どこか心が落ち着かないところがあるように思う。もちろん、どちらが良いとか悪いとか言うつもりはない。

λ. 桜

キャンパス内に咲いている桜が綺麗だった。帰りにもあちこちで桜が咲いているのが見えた。ついでに、中島千波作品展「桜花爛漫」というのを見てきた。世間は桜の季節ですな。

桜といえば、西行法師が「願はくは花の下にて春死なむ　そのきさらぎの望月のころ」と詠んだ通りに没したのは文治6年(建久元年) 2月16日だった。これはユリウス暦だと1190年3月23日、グレゴリオ暦だと1190年3月30日にあたるそうだ*1。今年の3月30日はもう過ぎちゃったな。一週間前は桜はまだあまり咲いていなかったように思うが、これはまあ誤差みたいなものか。ちと残念ではある*2。

参考

• 極東ブログ:西行忌

λ. 高橋メソッド

高橋メソッドについて紹介するページです。

素晴らしい。

λ. Ωmega

イネムリネズミ日記(2005-04-04)より。スライド「Generalizing Algebraic Datatypes in Ωmega」を見た感想。

• Syntax は GADT のものではなく、Phantom types に似てる。
• New Kind の概念を導入してるのは、現在のGHCのGADTよりもスマートだな。
• Some example に挙がっている A Language with Security Domains はなんだろう。興味を引かれる。
  • [2005-04-07 追記] 説明ありがとうございます。type-basedの情報流解析(information flow analysis)と言われると良くわかります。このスライドの例だと確かにLowであるような式がHighの変数を参照しないことを強制できてますね。
    SLam Calculus *1 についても後で調べてみよっと……*2
• A Language with Security Domains の例を見ると、lazyでないのにはそれなりに意味がありそう。これは Hughes の Dependent Types in Haskell を読んだときにも思ったのだけど、undefined は「証明」の値として不適。
• Computing over types のところはあまり細かいことは書かれていないが、型上の計算をどこまで許すかというのは多分微妙で、そこにはデザインデシジョンがあるのではないかと思う。
• [2006-04-23追記] Programming with Static Invariants in Ωmegaも参照

λ. 圏論の解析結果

<URL:http://seibun.nosv.org/?p=%B7%F7%CF%C0>より。

圏論の99%はやらしさで出来ています
圏論の1%は心の壁で出来ています

ちょっwww

λ. チコノフの定理

コンパクト性を理解できたので、今度はチコノフの定理(Tychonoff's Theorem)。今読んでいる Topology via Logic には有限個の直積の場合の証明しか載っていないが、それでも証明を追いかけるのに結構苦労した。まだ、コンパクト性の扱いに慣れていないのかも。

それから、位相空間だけでなくLocaleでもチコノフの定理は成り立つそうだ。しかし、両者の一般化である Topological System への一般化は知らないとのこと。何だか少し不思議だ。

λ. 「テレビの前で、国民に真摯に謝罪すべきではないでしょうか」

年金の名寄せが完了しなかったことに関して、 民主党の議員が国会で 「テレビの前で、国民に真摯に謝罪すべきではないでしょうか」 と言っていた。 そっか、謝罪というのはテレビの前ですべきものなのか。 「国会で」とかではなく「テレビの前で」なんだな。 これは面白い発想だと思った。皮肉ではなく。

λ. 日本語の文法における限定継続?

継続フェスタ2008 (Continuation Fest 2008) のプログラムが公開されていた。 先日読んだ“Continuations in Natural Language”(c.f. ヒビルテ (2008-03-13))が面白かったので、自然言語系の話を期待していたのだけど、大竹塁氏の「Delimited continuation in the grammar of Japanese (日本語の文法における限定継続)」という講演があった。

A natural language expression can be represented as a kind of program. Any such program, if well-formed, can be evaluated in different domains such as orthography, phonology, and semantics. The resulting values are the spelling, pronunciation and meaning, respectively, of the grammatical expression of the language the program represents.

From this viewpoint, I will illustrate the use of delimited continuation in analyzing sentences in Japanese. In particular, the meaning of question words such as 誰 (dare) and 何 (nani) involve shift operator, and that of も (mo) and か (ka) function as reset.

面白そう。 「誰」とか「何」といった疑問詞(question words)が出てくるけど、これは疑問文の意味論の話なのだろうか。

疑問文の話だとすると、どんな話か私にはさっぱり予想がつかないけど、もし平叙文の話だとすると、

• [[ 誰か ]] := λP. [[か]] ([[誰]] P)
• [[ 誰 ]] := λP. P (shift (λk. k))
• [[ か ]] := λP. ∃x. (reset P) x
• [[ も ]] := λP. ∀x. (reset P) x

として、

[[ 誰かが歩く ]]
= [[誰か]] [[歩く]]
= (λP. [[か]] ([[誰]] P)) [[歩く]]
= [[か]] ([[誰]] [[歩く]])
= (λP. ∃x. (reset P) x) ((λP. P (shift (λk. k))) walk)
= ∃x. (reset (walk (shift (λk. k)))) x
= ∃x. (λx. (walk x)) x
= ∃x. walk x

みたいな解釈をするとか、そんな感じかなのかなぁ、と妄想。 (この形式化だとちょっとコジツケくさいけど)