京都大学数理解析研究所

紹 介

　計算機科学の一分野にプログラミング言語の意味論がある。これはプログラミ ング言語が供える機構を数学的および論理学的にモデリングして言語の性質を 調べ，得られた知見を実際の言語の設計や改良に還元する研究分野である。こ の分野においてラムダ計算の部分モデルの構成とプログラム変換に関して研究 を行なっている。
　言語のあるモデルの部分モデルを構成するのは言語の性質を調べる上で有用な テクニックである。[1]ではラムダ計算の部分モデルの構築法である論理関係 をMoggiの計算的メタ言語に拡張する手法(意味論的TT-lifting)を提案した。意 味論的TT-lifting の特徴はパラメータを変える事で様々な論理関係を導く事が できる点にある。この柔軟さを応用して[2]では直和型のあるラムダ計算の定義 可能性の特徴付けを(意味論的TT-liftingの特殊化である) TT-closure により与 えた。別の応用として[3]では，副作用を持つプログラムを二つのモナド的意味論 により解釈した時，それらの間にある関係が成立することを示すための十分条件を 与えた。この結果は幅広いクラスの意味論に対して適用でき，副作用を持つプ ログラミング言語の意味論の比較や，安全性の検証に有用であると考えてい る。近年は、プログラム実行時の副作用を型理論的に見積もる 体系である効果システムの健全性の証明にTT-lifting を応用する研究を行っている。
　一方，[4]では京都大学理学部数学科の西村進氏と共同でプログラム変換の一 手法である融合変換の研究を行った。古典的な融合変換は累積変数と呼ばれる 余分なパラメータを持つ関数をうまく扱えないという問題があり，この解決は 融合変換の一つのテーマである。先行研究の多くはこの問題に構文的にアプロー チしているのに対し，[4]において我々は代数的な枠組みを構築して取り組み， 限定的ではあるが先行研究と同等の結果を簡潔に得られる事を示した。
　累積変数付きの関数の融合変換を再帰的定義を用いて行う方法，例えば Vöigtlander氏のlazy compositionや西村氏の高階削除という手法は属性文法 のdescriptional compositionという手法を背景としていることが知られてい る。[4]の研究後，これらの融合変換と属性文法の両者をシステマティックに分 析，導出する枠組として，トレース付きモノイダル圏における属性文法の定式 化を[5]で提案した。この定式化を押し進め，[6]では構文上の属性文法をトレー スを保つある種の関手として，またそれらの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. Relating Computational Effects by TT-Lifting. To appear in Proc. ICALP 2011, LNCS.
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. Attribute Grammars and Categorical Semantics. In Proc. ICALP 2008, Part II, LNCS 5126, pp. 271-282.
6. Categorical Descriptional Composition. In Proc. APLAS 2010, LNCS 6461, pp.222-238.