日々の流転

λ. "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月くらい産総研みたいなところに滞在して、彼らと色々議論してみたいものだなぁ。そうすれば、僕みたいなダメ人間にも研究っぽいことが出来そうな気がする ;-)

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