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

近年、プログラミング言語における型システムの役割がますます重要になってきており、プログラムの正しさの保証だけでなく、コンパイラやランタイムシステムにおいても積極的に型が用いられるようになってきています。当研究室でも最近は（特に並行プログラミング言語の）型システムとそれに基づくプログラム解析・メモリ管理といったトピックに力を入れて研究をすすめています。 そこで情報科学演習 III では、型システムとコンパイラやランタイムシステムがどのようにかかわっているかを知ってもらうために、以下のテーマを用意してみました（最後のトピックは、型とは関係ありませんが、当研究室で最近手がけている研究に関連するものです）。
  1. 並行プログラミング言語 HACL を使った簡単なプログラミング実験
  2. 並行計算に基づくプログラミング言語の処理系を作る
  3. ML Kit with Regions を使って遊ぶ
  4. 並行プログラミング言語の型システムの論文を読む
  5. MLなどの多相型システムを持つ言語の実装と型との関わりに関する論文を読む
  6. 3年演習で作った Scheme コンパイラをプログラム解析を用いて改良する
  7. 分散並行線形論理プログラミングの枠組に基づいた簡単な分散プログラミング言語のインタプリタを作成する （線形論理って？）

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

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

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

研究室の紹介

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

「理論は難しいからやだなあ」という人へ

なぜ「基礎理論」か

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

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

また、仮に天才ハッカーなら思いつく技術であっても、その技術にある程度普遍性をもたせて広く世の中に伝えるためにはやはり基礎理論の助けが必要となります。

「理論」は難しい？

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

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

最近の研究内容

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

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

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

  1. Kobayashi and Yonezawa, ``Asynchronous Communication Model Based on Linear Logic,'' Formal Aspects of Computing, 1995
  2. Kobayashi and Yonezawa, ``Higher-Order Concurrent Linear Logic Programming,'' Theory and Practice of Parallel Programming, Springer LNCS907
  3. Kobayashi and Yonezawa, ``Type-Theoretic Foundations for Concurrent Object-Oriented Programming,'' ACM OOPSLA'94.
  4. Kobayashi, Shimizu, and Yonezawa, "Distributed Concurrent Linear Logic Programming," to appear in Theoretical Computer Science, 1998.

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

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

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

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

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

静的解析・型を応用した最適化を考案し、（まだ不完全だが）HACL の処理系に実際に組み込まれている（このあたりに興味のある人は課題２、課題３、課題５、課題６へ）。

  1. 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.
  2. Shimizu and Kobayashi, ``並列言語の高レベルなデータの通信における型を利用した最適化について,'' コンピュータソフトウェア, 1997.
  3. Shimizu, ``A Study on Implementation of a Typed Concurrent Programming Language on Distributed Machines,'' 修士論文, 1996.
  4. Igarashi, ``Type-based Analysis of Usage of Values for Concurrent Programming Languages,'' 修士論文, 1997.
  5. Kobayashi, Nakade, and Yonezawa, ``Static Analysis of Communication for Asynchronous Concurrent Programming Languages,'' SAS'95, Springer LNCS983.
  6. Kariya, 卒論.
  7. Tamakoshi, 卒論.