計算資源の共有構造を反映した計算モデルの理論と応用

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

計算資源の共有構造の基礎となる型体系とそのモデルの理論の整備を行なった。特に、共有構造を表現できる線型な型体系の間に成り立つフル・コンプリートネスと呼ばれる強い完全性を、圏論的なモデルの構成方法を用いることにより証明した。これにより、研究計画で挙げた本年度の目標である数学的手法の開発と整理については、少なくとも巡回(再帰)のない共有構造の静的な取り扱いに関しては、ほぼめどがついたと考えれる。これらの成果のうちの主要な部分は、国際会議および雑誌においてすでに発表済みまたは掲載予定である。巡回的な共有構造の分析は、巡回のないものと比べ著しく困難であるが、その基礎的な部分については、学位論文を改定した著書をシュプリンガー社より出版した。1999年9月には、英国エディンバラ大学において、通常の共有構造のないラムダ計算から共有構造をもつ線型なラムダ計算への変換がフル・コンプリートであることについて講演する機会を得た。その後、同大学のJohn Power博士との討論の結果、本研究のモデルの構成の方法が、計算資源の共有構造以外の計算現象の分析にも有用である可能性があることがわかってきた。この一般化については、現在基礎的な結果に関する論文を準備中であり、次年度にはより具体的な応用例も考察していく予定である。