所員 -勝股 審也-

名前 勝股 審也 (Katsumata, Shin-ya)
助教
E-Mail sinya (emailアドレスには@kurims.kyoto-u.ac.jp をつけてください)
研究内容 理論計算機科学の研究
紹 介
 計算機科学の一分野にプログラミング言語の意味論がある。これはプログラミ ング言語が供える様々な機構を数学的および論理学的にモデル化して調べ,得ら れた知見を実際の言語の設計や改良に還元する研究分野である。この分野にお いてラムダ計算の部分モデルの構成とプログラム変換に関して研究を行なって いる。
 プログラミング言語の性質を調べることの多くは,「任意のプログラム の解釈がある性質を満たす」ことを示す問題に帰着される。この問題を解くに は,その性質の中から部分モデルを切り出せばよく,特にラムダ計算では 論理関係と呼ばれる手法が頻繁に用いられてきた。 論理関係はラムダ計算の構造に依 存して定義されるため,90年代に入り,ラムダ計算をモナド で拡張して プログラミング言語の持つ様々な機構を表現することが提案されると,モナド に対する論理関係の定義が様々な研究で問題となった。
 これに対し,[2]で意味論的$TT-lifting$というモナドのための論 理関係を与える手法を提案した。この手法の特徴はパラメータを変える事で様々 な論理関係を導く事ができる柔軟さにある。この柔軟さを応用し,[6]で,副作 用を持つプログラムを二つのモナド的意味論により解釈した時,両者の間にあ る関係が成立することを示すための十分条件を与えた。この結果は幅広いクラ スの意味論に対して適用でき,副作用を持つプログラミング言語の意味論の比 較や,安全性の検証に有用である。また,京都大学数理解析研究所の佐藤哲也 氏と共同で,モナド上の前順序に関する研究を行った[7]。モナドの前順序 は,Kleisli圏に前順序による豊穣化を与える他,余代数間の模倣関係の特徴付 けに応用されている。本研究はモナドの前順序の集まりが射影的極限になってい ることを示し,これをもとに具合的なモナドの前順序を列挙した。
 一方,関数型プログラミングに関連する話題として,融合変換 の研究も 行ってきた。累積変数付きの関数の融合変換を再帰的定義を用いて行う手法 は属性文法のdescriptional compositionという 手法を背景としているこ とが知られている。[4]の研究後,これらの融合変換と属性文法の 両者をシステマティックに分析,導出する枠組として,トレース付きモノイダ ル圏における属性文法の定式化を[3]で提案した。この定式化を 押し進め,[5]では構文上の属性文法をトレースを保つある種の 関手として,またそれらの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. A Characterisation of Lambda Definability with Sums via TT-Closure Operators. In Proc. CSL 2008, LNCS, 5213, pp. 277-291.
  3. Attribute Grammars and Categorical Semantics. In Proc. ICALP 2008, Part II, LNCS 5126, pp. 271-282.
  4. (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.
  5. Categorical Descriptional Composition. In Proc. APLAS 2010, LNCS 6461, pp.222-238.
  6. Relating Computational Effects by TT-Lifting. Information and Computation (Special issue on ICALP 2011), 222 (2013), pp. 228-246.
  7. (Joint work with Tetsuya Sato) Preorders on Monads and Coalgebraic Simulations. In Proc. FoSSaCS 2013, LNCS, 7794 (2013), pp. 145--160.