English page
研究活動
ここでは並行論理型言語である KL1 およびそのデザインの元になっている
GHC (Guarded Horn Clauses) に関する私の研究成果を簡単にまとめています。
目次 (ページ内リンク)
並行/並列論理型言語 KL1
KL1 は、国(通産省)の第五世代コンピュータプロジェクト(1982〜)において、
並列計算機上で記号処理を高速に行なうための核となるプログラミング言語と
して開発され利用されてきた、もっとも実績のある並行論理型言語
(concurrent logic programming language) です。
並行論理型言語は、
- 論理型言語 (Prolog) から探索の機能を取り除くことによって
- それぞれの述語が並行プロセスを表現するようにした
言語であり、並行/並列/分散計算に適しています。
また 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
K
ima
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
までお願い致します。
論文(業績)
- 学位論文
- 論文誌
- [1] 網代育大, 長健太, 上田和紀:
静的解析と制約充足によるプログラム自動デバッグ.
コンピュータソフトウェア, Vol.15, No.1, 1998/1, pp.54-58.
- [2] 網代育大, 上田和紀: Kima: 並行論理プログラム自動修正系.
コンピュータソフトウェア別冊ソフトウェア発展,
Vol.18, No.0, 2001, pp.122-137.
- [3] Ajiro, Y., Ueda, K.,
Kima: an Automated Error Correction
System for Concurrent Logic Programs.
Automated Software Engineering, Vol.9, No.1,
Kluwer Academic Publishers, January 2002, pp.67-94.
- 国際会議
- [4] Ajiro, Y., Ueda, K., Cho, K.,
Error-Correcting Source Code.
In Proc. Fourth Int. Conf. on Principles and Practice of Constraint
Programming (CP'98), LNCS 1520, Springer, 1998/10, pp.40-54.
- 国際ワークショップ
- 全国大会
- [6] 網代育大, 長健太, 上田和紀:
制約に基づく解析による並行論理プログラムの自動デバッグ.
人工知能学会第11回全国大会論文集, 1997/6, pp.205-208.
- [7] 網代育大, 長健太, 上田和紀:
静的解析と制約充足によるプログラム自動デバッグ.
日本ソフトウェア科学会第14回大会論文集, 1997/9, pp.533-536.
- [8] 網代育大, 上田和紀:
並行論理プログラム静的解析系 Kima の実装.
情報処理学会第58回全国大会論文集, 4N-04, 1999/3, pp.397-398.
- [9] 網代育大, 上田和紀: 並行論理プログラム自動修正系 kima
における誤り検出率の向上とその効果.
情報処理学会第60回全国大会論文集, 2V-06, 2000/3, pp.283-284.
- [10] 網代育大, 上田和紀:
並行論理プログラムのプログラム空間に関する考察.
人工知能学会第14回全国大会論文集, 2000/7, pp.449-452.
- [11] 網代育大, 上田和紀:
制約の局所性に基づく並行論理プログラム自動修正系 Kima の最適化.
日本ソフトウェア科学会第18回全国大会論文集, 5B-2, 2001/9, pp.1-4.
スライド
- [12] 網代育大, 上田和紀:
反復深化 A* 探索によるもっともらしいプログラムの効率的な生成.
人工知能学会第16回全国大会論文集, 1E3-02, 2002/5, pp.1-4.
スライド
- デモ発表
- [13] Ajiro, Y., Ueda, K., Kima - an Automated Error
Correction System for Concurrent Logic Programs.
IFIP Int. Conf. on Theoretical Computer Science
(IFIP TCS 2000), 2000/8.
- [14] Ajiro, Y., Ueda, K., Kima - an Automated Error
Correction System for Concurrent Logic Programs.
First Asian Workshop on Programming Languages and Systems,
2000/12.
- 受賞
- 平成9年度 KLIC プログラミング・コンテスト並列環境部門佳作入賞,
1997/12.
- 第4回日本ソフトウェア科学会論文賞 (文献 [1]), 2000/6.
- 人工知能学会全国大会ベストプレゼンテーション賞 (発表 [12]), 2003/6.
- ポスター
関連サイトへのリンク
おまけ
今後の進路を決める上で、だれかの参考になれば幸いです。
トップページへ帰る