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