メンバー

TOP > メンバー > 長谷川 真人

長谷川 真人

名前 長谷川 真人 (Hasegawa, Masahito)

教授

E-Mail hassei (emailアドレスには@kurims.kyoto-u.ac.jp をつけてください)


研究内容 理論計算機科学の研究

紹 介

  コンピュータ上で実現されている,もしくはされつつある多様なソフトウェアについて統一的かつ厳密に議論することを可能にするために,計算が根底に持っている数学構造を抽出し,分析することを研究の目的としている。 基本的な考え方は,複雑な計算現象を表現・分析するために,適切に抽象化された構造を特定し,そのような構造に関する考察から,計算現象に関する有益な情報を得ようというものであり,いわば「計算の表現論」である。特に,プログラミング言語の数学モデル(意味論)の,主に代数的・圏論的な手法と,証明論・型理論的な枠組みを用いた分析および応用に取り組んでいる。
これまでの研究成果の多くは,
i) トレース付きモノイダル圏を用いた再帰プログラムや巡回構造のモデル,
ii) 副作用を伴う計算のモナドを用いたモデル,あるいは
iii) 線型論理に基づく型理論とそのモノイダル圏によるモデル
に関するものである。
i)については,巡回構造から生じる再帰計算を論じた仕事[1](これはii)やiii)にも密接に関連している)を出発点に,不動点演算子やその拡張の,トレース付きモノイダル圏を用いた分析・構成に関する研究などを行なってきた。 圏論を直接には用いないが関連する方向では,巡回構造を持つ必要呼びラムダ計算の操作的意味論を調べている[5]。
ii)については,副作用を伴う制御構造を用いた再帰プログラムの意味論の研究を行ない,特に再帰と第一級継続の組み合わせから生じる計算を分析した[2]。また,第一級継続を用いた多相型プログラムが満たすパラメトリシティ原理を与えた[3]。
iii)に関しては,線型論理の圏論的モデルに関する理論の整備を行なっている[8]。 i)とiii)にまたがる話題として,トレース付きモノイダル圏の上に双方向計算のモデルを構築するGirardらの「相互作用の幾何」に関係する研究も行っている[4,10]。 また,古典線型論理の圏論的モデルである$*$-自律圏(Grothendieck-Verdier圏)がトレースを持つのは,実はコンパクト閉圏(対称リジッド圏)である場合に限られることを示した[7]。
さらに,$*$-自律圏の構造がHopfモナドの代数の圏に持ち上げられるための必要十分条件を与えた[9]。
また,プログラム意味論と量子トポロジー・量子計算の接点を模索している。これまでに,プログラミング言語の理論で用いられているモノイダル圏においてリボンHopf代数を考え,その表現の圏として非自明なブレイドを持ち同時に再帰プログラムのモデルにもなっているリボン圏を構成した[6]。

  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. Relational parametricity and control, Logical Methods in Computer Science, 2(3:3) (2006), 1-22.
  4. On traced monoidal closed categories, Math. Structures Comput. Sci., 19 (2) (2009), 217-244.
  5. Small-step and big-step semantics for call-by-need, J. Funct. Programming, 19 (6) (2009), 699-722. (with K. Nakata)
  6. A quantum double construction in Rel, Math. Structures Comput. Sci.}, 22(4) (2012), 618-650.
  7. Traced $*$-autonomous categories are compact closed, Theory Appl. Categ., 28 (7) (2013), 206-212. (with T. Hajgato)
  8. Linear exponential comonads without symmetry, In 4th International Workshop on Linearity, EPTCS, 238 (2016), 54-63.
  9. Linear distributivity with negation, star-autonomy, and Hopf monads, Theory Appl. Categ., 33(27) (2018), 1145-1157. (with J.-S. Lemay)
  10. From linear logic to cyclic sharing, In Proc. Joint International Workshop on Linearity & Trends in Linear Logic and Applications, EPTCS, 292 (2019), 31-42.

← BACK TO THE TOP

← BACK TO THE TOP

  • Follow on

Research Institute for Mathematical Sciences (RIMS)