close
1.
助成・補助金
Kyushu Univ. Production 九州大学成果文献
Cover image of 通信に基づく並列計算モデルのカテゴリー論的意味論
大塚 寛
研究期間: 1993
本文を見る:
概要: 本研究では、ラムダ計算を計算モデルに持つ、関数型プログラミング言語の実行時の最適化及び並列実行のための解析出段のひとつであるストリクト性解析を、従来の基本データ型上ではなく、構造データ型上で行えるようにカテゴリー論の立場から研究した。構造データ型としては、グラフとその拡張を念頭にしている。発表論文の「A proof of the substitution lemwa in de Bruijns votation」におけるド・ブライン記法とは、ラムダ式を機械的に操作しやすいように表現法を変えたものであり、代入補題とは、ラムダ計算の基本操作である代入の順序の交換可能性を記述定式化したものである。ラムダ式自体はグラフあるいはそれを制限した木構造の特殊なものとみなせる。しかし従来のラムダ式の計算機上での実現は、ラムダ式に付属する環境と呼ばれる大域的なデータが必要になり、これを複数プロセッサ上に分散させるのはむずかしいが、ド・ブライン記法では、そのような大域的なデータを必要とせず、複数プロセッサへの分散が容易となる。この論文は、代入補題をド・ブライン記法を用いて証明したものであるが、その成果は、ラムダ計算の代入の並列実行あるいは遅延実行が抽象的な議論としてではなく、機械的な操作としての基準を与えることである。そして今年度の研究により、そのようなラムダ式上での代入操作を含む、グラフ上の変換の並列実行の基準を、グラフというデータ構造からある程度判断出来るようになった。又、カテゴリー論の観点からは、グラフを含む、計算機上でよく使われる構造データ型を集合値関手圏で特徴付けられるとき、それらのデータ型からそのデータ型上の変換の並列実行の基準をある程度与えることができた。具体的にはそれぞれのデータ型の真偽値オブジェクトと呼ばれるインスタンスを領域とし、データ型上の変換の概念を拡張したものを変換に用いてストリクト性解析を行うことにより得られることが示せた。 続きを見る
2.
助成・補助金
Kyushu Univ. Production 九州大学成果文献
Cover image of 通信に基づく並列計算モデルのカテゴリー論的意味論
大塚 寛
研究期間: 1996
本文を見る:
概要: 並列計算、特にCCSの通信に関する研究と、それに基づく通信モデルを解析するための実験をTransputerおよびPVMの2種類の並列コンピュータシステムの上で行なった。 CCSでは、遷移関係の定義とそれに基づく(強)双模倣関係の定義のしかたでプロセスの等価関係の強弱が変わる。特にCCSを高階化したπ-計算においては、通信で渡される値によって遷移先を区別する遷移関係(early transition)と、通信で渡される値によらない遷移関係(late transition)が、プロセスや通信経路の動的な生成を記述するために導入されている。しかし我々は静的に決まったネットワークトポロジによって接続されたなかで通信を行なうプロセスを研究の対象にした。 このように高階化しないままのCCSで記述出来るプロセスを考察する場合には、プロセスや通信経路の動的な変化を考慮する必要はないが、通信で渡される値によって異なるプロセスへ遷移が起こる場合があるので、通信で渡される値については考慮しなければならない。そこで、上記後者の遷移関係を基礎にした(強)双模倣関係とその上の等価関係について研究した。この遷移関係の主要な特徴は、遷移システムの導出に際して、実際に通信が行なわれるまでは、そのプロセスの遷移の導出を行なわない、あるいは通信される値をパラメータ化し、それを基に遷移の導出を行うことにある。 なお、今回はこの遷移関係および双模倣関係をカテゴリー論的に解釈するところまでは至らなかった。もともと双模倣関係の導入の方法が、双帰納法による最大不動点で与えられるという非有基的集合論を基にしているので、プロセスに制限を与える必要があると思われる。 続きを見る