課題を選んでもらった時点で、我々のほうから課題を行なう上で必要となる基本的な事柄の説明・参考文献の紹介をし、残りの細かい点は参考文献を読むなり自分で考えるなりしてすすめてもらいます。
基本的には毎週1回(計4回)ミーティングをし、その場で進行状況等について報告をしてもらいます(レジュメを準備すること)。 終了後は、毎回の報告および最終の結果をまとめてレポートとして提出してもらいます。
当研究室では、プログラミング言語に関するトピック全般を研究対象としますが、特に重点をおいているのは、プログラミング言語の設計・実装に関するしっかりした基礎理論を構築するとともに、それを実際に処理系に*応用*することです。特に並行プログラミング言語の研究に関しては、処理系の設計・実装に実際に役に立つ理論がまだ不十分であり、当研究室で現在一番力をいれている分野です。並行プログラムの方が逐次プログラムよりも動作が複雑であり、プログラムを安全かつ効率よく走らせるのが難しいだけに、並行プログラミング言語の理論の確立は逐次言語のそれ以上に重要な課題といえます。
もちろん理論がなくてもプログラミング言語を設計・実装することは可能ではあるし、必ずしも基礎理論との結び付きのない重要な要素技術はたくさんあります(というよりは特に新しいプログラミング言語の場合、初期のうちはむしろそちらの方が多いでしょう)。しかし、近年の関数型言語(特にML)の処理系の設計・実装にみられるように、より高度でかつ頑強な技術を開発しようとすると、基礎理論が不可欠となります。例えば、関数型言語では closure やlist の生成に大量のメモリを消費することは知っていると思いますが、
をどうやったら作れるか思いうかべられるでしょうか?(これについて知 りたい人は課題7へ)おそらくどんな天才ハッカー でも、情報科学の素養がなければそのような処理系を実装しかつ他人にそれが 正しく動作することを説明することは不可能だと思います。これはアインシュ タインの相対性理論やフェルマーの大定理の証明が完全に一人の手によってな されたものではなく、そのための道具立てがそろっていてはじめて可能であっ たのと同じことです(別に上記処理系が相対性理論のように画期的なものであ るといっているわけではありません。念のため)。
また、仮に天才ハッカーなら思いつく技術であっても、その技術に普遍性をもたせて 広く世の中に伝えるためにはやはり基礎理論の助けが必要となります。 誰かが非常に素晴らしいプログラムを開発したとしても、そのプログラムの中身に ついて理解する人がいなければ、書かれたプログラミング言語や 対象とするコンピュータがすたれてしまったら、その時点でそのプログラムにつめこまれて いたアイデアは失われてしまいます。また、プログラムがどんな場合でも本当に正しい 動作をするかどうかは、書いた人を信用するしかありません。 仮に自然言語でドキュメントが書かれていたとしたらどうでしょうか? それでも、そのドキュメントが他の人がプログラムを 再構成したり正しさを検証するのに十分な情報を含んでいる保証はどこにも ありません。それに対し、数学や論理学の言葉でプログラムの振舞いが記述されていれば、 記述に不十分な点がないかどうかやプログラムの正しさのチェックもでき、 プログラム自身がすたれてしまっても、そのアイデア自身は数学や論理学という 普遍的な言葉を通して残ります。
「なんでもいいから何か面白いシステムを開発してみたい」という人も多いと思いますが、そこで注意してもらいたいのは、自分で満足するだけなら別として、研究として世の中で認めてもらえるようなシステムを開発したければ(最終的に理論面で貢献するのでないにしても)やはりある程度基礎理論をふまえておく必要があると思います。実際、近年のプログラミング言語(特に関数型言語)の設計・実装の進歩をみるともはや理論を無視できない状況であるといえます。
一口に「理論」といってもいろいろありますが、確かに最初は敷居が高く難しく感じられることが多いでしょう。しかし本当に「何か新しい技術を開発したい」と思うのであれば、一から自分で考えるよりは、すでに確立した理論をふまえてから取り組むほうがよほど易しいと思います。(また同じ例をだしますが)理論をふまえずに一から自分で考えようとするのはちょうどアマチュア数学家がフェルマーの大定理を証明しようとするのと同じことです。
線形論理という論理の一種と並行計算と の間に密接な関係があることに着目し、それに基づいた並行線形論理プログラ ミング言語 HACL を設計・実装した。HACL という言語自身は、 ML に並行計算のための primitives を追加したものだと思ってもらえればよ い。ML と同じようにシステムが型推論をしてくれるのでいちいち型宣言をし なくてよい(これに興味のある人は課題1、3へ)。関連論文は
他。処理系は single processor workstation 用処理系(コンパイラ)HACL, 分散環境 (workstation cluster) 用処理系(コンパイラ)dHACL が存在する。
ML で型チェックによってプログラムのバグを未然に防いでいるのと同じよ うに、並行プログラムでもそれに適した何らかの仕組みが必要である。下記の [4] は、日常生活に例えるならば「返事をもらおうと思って往復はがきで手紙 をだしたのに、相手の人が返信用のはがきをすててしまった、あるいは宛名の 部分を書き換えて他の人にだしてしまった、なぜか違う人からたくさんの返事 がきた」といったのに相当するトラブルを並列言語の世界で型システムによっ て未然に防ごうというもの。[5] は(たぶんOSの授業でおなじみの?) deadlock を型システムによって未然に防ごうというものである(これに興味 のある人は課題1、2へ)。
静的解析・型を応用した最適化を考案し、HACL やML の処理系で実験を行なっている(このあたりに興味のある人は課題2、4〜7へ)。