日々の流転

λ. だらだら

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

λ. "Types for Verification" 2日目

.

λ. Ken-etsu Fujita (藤田 憲悦) (Shimane University) "Bijective CPS-translations between λμ-calculi and λ-calculi."

I will talk about bijective CPS-translations between λμ-calculi and λ-calculi.

M.Parigot introduced the λμ-calculus as a formal system of second order classical logic and investigated the computational meaning of classical proofs. On the other hand, the term CPS-translation, in general, denotes a program translation method into continuation-passing style that is the meaning of the program as a function taking the rest of the computation. From a programming point of view, the CPS-translations in this talk make it possible to simulate computations of call-by-name calculi by those of call-by-value ones. First, I provide a CPS-translation from type-free λμ-calculus into λ-calculus. Then it is briefly shown that the CPS-translation forms a bijection by defining an inverse translation back to the source calculus (This result was presented at TLCA'03). Next, in order to carry over the technique in the type-free case to polymorphic λμ-calculus, I give technical problems about

1. the target calculus corresponding to the source,
2. the denotation of λμ-types, and
3. the inverse translation and extensionality of the source calculus

together with ideas to solve them. Finally, I discuss by-product of the main result.

CPS変換の像(とその簡約結果からなる)集合Univと、もとのλμの項全体の集合Sの間に全単射があるのだけど、CPS変換結果を簡約しても問題ないという点に少し驚いた。ただ、僕はλμ計算については「call/ccみたいのを直接扱える体系」くらいの認識しかなくてシンタクスを知らなかったので、いまいちよく分からなかった。けど、結構面白そうな話なので、後でちゃんと調べてみたいところだ。とりあえず、P.Wadlerの"Call-by-value is dual to call-by-name"でもあたってみるか。

λ. QuickCheck再び

QuickCheckについてもう少し詳しい話を John Hughes さんに講義してもらった。Erlangには型が無くてオーバーローディングも無いからErlang版ではちょっとトリッキーなことをする必要があったという話で、急に「Rubyはどう?」と話を振られてしどろもどろになってしまった。英語の出来る人がうらやましいなぁ。

λ. 昼食

に行くときに John Hughes さんに"Generalising Monads to Arrows"に書かれていた type restrictions on datatype (2004-04-10の日記を参照) について質問した。Haskellの仕様を変更する予定とか可能性はないかと訊いたたら、以前にプロポーザル("Restricted Datatypes in Haskell" かな?)を書いたけどそれには最適化(?)の問題があって、今新しいのを書いてると言っていた。

昼食は近くの豚カツ屋(?)さん。池上さんとJohn Hughes さんと同じテーブルで、今度は日常の話をしてたのだけど、ほとんど聞き役な私。あと、それにしてもワンピースやエヴァンゲリオンの話が出るとは思わなかったYO。

λ. 神戸大へ

佐藤さんの紹介で、神戸大の菊池誠先生を訪ねた。Channel Theory や状況理論の話を色々と教えてもらう。

Channel Theory は(集合論のように)非常に一般的な枠組みだから扱おうと思えば何でも扱えてしまうから、何をトークンとし何をタイプとすべきかを一度状況理論に立ち返って考えているとか。

Goguen の Institution のバックグラウンドに J.Barwise の Abstract Model Theory があるというのも初耳だったので驚いた。Abstract Model Theory というのは、J.Barwiseによる無限個のQuantifierを許すような論理体系の研究がきっかけになって作られた、言語とモデルに関する一般理論……という話だったと思うのだけどちょっと記憶に自信がない。詳しくは、『Model-Theoretic Logics』(Edited by J.Barwise, S.Feferman) や "Axioms for Abstract Model Theory", J.Barwise あたりを読むといいらしい。

それから、Formal Concept AnalysisのグループではLatticeを使って割と似たようなことをしているらしいくて、これも興味をそそられた。『Formal Concept Analysis: Mathematical Foundation』(Bernhard Ganter, Rudolf Wille)という本も出ている。

λ. 帰り

この2日間はすごい充実してたので2日間で帰ってきてしまうのが惜しく感じられてしまう。1月くらい産総研みたいなところに滞在して、彼らと色々議論してみたいものだなぁ。そうすれば、僕みたいなダメ人間にも研究っぽいことが出来そうな気がする ;-)

ともあれ、次にくるときは話を聴きに来るのではなく、発表するために来たいものだ。

λ. WWW2005　3日目

寝坊した。ピンチ。朝飯を食わずに急いだところ、なんとか集合時間には間に合ったが、Assignment は既に埋まっていた。しょぼーん（´・ω・｀）

今日もお弁当の配布を手伝う。配布してて思ったのは、ベジタリアン用のお弁当を希望する人の割合が多かったこと。なんでだろうと思って訊いて見たら、「ベジタリアンでなくても、アレルギーや宗教上の理由で食べれないものがある人が、無難な選択としてベジタリアン用を選んでいるのでは?」とのこと。なるほど、たしかに。

あと、お弁当を配っているときに、黒子さんを指して「彼は何で帽子を被ってるのか?」と英語で訊かれて困ってしまった。とりあえず、「It's a costume of Kuroko. Kuroko is 〜」とか言っては見たのだけど、黒子の説明で詰まってしまった。後で本人にも訊いてたけど、本人は「Do you know Kabuki? Kuroko is 〜」と返していた。そうか。僕は黒子といえば文楽というイメージを持っていたのだけど、歌舞伎にも黒子がいるのか。

Lorrie Cranor 氏の基調講演。時間が昼と言うこともあるけど、Timの時よりも人が入ってる気がする。

O'REILLY のブースで和書が10%オフ、洋書が2000円均一だったので、とりあえず RELAX NG を買った。そしたら、O'REILLYメモ帳を貰えた。

Web Internationalization Developments。これまでの中で一番理解できたセッションだった。

ニューオークラで、ディナーパーティ。今回はチケット関係のトラブルもなかったし楽だった。料理、特にケーキは美味しかった。それから、ステージで能をやっていた。舞噺子「船弁慶」というのだそうだ。あまり見れなかったが、やっぱり凄いなぁ。ちゃんと見たくなった。

それと、昨日も書いた黒子さんの後ろ姿の写真。

λ. 大分六日目

土曜は寮の食堂が休みなので、工場の第二食堂で食べてきた。 400円のバイキングで、なかなか良かった。 それから、ローソンへ向かい、日本 Ruby 会議 2007の追加販売のチケットゲット。

夜勤に備えて昼間は寝るつもりなのだけど、その前にまた少し泳ごうと思ってプールに行ったら閉館日だった。土日祝日は休みなのか、残念。

しかし、問題は夕食である。土曜夕方は工場の食堂も休みなのだが……

λ. システム・ソフトウェア #2 システムコール

を観た。

• ビデオ
• 講義資料

λ. 『Cygwinで日本語TeX』 by 黒木裕介

を読む。 黒木さんの作っているCygwin向けの日本語TeXパッケージの開発についてで、スクリーンショット一つとってもちゃんと考えて用意してあったのかと感心。

ちなみに、最近新しいWindowsマシンにTeXを入れるときは、いつも黒木さんのパッケージのお世話になってます。いつもありがとうございます。

• Cygwin で 日本語 TeX --- ptetex を簡単インストール