|
再帰プログラムや巡回データ構造を用いた計算，また双方向に情報をやり取りする計算は，それぞれ，「再帰プログラムの幾何」および「相互作用の幾何」として，巡回的な構造を持つ数学構造（トレース付きモノイダル圏）を基礎として捉えられる．一方，そのような数学構造は，結び目の量子不変量を中心とした低次元トポロジーの近年の発展（量子トポロジー）においても重要な役割を果たしてきた．
最近，再帰プログラムの幾何・相互作用の幾何と、量子トポロジーの両方の特徴を合わせ持つトレース付きモノイダル圏（リボン圏）の具体的な例が，研究代表者によって構成された．本研究では，この最近の成果を出発点として，プログラミング言語の意味論を量子トポロジーの知見と有機的に組み合わせることにより，位相的量子計算など新しい計算パラダイムに対応したプログラム意味論の構築（プログラム意味論の量子化）を行うことを目指している．
本年度は、プログラム意味論の量子化を具体化することを目指し、ゲーム意味論や線形論理の意味論におけるリボンホップ代数の構成を調べた。その結果、ゲーム意味論で用いられる多くの圏が非自明なホップ代数を持たないこと、また線形論理の意味論においても非自明なリボンホップ代数が存在する場合としない場合があることを見出した（Kenji Maillardとの共同研究）。これらの当初予想していなかった結果は、プログラム意味論の量子化には、既存の量子トポロジーの知見に加えた新しいアイデアが必要であることを示唆している。
また、既存の意味論との比較に関連して、型付きラムダ計算に関する国際会議TLCA2013のプログラム委員長を務め、論文集を編集・出版した。
|
