通信に基づく並列計算モデルのカテゴリー論的意味論

点击翻译按钮获取中文摘要

本研究では、ラムダ計算を計算モデルに持つ、関数型プログラミング言語の実行時の最適化及び並列実行のための解析出段のひとつであるストリクト性解析を、従来の基本データ型上ではなく、構造データ型上で行えるようにカテゴリー論の立場から研究した。構造データ型としては、グラフとその拡張を念頭にしている。発表論文の「A proof of the substitution lemwa in de Bruijns votation」におけるド・ブライン記法とは、ラムダ式を機械的に操作しやすいように表現法を変えたものであり、代入補題とは、ラムダ計算の基本操作である代入の順序の交換可能性を記述定式化したものである。ラムダ式自体はグラフあるいはそれを制限した木構造の特殊なものとみなせる。しかし従来のラムダ式の計算機上での実現は、ラムダ式に付属する環境と呼ばれる大域的なデータが必要になり、これを複数プロセッサ上に分散させるのはむずかしいが、ド・ブライン記法では、そのような大域的なデータを必要とせず、複数プロセッサへの分散が容易となる。この論文は、代入補題をド・ブライン記法を用いて証明したものであるが、その成果は、ラムダ計算の代入の並列実行あるいは遅延実行が抽象的な議論としてではなく、機械的な操作としての基準を与えることである。そして今年度の研究により、そのようなラムダ式上での代入操作を含む、グラフ上の変換の並列実行の基準を、グラフというデータ構造からある程度判断出来るようになった。又、カテゴリー論の観点からは、グラフを含む、計算機上でよく使われる構造データ型を集合値関手圏で特徴付けられるとき、それらのデータ型からそのデータ型上の変換の並列実行の基準をある程度与えることができた。具体的にはそれぞれのデータ型の真偽値オブジェクトと呼ばれるインスタンスを領域とし、データ型上の変換の概念を拡張したものを変換に用いてストリクト性解析を行うことにより得られることが示せた。