日々の流転

λ. シグマ計算

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

λ. あろ〜むで夕食

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

λ. 今日の向井研

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

発表資料。

λ. Rena (6)

あまりにもダメ過ぎたので、少しだけ直した。rena-0.0.2.tar.gz

λ. predicativeな型理論であるということ

Agdaで(2階ラムダ計算の)パラメトリシティに関する命題を証明してみようと思い、以下のようなコードを書き始めたのだが、Forallのところで「Sort comparison failed」と怒られてしまった。

Rel (X,Y::Set) :: Type
  = X->Y->Set
 
FunRel (|A,B,C,D::Set) (R::Rel A B) (S::Rel C D) :: Rel (A->C) (B->D)
  = \(f::A->C)-> 
     \(g::B->D)-> 
       ((a::A) |-> (b::B) |-> R a b -> S (f a) (g b))
 
Forall (F::Set->Set) :: Set
  = (X::Set) -> F X
 
ForallRel (|F,G::Set->Set) (R::(A,B::Set)|->Rel A B->Rel (F A) (G B))
  :: Rel (Forall F) (Forall G)
  = \(f::Forall F)-> 
     \(g::Forall G)-> 
      ((A,B::Set) |-> (S::Rel A B) -> R S (f A) (g B))

しばらく悩んで、ようやくAgdaがMartin-Löf流のpredicativeな型システムであることを思い出した。FやCCのようなimpredicativeな型システムと違って、こういう定義は出来ないのだった。関数の型のソートに関する規則を、Adga の Structured Type Theory と、λ-cubeのスタイルで形式化したCC とで比べてみると良くわかる。λ-cubeでは返り値の型のソートが関数の型のソートになる。一方、Structured Type Theory では直観的には引数の型のソートと返り値の型のソートの最小上界が関数の型のソートになる。

アホだなオレ。しかし、impredicativeな型システムに慣れてる人が使うと絶対ハマると思うよ、これ。

それで思ったが、そうなるとGHCのCore言語をAgdaのコードに変換してゴニョゴニョってのは問題が起こりそうな気がするな。GHCのCore言語は一応Fω風のimpredicativeな型システムだったと思うので。

λ. Describing and Reasoning on Web Services using Process Algebra. Gwen Salaün, Lucas Bordeaux, Marco Schaerf

を読んだ。

ITシステムでbisimulationの説明をしていたときに、bisimulationの意味がわからないが使ってみた というのを誰かが見つけてきて面白かった。

bisimulationの(余代数的/圏論的な)定義は知っているけど、weak bisimulation と strong bisimulation については知らない。調べなくては。weak bisimulation は behavioral equivalence とは違うよね?

(2005-09-16 追記) strong bisimulation が普通のbisimulation。τアクションによる違いを無視するのが weak bisimulation 。http://www.lix.polytechnique.fr/~catuscia/teaching/DEA/General/Exercises_James/exercises.pdf の「4 Definition: CCS operational equivalences」が分かりやすかった。

λ. "Youtube to me" 改造版

Greasemonkeying with Google Video and YouTube が便利そうだったので使おうとしたのだけど、期待通りに動かなかったので、ちょっと改造してみた。youtube_to_me.user.js

【2007-09-29追記】 久しぶりに使おうとしたら、flvのURLが変わっていて使えなくなっていた。 仕方ないので直したが、javascriptを忘れていて焦る。

λ. 部分評価

<URL:http://alohakun.blog7.fc2.com/blog-entry-306.html> より。

流石に「Lispのマクロ展開」とか「融合変換」は部分評価とは呼ばない気が……。だって、それらはそもそも「評価」の一部ではないと思うし。

(後で部分評価について少し書く)

λ. 大分から帰る

今日は、午後から懐かしの関東へと帰る。 思い返すと、この一ヶ月色々あったなぁ。 この出会いと経験とを大切にしたい。

大分は天晴れだったが、関東に着いたら雨で、少し驚く。 しかも、雷で自宅と学校が一瞬停電したりもしたし。

明日からは配属先でまた研修である。 周囲には「現実に引き戻される」ことを残念がる人も多いが、個人的にはこっちに戻ってこれて結構ウキウキしている。 大分での生活はもちろん満喫していたが、それでもやはり我慢していたことというのも多いしね。

λ. Topology via Logic だいたい読了

Topology via Logic を一応最後まで読み終わった。 後半の練習問題はほとんど解いてないし、本文も SFP domain, Power domain, Cohn's field spectrum 等についてはさらっと読んだだけで流してしまったが。

次は『位相と論理』でも読もうか。これは似たタイトルだけど内容はだいぶ違う。

λ. 西鎌倉混声コーラス第6回定期演奏会

西鎌倉混声コーラスの第6回定期演奏会なるものを観てきた。

• レクイエム ニ短調 K.626 (モーツァルト) [Naxos Music Library] [Naxos Music Library (SFC用)]
• 唱歌の四季
  • 朧月夜
  • 茶摘
  • 紅葉
  • 雪
• 混声合唱曲集　鳥の歌 (10のスペイン民謡より)
  • 鳥の歌
  • アララ
  • アラブの二人娘
  • さよならの夜

λ. クラスター爆弾禁止条約 採択

これまでクラスター爆弾が果たしていた役割を、どうやって代替していくのかな。 それを十分検討する前に採択されてしまった印象があって、色々不安。