| 研究概要 |
線型パラメトリシティを実現するにあたって,基盤をなす表示的意味論を与えるための数学的な道具として,twinerの理論を構築した.これは,Joyalによる解析関手のgroupoidへの拡張になっているとともに,群のwreath積の拡張でもある.我々は以前,解析関手を用いた一階線型論理のモデルを考察した.しかし,線型パラメトリシティを実現するためには,高階の線型論理を考える必要があり,そのモデルを構築するには解析関手では不十分である.この要請にこたえるものとして,twinerという新しい概念を導入するにいたった.
さらに,twinerを用いて高階線型論理のモデルを構築した.このモデルは,線型パラメトリシティを考察するために,その基盤となる最初のモデルの役割を果たす.高階線型論理を含む高階型システムのモデルを作ることは非常に難しく,限られたモデルしか知られていない.我々のモデルは,その意味で新しい特徴を持った高階型システムのモデルとして,それ自身価値を持つものと考える.
上に述べたモデルの上で線型パラメトリシティの原理を考え,この原理を満たすような第二のモデルを構築するのが次の仕事である.このためには,まず第一のモデルを含むユニバースで成立するメタな論理を考え,その中で線型パラメトリシティを形式化することから始めなければならない.この論理は,線型論理にdependent typeを導入したものとなるはずである.この方向での研究は今までなかったもので,我々はそのいくつかの試案を提示した.
|
