|
線形論理の圏論モデル上に構築された計算体系の性質を研究した。この計算体系は我々によって提案されたものである。ラムダ計算に代表される型理論と圏論との間の静的な関連は古くから知られた古典的な結果であるが、それを動的なレベル、すなわち計算の概念まで包括するように拡張した体系となっている。そのようなまったく新しい体系なので、その計算体系としての性質は多くのものが未解明の状態である。我々は、計算体系の最も基本的な性質の一つであるチャーチ・ロッサー性に関する研究を行った。圏論がもつ独自の構造が計算体系の中に出現するので、古典的な並列簡約などのアイデアで処理できるほど簡単ではない。そのような構造の中でもユニットに関する部分は特に難しい。アルゴリズミックに扱った先行研究もごくわずかしかなく、扱いが非常に困難である。一方において、計算体系の中での重要度としてはさほど高くないと思われるので、ユニットをとりあえずは度外視して残りの部分に関するチャーチ・ロッサー性に関しての検討を行った。そのための手法として我々が考案したは、セマンティクスを用いる方法である。ここでは、正規関手によるセマンティクスを用いている。このような具体的なセマンティクスを利用してチャーチ・ロッサー性にアプローチする手法は、他ではあまり見たことがない。我々は弱正規化性を仮定した上で、チャーチ・ロッサー性の証明を試みた。細部に関してはチェックすべき点が残っているが、概略成功したと考えている。
|
