| Project/Area Number |
10780185
|
|---|
| Research Category |
Grant-in-Aid for Encouragement of Young Scientists (A)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
竹内 泉 京都大学, 大学院・情報学研究科, 助手 (20264583)
|
|---|
| Project Period (FY) |
1998 – 1999
|
| Project Status |
Completed (Fiscal Year 1999)
|
| Budget Amount *help |
¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 1999: ¥800,000 (Direct Cost: ¥800,000)
|
|---|
| Keywords | 高階型 / 型理論 / パラメトリシティー / 多相型 / ラムダ計算 / パラメトリシティ |
|---|
| Research Abstract |
本研究では、高階型理論におけるパラメトリシティーの理論について研究し、以下の成果を得た。
まず、高階型理論の基礎として、二階型付ラムダ計算の上の二階帰納法とパラメトリシティーの関係を研究した。そして、パラメトリシティーの理論から、各種の帰納法が自然に導入されることを示した。この研究は英文学術雑誌「フンダメンタ・インフォルマチカ」に収録された。
次に、その理論を高階型理論に拡張した。高階型理論では、圏論の概念を幾つか表現することが出来る。圏論に於て随伴函手は重要な道具とされている。「極限を保存する函手には随伴函手がある」という定理は、随伴函手に関して最も基本的な定理である。高階型理論では、函手、極限、随伴函手等の概念を表現することが出来る。その様に表現した許では、パラメトリシティーの理論からこの定理が証明される。このことが、本研究の主要な成果である。
また本研究では、多相型の計算にとって重要である、最汎型付けについても研究した。従来、線型項の最汎型と準線型項の最汎型に対して、その特徴付けがなされていた。その両者の証明は独立に与えられていた。一方、ベラルディは計算項の最適化という観点から「枝刈」という方法を提案していた。本研究では、枝刈の方法によって、両者の証明が本質的には同一であることを明らかにした。この成果は国際学会「2000年オーストララシア計算機科学週間」にて発表し、英文学術速報「理論的計算機科学電子版速報」に収録された。
|
