English page

研究活動

ここでは並行論理型言語である KL1 およびそのデザインの元になっている GHC (Guarded Horn Clauses) に関する私の研究成果を簡単にまとめています。

目次 (ページ内リンク)


並行/並列論理型言語 KL1

KL1 は、国(通産省)の第五世代コンピュータプロジェクト(1982〜)において、 並列計算機上で記号処理を高速に行なうための核となるプログラミング言語と して開発され利用されてきた、もっとも実績のある並行論理型言語 (concurrent logic programming language) です。

並行論理型言語は、

  1. 論理型言語 (Prolog) から探索の機能を取り除くことによって
  2. それぞれの述語が並行プロセスを表現するようにした
言語であり、並行/並列/分散計算に適しています。 また 2 の性質から、並行論理型言語で記述されたプログラムは、手続き的にも 宣言的にも読むことが可能です。 探索の機能を失ってはいるものの、記号処理の記述のしやすさに関しては、 論理型言語と同等かそれ以上であるといえるでしょう。

並行論理プログラムでは、

言語仕様の中で理論的に並行性を扱っていることで 並行/並列プログラムの記述が容易となり、 プログラムを並列化するための手間を最小限に抑えることができます。 並列プログラムを書くために現在広く用いられている C 言語 (と並列ライブラリ/インタフェースである PVM, MPI、やスレッド) や HPF (High Performance Fortran) は、既存の手続き型言語に並列化のための 拡張を施したものであるがゆえに、並行/並列性を (言語のセマンティクスの観点から)うまく扱うことができません。 実際に MPI, PVM などを使って並列プログラムを書いたことのあるひとには分か ることですが、プログラムを並列化するための手間が もとの逐次プログラムを作る手間以上にかかることになります。

並行論理型言語は高級言語であるため、 並行論理プログラムの実行効率は C 言語などの低級言語 (言語のレベルからハードウェアの動作が見えてしまう言語)で うまく書かれたプログラムに比べて劣ります。 しかし、プログラムの静的解析によって、実行効率を手続き型言語で書かれた プログラムにかなり近いところまで改善しようという研究が現在、 上田研究室の他のグループで行なわれています(次節のリンクを参照)。

KL1 の処理系としては KLIC と呼ばれるフリーの KL1-to-C コンパイラがあり、 たいていの UNIX マシンにインストールすることができます。 KLIC 処理系は こちらのサイト で配布されています。 Sun Microsystems 社の並列サーバや、最近はやりのデュアルプロセッサ PC/AT 互換機などの上で、手軽に並列プログラムが楽しめます。


(Moded Flat) GHC と静的解析技術

並行論理型言語は、論理型言語と同様、一階述語論理に基づいており、 数学的に扱いやすいため、プログラムの性質をプログラムの実行前に推論する 「静的解析」との親和性が高いと考えられます。 現在、KL1 のデザインの基である GHC に静的解析のための体系を組込んだ Moded Flat GHC を用いて、 並行論理プログラミングにおける静的解析技術の開発が進められています。 GHC に、プロセスを PE (Processor Element)に分割するためのコンストラクトや syntax sugar、組込み述語などを追加したのが KL1 です(たぶん)。 静的解析によって検証したい対象として、以下のものが挙げられます:

これらはコンピュータの社会への浸透によって近年ますます重要となり、 技術の開発が強く望まれるものの、その実現が難しい分野であるといえます。

並行/並列/分散計算と従来の逐次型計算との違いは、 逐次計算の最中になんらかの「通信」が発生するという点です。実時間計算も、 逐次処理に対して外界(環境)との通信が発生するだけだとみなすことができます。 これは単純な違いですが、しかし大きな違いで、 これによってプログラムの振舞いが複雑化し、 プログラムのデバッグなどが非常に困難なものとなるため、 静的解析によってプログラムの性質が事前に解析できることの利点は非常に大きいといえます。 並行論理型言語 (Moded Flat GHC) は、プログラミング言語であるばかりでなく、 並行/並列/分散/実時間計算を統一的に扱うため資質を十分に備えた、 計算モデルとしての側面も持っています。

現在、上田研究室で進められている研究の詳細については これ をご覧ください。 また、 GHC の設計者(上田和紀 教授)のページ GHC/KL1 の講義資料 もあります。


並行論理プログラム自動修正系 Kima

KL1, it's automatic !

Kima は、研究室の先輩である 長 健太 氏によって第1版が作成されました。 Analyzer of Ill-Moded KL1 programs が名称の由来です。 第1版は このページ にある「KL1プログラム開発支援ツール」の項目から入手できます。

Kima 第1版は、Moded Flat GHC の強モード/型体系を KL1 上に仮定することで、 KL1 プログラム中の誤りをプログラムテキスト中の一定の範囲内に絞り込む機能を持っていました。 Kima 第2版は、この技法をさらに発展させ、 プログラム中の軽微な誤りを自動的に修正することを可能にしています。 詳しくは、アーカイヴに付属のREADME または論文をご覧ください。 また、Kima は KL1プログラム静的解析系 klint 第2.1版 を基に作成されています。

ダウンロード

Kima は、Unix 系 OS 上で利用できます。

Kima の使用許諾は、 ICOT 無償公開ソフトウェアの利用条件に準じます。 また、Kima に対するご意見、ご感想、バグレポート等は ajiro@ueda.info.waseda.ac.jp までお願い致します。


論文(業績)


関連サイトへのリンク


おまけ

今後の進路を決める上で、だれかの参考になれば幸いです。


トップページへ帰る