| 研究分担者 |
JONES Cliff マンチェスター大学, 計算機科学科, 講師
小林 直樹 東京大学, 大学院理学系研究科, 助手
本田 耕平 慶応義塾大学, 理工学部, 学振特別研究員
渡部 卓雄 北陸先端科学技術大学院大学, 情報科学研究科, 助教授 (20222408)
柴山 悦哉 東京工業大学, 理学部, 助教授 (80162642)
所 真理雄 慶応義塾大学, 理工学部, 教授 (10051898)
|
|---|
| 研究概要 |
本年度の日本側研究者の主要研究成果を以下にまとめておく。このまとめは、平成6年3月に英国を訪問した研究代表者および分担者の成果のみにとどめておく。英国の訪問は年度末ぎりぎりの時点でおこなわれたため、その訪問に得られた具体的成果をここには記さないが、下に述べる成果をもとに、英国側の主要研究者Prof.C.Jones,Prof.I.Watson,Dr.J.Sargeant(いずれもManchester大学)Prof.R.Milner,Prof.R.Burstall,Dr.C.STirling,Dr.Benjamin Pierce,Dr.David Turner,Dr.D.Walker(いずれもEdinburgh大学),Prof.S.Abramsky(Impedrial College,London)等と極めて技術的に深い議論をすることができ、今後の日英両国の並列オブジェクト指向言語の意味論研究の深化に大きく寄与した。
「小林直樹、米澤明憲」
小林と米澤は、従来よりメッセージパッシング形式の非同期通信に基づく非常に強力な並列計算の枠組みACLを考案し、本年度はその理論的基礎の研究およびACLに基づく新しい並列言語の実装のための準備をすすめてきた。
ACLの操作的およびモデル的意味論
ACLは線形論理に基づく論理プログラミングの一種であり、その操作的意味論およびモデル的意味論はGirardによって1987年に提案された線形論理を用いて直接与えることができる。本年度は前年度に本研究員が考案していたACLの意味論をより明確にし、International Logic Programming SymposiumおよびSpringer社から出版されているLNCS(Lecture Notes in Computer Science)seriesにおいて研究成果の発表を行った。さらにより詳しい成果をまとめた論文は雑誌Journal of Formal Aspects of Computingに掲載されることが確定した。
ACLにおけるプロセスの等価性
将来の大規模並列計算機上においては、プロセッサの数・ネットワークのトポロジーの静的および動的な変化に対応するために並列プログラムの変換がますます重要になると予想される。本年度はプログラム変換のための基礎として、プロセスの等価性に関する研究を行い、線形論理に関する世界の一線の研究者が集まったLinear Logic Workshopにおいて、その成果発表を行った。
ACLへの型システムの導入
型推論は、プログラムの誤りの一部をコンパイル時に静的に検出するとともに最適化にも役立ち、さらにプログラムの再利用性も高めるという点で、非常に重要な要素技術である。従来の並列プログラミング言語においては、アドホックな言語設計のために、型推論システムが備わったものが少なかったが、我々は、ACLの明解な理論的基礎をいかして型推論システムを考案することに成功した。この型推論システムは、他の多くの並列プログラミング言語にも適用できる見込みである。これに関する論文は現在国際会議に投稿中である。
「本田耕平」
本田は、従来より並行オブジェクト計算理論のさまざまな側面を明確化するために、数学的な並行計算理論の基礎を築いてきた。これは、並行計算のための基本的な形式系として非同期プロセス計算であるν計算(英国のロビン・ミルナ-教授のπ計算をさらに洗練したもの)を採用し、これに基づく相互作用に基づくプログラミングの基礎理論として、二者間の相互作用の整合性を検査するための型理論と型検査システムの定式化、および相互作用の基礎理論としての並行結合子系の構築を主要目標としてきた。
型理論
型理論に関しては、これまでに考案した型概念をより柔軟に改良した小プログラミング言語を開発し、型システムを定式化し、さらに、そのための型チェックアルゴリズムを大堀らによるカインディングという方法を用いて定式化し、また、その正当性を検証する方式も確立した。
並行結合子理論
この理論は、有限個の原子とその間の単純な相互作用に基づいて協調計算を行なう理論で、今後の協調計算言語の意味論・実装などの基盤として活用できることが期待されるのである。これについては、ν計算の基本的な計算概念である非同期名前通信の操作に対して帰納的分析を行うことにより、原子の構成とその間の相互作用規則を定式化した。また、その相互作用計算における表現能力を検証し、この理論の強力さを実証した。
|
