所員 -勝股 審也-

名前 勝股 審也 (Katsumata, Shin-ya)
助教
E-Mail sinya (emailアドレスには@kurims.kyoto-u.ac.jp をつけてください)
研究内容 理論計算機科学の研究
紹 介
 計算機科学の一分野にプログラミング言語の意味論がある。これはプログラミ ング言語が供える様々な機構を数学的および論理学的にモデル化して調べ, 得 られた知見を実際の言語の設計や改良に還元する研究分野である。この分野に おいて以下の研究を行ってきた。

 エフェクトシステムの意味論  プログラムの最適化や安全性の検証を行う上で必要不可欠なのがプログラムの 挙動の静的な分析である。特にプログラムが引き起こす入出力やメモリのアク セス,非決定的選択といった副作用の分析には, エフェクトシステムと呼ばれる型理論的な アプローチが広く用いられている。現在はモナドに 類似した構造である次数付きモナドに関心がある。[7]では 一般的なエフェクトシステムの圏論的意味論を次数付きモナドを用いてを与え た。また,次数付きモナドに対するKleisli圏とEilenberg-Moore圏の構成を東京大学 の藤井氏とパリ・ディドロ大学のMelliés氏との共同研 究[8]で与えた。

 ラムダ計算の部分モデルの構成  プログラミング言語の性質を調べ ることの多くは, 「プログラムの解釈がある性質を満たす」ことを示す問題に 帰着される。この問題を解くには, その性質を満たす部分モデルの存在を示せ ばよく, 特にラムダ計算では論理関係と呼ばれる手法が頻繁に用いられ てきた。論理関係はラムダ計算の型の構造に依存して定義されるため, 90年代 に入り, ラムダ計算をモナド型で拡張してプログラミング言語の 持つ様々な機構を表現することが提案されると, モナド型に対する論理関係の定義が様々 な研究で問題となった。
これに対し, [1]で意味論的$\top\top$-liftingというモナドのための論理関係の構成法を提案 した。この構成法の特徴はパラメータを変える事で様々な論理関係を導く事が できる柔軟さにある。この柔軟さを応用し, [5]で, 値呼び関 数型プログラミング言語の二つのモナド的意味論の間に大域的な関係が成立す ることを示すための十分条件を与えた。この結果は幅広いクラスの表示的意味 論に対して適用でき, 副作用を持つ関数型プログラミング言語の意味論の比較 や, 安全性の検証に有用である。

 プログラム変換  関数型プログラミングに関連する話題として, 融合変換の研究を行った。累積変数付きの関数の融合変換を再帰的 定義を用いて行う手法は属性文法のdescriptional compositionという手法を背景としていることが知られている。 [3]の研究後, これらの 融合変換と属性文法の両者をシステマティックに分析, 導出する枠組として, トレース付きモノイダル圏における属性文法の定式化を[2]で提 案した。この定式化を押し進め, [4]では構文上の属性文法をト レースを保つある種の関手として, またそれらのdescriptional compositionを 関手の合成として定式化できる事を示した。
  1. A Semantic Formulation of TT-lifting and Logical Predicates for Computational Metalanguage. In Proc. CSL 2005, LNCS, 3634 (2005), 87-102.
  2. Attribute Grammars and Categorical Semantics. In Proc. ICALP 2008, Part II, LNCS 5126, pp. 271-282.
  3. (Joint work with Susumu Nishimura) Algebraic Fusion of Functions with an Accumulating Parameter and Its Improvement. J. Functional Programming, 18, issue 5-6, pp. 781-819.
  4. Categorical Descriptional Composition. In Proc. APLAS 2010, LNCS 6461, pp.222-238.
  5. Relating Computational Effects by TT-Lifting. Information and Computation (Special issue on ICALP 2011), 222 (2013), pp. 228-246.
  6. (Joint work with Tetsuya Sato) Preorders on Monads and Coalgebraic Simulations. In Proc. FoSSaCS 2013, LNCS, 7794 (2013), pp. 145--160.
  7. Parametric Effect Monads and Semantics of Effect Systems. ACM SIGPLAN Notices - POPL '14, 49 (2014), issue 1, pp. 633-645.
  8. (Joint work with Soichiro Fujii and Paul-André Melliès) Towards a Formal Theory of Graded Monads. In Proc. FoSSaCS 2016, LNCS, 9634 (2016), pp. 513-530.