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

1999 Fiscal Year Annual Research Report

• Project/Area Number: 11780215
• Research Institution: Kyoto University
• Principal Investigator: 長谷川 真人 京都大学, 数理解析研究所, 講師 (50293973)
• Keywords: プログラミング言語 / 計算資源 / 再帰計算 / 型理論 / 意味論 / 圏論 / 線型論理 / ラムダ計算

Research Abstract

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

Research Products

• [Publications] 長谷川真人: "再帰的プログラムの意味論とトレース付きモノイダルカテゴリ"コンピュータソフトウェア. 16(2). 62-66 (1999)
• [Publications] Masahito Hasegawa: "Logical predicates for intuitionistic linear type theories"Springer Lecture Notes in Computer Science. 1581. 198-213 (1999)
• [Publications] Masahito Hasegawa: "Girard traslation and logical predicates"Journal of Functional Programminng. (掲載予定).
• [Publications] Masahito Hasegawa: "Models of Sharing Graphs : A Categorical Semantics of left and letrec"Springer-Verlag. 146 (1999)
• [Publications] 田辺誠,中島玲二,長谷川真人: "コンピュータサイエンス入門:論理とプログラム意味論"岩波書店. 203 (1999)