| 研究概要 |
線形論理の圏論的モデル上でのトレースの構成の研究を行った.このモデルのもつmonoidal closed圏としての構造を利用したトレースは,通常は容易に構成できると期待される.通常の線形空間との親和性が高いからである.しかし,プログラミング言語の再帰構造を実現するために要求されるのは,線形論理のモデルに現れるcomonadから作られるcoKleisli圏上でのトレースである.この圏は,cofree coalgebraの作るco-Eilenberg-Moore圏の部分圏と同値なので,この部分圏上でのトレースを考察した.必然的に,トレースはcoalgebra mapとして得られる.このことから,comultiplicationがつぶれてしまうようなcomonadの場合には,monoidal closed圏上でのトレースがそのまま,上の意味での部分圏上のトレースを与えることが分かる,さらに線形論理の圏論モデルにおいては,coalgebra mapは自動的にcomonoid mapとなることが知られているので,部分圏上でのトレースもcomonoid mapとなっていることが要求される.以前の研究での,組合せ論的数え上げモデル上でのトレースに現れた構成は,この要求から自然に現れるものであることが分かった.
|
