2005 Fiscal Year Annual Research Report
Project/Area Number |
17540102
|
Research Institution | The University of Tokyo |
Principal Investigator |
長谷川 立 東京大学, 大学院・数理科学研究科, 助教授 (20243107)
|
Co-Investigator(Kenkyū-buntansha) |
長谷川 真人 京都大学, 数理解析研究所, 助教授 (50293973)
|
Keywords | 線形論理 / 圏論モデル / トレース / 組合せ論的数え上げモデル |
Research Abstract |
線形論理の圏論的モデル上でのトレースの構成の研究を行った.このモデルのもつmonoidal closed圏としての構造を利用したトレースは,通常は容易に構成できると期待される.通常の線形空間との親和性が高いからである.しかし,プログラミング言語の再帰構造を実現するために要求されるのは,線形論理のモデルに現れるcomonadから作られるcoKleisli圏上でのトレースである.この圏は,cofree coalgebraの作るco-Eilenberg-Moore圏の部分圏と同値なので,この部分圏上でのトレースを考察した.必然的に,トレースはcoalgebra mapとして得られる.このことから,comultiplicationがつぶれてしまうようなcomonadの場合には,monoidal closed圏上でのトレースがそのまま,上の意味での部分圏上のトレースを与えることが分かる,さらに線形論理の圏論モデルにおいては,coalgebra mapは自動的にcomonoid mapとなることが知られているので,部分圏上でのトレースもcomonoid mapとなっていることが要求される.以前の研究での,組合せ論的数え上げモデル上でのトレースに現れた構成は,この要求から自然に現れるものであることが分かった.
|
Research Products
(1 results)