トレース付きモノイダル圏と高階相互作用の幾何
長谷川真人(京都大学数理解析研究所)

  トレース付きモノイダル圏(traced monoidal category)は、1990年代
半ばに、Joyal、Street、Verityにより、結び目等の巡回的な構造を捉える圏
論の概念として導入されましたが、GirardやAbramskyらの、相互作用の幾何
(Geometry of Interaction、GoI)による双方向のコミュニケーションを伴う
計算モデルの構成や、長谷川やHylandらの、再帰プログラム(自己言及的なプ
ログラム)のモデルで用いられる不動点演算子の特徴付けに用いられるなど、
近年、計算の意味論において、重要な役割を果たすようになりました。
  一方、これらのトレース付きモノイダル圏を用いたGoIや再帰計算の研究で
は、関数型プログラミング言語やラムダ計算において本質的に用いられている、
関数を引数に取る関数=高階関数(汎関数)は、あまり重要ではありませんで
した。計算機科学での応用を考えると、高階の計算や高階の相互作用があると
はどういうことなのか、GoIのなかできちんと説明できなくてはなりません。
  この講演では、トレース付きモノイダル圏とGoI、また再帰プログラムの意
味論について紹介したあと、そのような高階の計算現象が解釈できるというこ
との、GoIにおける随伴関手を用いた簡潔な特徴付けを与えます。そして、そ
の応用として、再帰を持つ型付きラムダ計算の任意のモデル(トレース付きカ
ルテジアン閉圏)は、あるトーティルモノイダル圏から適当な余モナドによる
余Kleisli構成(線型分解)によって得られるモデルと同値になること等を示
します。時間が許せば、プログラム変換や属性文法に関する、勝股らによる最
近の研究との関係も紹介したいと思います。