所員 -勝股 審也-

名前 勝股 審也 (Katsumata, Shin-ya)
助教
E-Mail sinya (emailアドレスには@kurims.kyoto-u.ac.jp をつけてください)
研究内容 理論計算機科学の研究
紹 介
 計算機科学の一分野にプログラミング言語の意味論がある。これはプログラミ ング言語が供える様々な機構を数学的および論理学的にモデル化して調べ, 得ら れた知見を実際の言語の設計や改良に還元する研究分野である。この分野にお いてラムダ計算の部分モデルの構成とプログラム変換に関して研究を行なって いる。
 プログラミング言語の性質を調べることの多くは, 「任意のプログラム の解釈がある性質を満たす」ことを示す問題に帰着される。この問題を解くに は, その性質の中から部分モデルを切り出せばよく, 特にラムダ計算では 論理関係と呼ばれる手法が頻繁に用いられてきた。 論理関係はラムダ計算の構造に依 存して定義されるため, 90年代に入り, ラムダ計算をモナド で拡張して プログラミング言語の持つ様々な機構を表現することが提案されると, モナド に対する論理関係の定義が様々な研究で問題となった。
 これに対し, [1]で意味論的$TT-lifting$というモナ ドのための論理関係を与える手法を提案した。この手法の特徴はパラメータを 変える事で様々な論理関係を導く事ができる柔軟さにある。この柔軟さを応用 し, [5]で, 副作用を持つプログラムを二つのモナド的意味論 により解釈した時, 両者の間にある関係が成立することを示すための十分条件 を与えた。この結果は幅広いクラスの意味論に対して適用でき, 副作用を持つ プログラミング言語の意味論の比較や, 安全性の検証に有用であ る。この研究のテクニックを発展させ, [7]では$TT-lifting$を応用して 一般化されたエフェクトシステムのエフェクト健全性を示した。この他, 京都大学数理解析研究所の佐藤哲也氏と共同で, モナド上の前順序に関する研 究を行った[6]。モナド上の前順序は, Kleisli圏に対し前順序 による豊穣化を与える他, 余代数間の模倣関係の特徴付けに応用されている。 [6]ではモナド上の前順序の集まりが射影的極限になって いることを示し, これをもとに具体的なモナドの上の前順序を列挙した。
 一方, 関数型プログラミングに関連する話題として, 融合変換 の研究も 行ってきた。累積変数付きの関数の融合変換を再帰的定義を用いて行う手法 は属性文法の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.