近年の大規模並列計算機や高速ネットワークの開発にともない、並行・分散プログラミング言語の重要性がますます高まってきている。しかるに、並行プログラミング言語の理論的基礎に関する研究はまだ未発達な分野が多く、特にプログラミング言語へすぐに適用しうる有益な型システム・プログラム解析技法等に関する研究が十分になされていない。そのため、関数型言語MLのように理論的基礎に基づいて設計・実装された並行プログラミング言語は現状では皆無であり、多くの並行プログラミング言語はアドホックに設計され、その結果、プログラム解析技法や実装技法の開発に関する見通しが悪くなっている。 本研究では、上のような観測に基づき、並行プログラミング言語、特に並行オブジェクト指向言語のためのさまざまな側面(意味論・型システム・プログラム解析・言語設計・実装技法)を統一的に論じるための理論的基礎の確立を目指す。論文は(1)Girardの線形論理に基づく基本的な並行計算モデルACL/HACLの構築およびそれに基づく並行プログラミング言語HACLの設計(3、4章)、(2)(1)の並行プログラミング言語を核とした、高レベルな言語機能、特に並列オブジェクト指向言語のさまざまな機能の構築、およびそれを援護するためのプログラム解析技術の提案(5、6章)の2部からなる。 第1部では、並行線形論理プログラミングの枠組ACL/HACLを提案し、その理論的基礎を確立する。並行線形論理プログラミングにおいては線形論理の論理式を並行プロセスやメッセージとみなし、計算を論理式の証明過程とみなすことにより、複数のプロセスの並行実行・通信チャネルの動的生成・通信チャネルを介した非同期メッセージの送受信などの並行計算において基本的な動作を明快に表現することができる。このような並行線形論理プログラミングの利点は、 計算に代表される他のプロセス計算に関する理論的研究のほとんどが操作的意味論とそれにもつづくプロセ意味を与えることである。その結果、並行計算系の操作的意味のさまざまなバリエーションとは独立な意味論を与えることができ、また、基礎となる線形論理をいれかえることにより、さまざまな表現力をもつプロセス計算系を統一的にとらえることができる。第3章においては命題線形論理および一階の述語線形論理に基づいたACLについて、操作的意味の線形論理に対する健全性および完全性を証明するとともに、論理式の論理的等価性、意味的等価性と並行プロセスの操作的等価性との関係について論じる。また、並行線形論理プログラミング特有の計算メカニズムの有用性について論じる。第4章においては高階の線形論理に基づいた枠組高階ACL(Higher-Order ACL)を提案し、それに基づいた並行プログラミング言語HACLを設計する。さらにHACLの並行プログラミング言語としての表現力を具体的なプログラム例をとおして示す。 第2部においては、第1部で構成した基礎となる並行プログラミング言語HACLを基に、その上に高レベルな言語機能を構成するとともに、HACLを通して型システム・プログラム解析技法およびそれに基づく最適化等を統一的に論じる。まず第5章で、インヘリタンス・メソッドの再定義・複数のメソッドのアトミックな実行など、並行オブジェクト指向言語のためのさまざまな重要な機能が自然かつ容易に実現できることを示す。これにより、高レベルな機能をもつ並行オブジェクト指向言語が、核言語となるHACLへの単純な変換方法を示すだけで容易に構成できることがわかる。並行オブジェクトを直接実装するのに比べたこのようなアプローチの利点は、(1)高レベルな機能の追加・変更が核言語の実装に手を加えることなく容易に行なえること、かつ(2)そのようにして追加された高レベルな機能の動作がHACLへの変換を通して明確に与えられること、および(3)並行オブジェクト指向言語の型システム、プログラム解析技法、実装技法等をHACLをとおして統一的に論じることができる点である。5章ではさまざまな機能の実現を示すとともに、(3)の一例として、インヘリタンスやメソッドの再定義を許すような言語においても、メソッドディスパッチテーブルの生成の問題が、定数コストでフィールド取り出しが行なえるようなレコード計算の構築の問題に還元することにより、メソッドの起動が定数コストで行なえるようにコンパイルできることを示す。第6章ではHACLを核言語とした高レベル言語の構築をサポートするために必要となる、通信に関する静的解析技法およびそれに基づく最適化について論じる。この解析技法は、核言語に基づく実装による効率の低下を改善するのに用いられるだけでなく、一般の並行オブジェクト指向言語のプログラムの静的解析および最適化にも用いることができると期待される。 |