所員 -長谷川 真人-

名前 長谷川 真人 (Hasegawa, Masahito)
教授
E-Mail hassei (emailアドレスには@kurims.kyoto-u.ac.jp をつけてください)
研究内容 理論計算機科学の研究
紹 介
 今日の電子計算機において実現されている,もしくはされつつある多様なソフ トウェアについて統一的かつ厳密に議論することを可能にするために,計算 現象が根底に持っている数学構造を抽出し,分析することを研究の目的として いる。 基本的な考え方は,複雑な計算現象を表現・分析するために,適切に抽象化さ れた構造を特定し,そのような構造に関する考察から,計算現象に関する有益 な情報を得ようというものであり,いわば「計算の表現論」である。特に,プ ログラミング言語における制御構造の数学モデル(意味論)の,主に代数的・ 圏論的な手法と,証明論・型理論的な枠組みを用いた分析および応用に取り 組んでいる。
 これまでの研究成果の多くは,
i) トレース付きモノイダル圏を用いた再帰プログラムや巡回構造のモデル,
ii) 副作用を伴う計算のモナドを用いたモデル,あるいは
iii) 線型論理に基づく型理論とそのモノイダル圏によるモデル
に関するものである。
i)については,巡回構造から生じる再帰計算を論じた仕事[1](これはii) やiii)にも密接に関連していた)を出発点に,領域理論における最小不動点演 算子の一様性原理をトレース付きモノイダル圏に拡張した研究 などを行なってきた。圏論を直接には用いないが関 連する方向では,巡回構造を持つ必要呼びラムダ計算の操作的意味論を調べて いる[7]。
ii)については,副作用を伴う制御構造を用いた再帰プログラムの意味論の研究 を行ない,特に再帰と第一級継続の組み合わせから生じる計算を分析した[2]。 また,第一級継続を用いた多相型プログラムが満たすパラメトリシティ原理を 与えた[6]。
iii)に関しては,線型論理に対応する線型ラムダ計算とその圏論的モデルに関 する理論の整備を行なっている[4]。
さらに,ii)とiii)にまたがる仕事として,制御構造の数学モデルに内在する 一種の線型性に着目することにより,効果的に用いられた制御構造の持つ,明 快かつ有用な性質を調べてきた[3]。
最近は,i)とiii)に関連して,トレース付きモノイダル圏の上に双方向計算の モデルを構築するGirardらの「相互作用の幾何」を,高階の計算を含むように 拡張した状況について調べている[6, 8]。また,古典線型論理の圏論的モデル ($*$-自律圏)がトレースを持つのは,実はコンパクト閉圏 である場合に限られることを示した[10]。
 また,新しいテーマとして,プログラム意味論と量子トポロジーの 接点を模索している。これまでに,プログラミング言語の理論で用いられている モノイダル圏においてリボンHopf代数を考え,その表現の圏として非自明な ブレイドを持ち同時に再帰プログラムのモデルにもなっているリボン圏を構成した [9]。
  1. Models of Sharing Graphs: A Categorical Semantics of let and letrec, Distinguished Dissertation Series, Springer-Verlag (1999).
  2. Axioms for recursion in call-by-value, Higher-Order and Symbolic Computation, 15(2/3) (2002), 235-264. (with Y. Kakutani)
  3. Linearly used effects: monadic and CPS transformations into the linear lambda calculus, In Proc. Functional and Logic Programming, LNCS, 2441 (2002), 167-182.
  4. Classical linear logic of implications, Math. Structures Comput. Sci., 15(2) (2005), 323-342.
  5. Relational parametricity and control, Logical Methods in Computer Science, 2(3:3) (2006), 1-22.
  6. On traced monoidal closed categories, Math. Structures Comput. Sci., 19 (2) (2009), 217-244.
  7. Small-step and big-step semantics for call-by-need, J. Funct. Programming, 19 (6) (2009), 699-722. (with K. Nakata)
  8. A note on the biadjunction between 2-categories of traced monoidal categories and tortile monoidal categories, Math. Proc. Cambridge Phils. Soc., 148 (1) (2010), 107-109. (with S. Katsumata)
  9. A quantum double construction in Rel, Math. Structures Comput. Sci.}, 22(4) (2012), 618-650.
  10. Traced $*$-autonomous categories are compact closed, Theory Appl. Categ., 28 (7) (2013), 206-212. (with T. Hajgato)