情報科学演習 III 課題紹介(小林研究室

近年、プログラミング言語における型システムをはじめとする基礎理論の役割 がますます重要になってきており、プログラムの正しさの保証だけでなく、コ ンパイラにおけるプログラム最適化や効率のよいランタイムシステムの構築、 セキュリティの問題の解決のためにも種々の型システムやプログラム解析が用 いられています。当研究室でも最近は(特に並行プログラミング言語の)型シ ステムとそれに基づくプログラム解析・メモリ管理といったトピックに力を入 れて研究をすすめています。 そこで情報科学演習 III では、型システムなどの基礎理論とコンパイラやラ ンタイムシステムがどのようにかかわっているかを知ってもらうために、以下 のテーマを用意してみました(この中には、4週間の演習期間の中で完了させ るのは難しい課題も含まれています。そういうものについては、4週間の期間 中ではまずは概略をつかむことに専念し、後日もし興味があれば自主的に継続 してもらうということになります)。

課題の進め方・報告について

課題を選んでもらった時点で、我々のほうから課題を行なう上で必要となる基本的な事柄の説明・参考文献の紹介をし、残りの細かい点は参考文献を読むなり自分で考えるなりしてすすめてもらいます。

基本的には毎週1回(計4回)ミーティングをし、その場で進行状況等について報告をしてもらいます(レジュメを準備すること)。 終了後は、毎回の報告および最終の結果をまとめてレポートとして提出してもらいます。


研究室の紹介

当研究室では、プログラミング言語に関するトピック全般を研究対象としますが、特に重点をおいているのは、プログラミング言語の設計・実装に関するしっかりした基礎理論を構築するとともに、それを実際に処理系に*応用*することです。特に並行プログラミング言語の研究に関しては、処理系の設計・実装に実際に役に立つ理論がまだ不十分であり、当研究室で現在一番力をいれている分野です。並行プログラムの方が逐次プログラムよりも動作が複雑であり、プログラムを安全かつ効率よく走らせるのが難しいだけに、並行プログラミング言語の理論の確立は逐次言語のそれ以上に重要な課題といえます。

なぜ「基礎理論」か

もちろん理論がなくてもプログラミング言語を設計・実装することは可能ではあるし、必ずしも基礎理論との結び付きのない重要な要素技術はたくさんあります(というよりは特に新しいプログラミング言語の場合、初期のうちはむしろそちらの方が多いでしょう)。しかし、近年の関数型言語(特にML)の処理系の設計・実装にみられるように、より高度でかつ頑強な技術を開発しようとすると、基礎理論が不可欠となります。例えば、関数型言語では closure やlist の生成に大量のメモリを消費することは知っていると思いますが、

をどうやったら作れるか思いうかべられるでしょうか?(これについて知 りたい人は課題7へ)おそらくどんな天才ハッカー でも、情報科学の素養がなければそのような処理系を実装しかつ他人にそれが 正しく動作することを説明することは不可能だと思います。これはアインシュ タインの相対性理論やフェルマーの大定理の証明が完全に一人の手によってな されたものではなく、そのための道具立てがそろっていてはじめて可能であっ たのと同じことです(別に上記処理系が相対性理論のように画期的なものであ るといっているわけではありません。念のため)。

また、仮に天才ハッカーなら思いつく技術であっても、その技術に普遍性をもたせて 広く世の中に伝えるためにはやはり基礎理論の助けが必要となります。 誰かが非常に素晴らしいプログラムを開発したとしても、そのプログラムの中身に ついて理解する人がいなければ、書かれたプログラミング言語や 対象とするコンピュータがすたれてしまったら、その時点でそのプログラムにつめこまれて いたアイデアは失われてしまいます。また、プログラムがどんな場合でも本当に正しい 動作をするかどうかは、書いた人を信用するしかありません。 仮に自然言語でドキュメントが書かれていたとしたらどうでしょうか? それでも、そのドキュメントが他の人がプログラムを 再構成したり正しさを検証するのに十分な情報を含んでいる保証はどこにも ありません。それに対し、数学や論理学の言葉でプログラムの振舞いが記述されていれば、 記述に不十分な点がないかどうかやプログラムの正しさのチェックもでき、 プログラム自身がすたれてしまっても、そのアイデア自身は数学や論理学という 普遍的な言葉を通して残ります。

「なんでもいいから何か面白いシステムを開発してみたい」という人も多いと思いますが、そこで注意してもらいたいのは、自分で満足するだけなら別として、研究として世の中で認めてもらえるようなシステムを開発したければ(最終的に理論面で貢献するのでないにしても)やはりある程度基礎理論をふまえておく必要があると思います。実際、近年のプログラミング言語(特に関数型言語)の設計・実装の進歩をみるともはや理論を無視できない状況であるといえます。

「理論」は難しい?

一口に「理論」といってもいろいろありますが、確かに最初は敷居が高く難しく感じられることが多いでしょう。しかし本当に「何か新しい技術を開発したい」と思うのであれば、一から自分で考えるよりは、すでに確立した理論をふまえてから取り組むほうがよほど易しいと思います。(また同じ例をだしますが)理論をふまえずに一から自分で考えようとするのはちょうどアマチュア数学家がフェルマーの大定理を証明しようとするのと同じことです。

最近の研究内容

参考のために以下にここ数年の研究室(というよりも研究室の members)の研究内容をあげておきます。

並行・分散プログラミング言語の設計・実装

線形論理という論理の一種と並行計算と の間に密接な関係があることに着目し、それに基づいた並行線形論理プログラ ミング言語 HACL を設計・実装した。HACL という言語自身は、 ML に並行計算のための primitives を追加したものだと思ってもらえればよ い。ML と同じようにシステムが型推論をしてくれるのでいちいち型宣言をし なくてよい(これに興味のある人は課題1、3へ)。関連論文は

  1. Kobayashi, Shimizu, and Yonezawa, "Distributed Concurrent Linear Logic Programming," to appear in Theoretical Computer Science, 1998.
  2. Kobayashi and Yonezawa, ``Towards Foundations for Concurrent Object-Oriented Programming -- Types and Language Design,'' TAPOS, John-Wiley&Sons, 1995.
  3. Kobayashi and Yonezawa, ``Asynchronous Communication Model Based on Linear Logic,'' Formal Aspects of Computing, 1995
  4. Kobayashi and Yonezawa, ``Higher-Order Concurrent Linear Logic Programming,'' Theory and Practice of Parallel Programming, Springer LNCS907

他。処理系は single processor workstation 用処理系(コンパイラ)HACL, 分散環境 (workstation cluster) 用処理系(コンパイラ)dHACL が存在する。

並行プログラムの安全性を保証する理論

ML で型チェックによってプログラムのバグを未然に防いでいるのと同じよ うに、並行プログラムでもそれに適した何らかの仕組みが必要である。下記の [4] は、日常生活に例えるならば「返事をもらおうと思って往復はがきで手紙 をだしたのに、相手の人が返信用のはがきをすててしまった、あるいは宛名の 部分を書き換えて他の人にだしてしまった、なぜか違う人からたくさんの返事 がきた」といったのに相当するトラブルを並列言語の世界で型システムによっ て未然に防ごうというもの。[5] は(たぶんOSの授業でおなじみの?) deadlock を型システムによって未然に防ごうというものである(これに興味 のある人は課題1、2へ)。

  1. Sumii and Kobayashi, ``A Generalized Deadlock-free Typed Process Calculus,'' HLCL'98, 1998.
  2. Kobayashi, ``A Partially Deadlock-free Typed Process Calculus,'' ACM Transactions on Programming Languages and Systems (TOPLAS), 1998
  3. Kobayashi, Pierce, and Turner, ``Linearity and the Pi-Calculus,'' ACM POPL'96.
  4. Kishimoto, ``Semi-automatic Barbed Bisimulation Checker,'' 卒業論文, 1997.

プログラム解析・最適化・実装技術

静的解析・型を応用した最適化を考案し、HACL やML の処理系で実験を行なっている(このあたりに興味のある人は課題2、4〜7へ)。

  1. Kobayashi, ``Quasi-Linear Types," POPL'99.
  2. Kariya and Kobayashi, ``リージョン推論に基づくメモリ管理の下でのガーベジコレ クション,'' コンピュータソフトウェア, 1999.
  3. Igarashi and Kobayashi, ``Type-based Analysis of Communication for Concurrent Programming Languages,'' Proceedings of Fourth International Static Analysis Symposium (SAS97), Springer LNCS 1302, pp187-201, 1997.
  4. Shimizu and Kobayashi, ``並列言語の高レベルなデータの通信における型を利用した最適化について,'' コンピュータソフトウェア, 1997.
  5. Shimizu, ``A Study on Implementation of a Typed Concurrent Programming Language on Distributed Machines,'' 修士論文, 1996.
  6. Igarashi, ``Type-based Analysis of Usage of Values for Concurrent Programming Languages,'' 修士論文, 1997.
  7. Kobayashi, Nakade, and Yonezawa, ``Static Analysis of Communication for Asynchronous Concurrent Programming Languages,'' SAS'95, Springer LNCS983.