| 研究課題/領域番号 |
11780215
|
|---|
| 研究種目 |
奨励研究(A)
|
| 配分区分 | 補助金 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
長谷川 真人 京大, 数理解析研究所, 講師 (50293973)
|
|---|
| 研究期間 (年度) |
1999 – 2000
|
| 研究課題ステータス |
完了 (2000年度)
|
| 配分額 *注記 |
2,200千円 (直接経費: 2,200千円)
2000年度: 1,000千円 (直接経費: 1,000千円)
1999年度: 1,200千円 (直接経費: 1,200千円)
|
|---|
| キーワード | プログラミング言語 / 計算資源 / 再帰計算 / 型理論 / 意味論 / 圏論 / 線型論理 / ラムダ計算 |
|---|
| 研究概要 |
計算資源の共有構造の基礎となる型体系とそのモデルの理論の整備を行なった。特に、共有構造を表現できる線型な型体系の間に成り立つフル・コンプリートネスと呼ばれる強い完全性を、圏論的なモデルの構成方法を用いることにより証明した。これにより、研究計画で挙げた本年度の目標である数学的手法の開発と整理については、少なくとも巡回(再帰)のない共有構造の静的な取り扱いに関しては、ほぼめどがついたと考えれる。これらの成果のうちの主要な部分は、国際会議および雑誌においてすでに発表済みまたは掲載予定である。
巡回的な共有構造の分析は、巡回のないものと比べ著しく困難であるが、その基礎的な部分については、学位論文を改定した著書をシュプリンガー社より出版した。
1999年9月には、英国エディンバラ大学において、通常の共有構造のないラムダ計算から共有構造をもつ線型なラムダ計算への変換がフル・コンプリートであることについて講演する機会を得た。その後、同大学のJohn Power博士との討論の結果、本研究のモデルの構成の方法が、計算資源の共有構造以外の計算現象の分析にも有用である可能性があることがわかってきた。この一般化については、現在基礎的な結果に関する論文を準備中であり、次年度にはより具体的な応用例も考察していく予定である。
|
