高階型理論におけるパラメトリシティーの理論

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

本研究では、高階型理論におけるパラメトリシティーの理論について研究し、以下の成果を得た。まず、高階型理論の基礎として、二階型付ラムダ計算の上の二階帰納法とパラメトリシティーの関係を研究した。そして、パラメトリシティーの理論から、各種の帰納法が自然に導入されることを示した。この研究は英文学術雑誌「フンダメンタ・インフォルマチカ」に収録された。次に、その理論を高階型理論に拡張した。高階型理論では、圏論の概念を幾つか表現することが出来る。圏論に於て随伴函手は重要な道具とされている。「極限を保存する函手には随伴函手がある」という定理は、随伴函手に関して最も基本的な定理である。高階型理論では、函手、極限、随伴函手等の概念を表現することが出来る。その様に表現した許では、パラメトリシティーの理論からこの定理が証明される。このことが、本研究の主要な成果である。また本研究では、多相型の計算にとって重要である、最汎型付けについても研究した。従来、線型項の最汎型と準線型項の最汎型に対して、その特徴付けがなされていた。その両者の証明は独立に与えられていた。一方、ベラルディは計算項の最適化という観点から「枝刈」という方法を提案していた。本研究では、枝刈の方法によって、両者の証明が本質的には同一であることを明らかにした。この成果は国際学会「2000年オーストララシア計算機科学週間」にて発表し、英文学術速報「理論的計算機科学電子版速報」に収録された。