トップ «前の日記(2005-04-06) 最新 次の日記(2005-04-08)» 月表示 編集

日々の流転


2005-04-07 [長年日記]

λ. 入学式

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

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

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

λ.

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

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

参考

*1 変換には、ふなばさんの「こよみ変換」を使わせてもらいました。感謝。

*2 ちなみに今年の旧暦2月16日は新暦3月25日

λ. 高橋メソッド

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

素晴らしい。

λ. Ω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も参照

*1 "Language-Based Information-Flow Security" でも取り上げられていたのにスッカリ忘れてたよ…… orz

*2 こういうのは田中君が詳しそうだな。