菊池 健太郎

〒980-8577 宮城県 仙台市 青葉区 片平 2-1-1
東北大学 電気通信研究所 コンピューティング情報理論研究室 助教 (動画

研究業績の説明

専門分野は、情報科学・コンピュータサイエンスの理論に関係する領域である 「ソフトウェア基礎」、「プログラム理論」、「数理論理学」 です。
これまでの研究業績につきまして、以下の3つの分野に分けて説明します。(クリックすると説明を見ることができます。)

(A) 数理論理学・非古典論理関係(研究業績一覧の論文[12][15][18][19][20][21][30][32][33][35])
数理論理学・非古典論理関係は、 様相論理や直観主義論理といった主にクリプキ意味論によって特徴付けられる非古典論理に関する研究です。 博士学位論文[30]では、 直観主義論理のクリプキ意味論を一般化することによって得られる命題論理に対してシーケント計算の体系を提案し、 カット除去定理などの証明論的な考察を行いました。 そこで得られた成果や関連する内容の論文は、国際学術雑誌で発表しました[18][19][20][21]。

その後、 東京工業大学で修士号を修めた石垣良氏との共同研究で、 それらの結果を述語論理に拡張することを試み、 木構造を持つシーケント計算の体系による形式化を行いました。 その研究成果は、 石垣氏との共著論文[12][15]で発表しました。 論文[12]は国際会議論文ですが、 この国際会議TABLEAUXは採録難度が高め(当該年は投稿43本中16本受理)で、 Microsoft Academic Searchのコンピュータサイエンス部門 (下記「参考となる指標」を参照) にも掲載されている伝統ある会議であり、 上記の国際学術雑誌論文[15][18][19][20][21]に掲載された内容よりも優れた研究成果であると考えられます。

(B) ラムダ計算・型理論関係(研究業績一覧の論文[7][8][9][10][11][13][14][16][17][25][28][29])
ラムダ計算・型理論関係は、 博士の学位を取得した後に日本学術振興会特別研究員(PD)として千葉大学の数学・情報数理学科で本格的に着手して以来取り組んでいる研究テーマです。 ラムダ計算と型理論は、 関数型プログラミング言語と密接な関係があることが知られており、 カリー・ハワードの対応を通して考えると、 直観主義論理の自然演繹の体系における証明図は関数型プログラム(ラムダ項)に、 計算の実行(ベータ簡約)は証明図の正規化に相当します。

直観主義論理に対するシーケント計算の体系においても同様な対応が成り立つかどうかは、 多くの研究者によって興味を持たれていましたが、 2000年頃までは明らかになっていませんでした。 論文[17]で、 説明者は、 型付きラムダ計算のベータ簡約が、 直観主義論理に対するHerbelin流のシーケント計算においてどのような証明図の変換(カット除去手続き)に対応するのかを明確にし、 その上で、 明示的代入計算の手法を用いて、 変換の停止性の直接的な証明を与えました。 この結果は、 シーケント計算に基づく型システムに対する最も基本的なものであるため、 様々な方向へ拡張することが可能です。

論文[10]では、 論文[17]で扱った項計算を拡張することにより、 例外処理などの制御機構を実現可能な計算体系に対応する古典論理の自然演繹における正規化手続きと、 シーケント計算におけるカット除去手続きの対応関係を明らかにし、 それを利用して、 古典論理に対して停止性と合流性をみたす局所ステップカット除去手続きを提案しました。 また、 直観主義論理に対する通常のシーケント計算において、 自然演繹の正規化手続きがどのようなカット除去手続きに対応するのかについても明らかにし[16]、 ラムダ計算のベータ簡約を模倣するために十分な能力をもつカット除去手続きの停止性と合流性を証明しました[11][14]。 さらに、 論文[17]で扱った項計算に対する交差型システムを定義し、 その型付け可能性によって停止性を特徴づけることができることを示しました[13]。

(C) プログラム検証・書き換えシステム関係(研究業績一覧の論文[1][2][3][4][5][6][22][23][24][26][27])
プログラム検証・書き換えシステム関係は、 現在所属している研究室の主要テーマであり、 説明者も参加して共同で研究しています。 この研究では、 書き換えシステムの手法に基づいてプログラムが満たすべき性質を数学的に証明することによりプログラムの正しさを保証することを一つの目的としています。 この分野での業績は、 (i)文脈を操作するプログラム変換を利用した末尾再帰プログラムの性質の検証に関する論文[4][6][24][27] と (ii)束縛変数の利用を可能とした高階書き換えシステムに関する論文[1][2][3][5][22][23][26] に分類されます。 以下では、(i)、(ii)それぞれの研究の意義と成果について簡単に説明します。

(i) 一般に、 関数型言語で書かれたプログラムは、 関数の再帰的な定義に基づいているため、 帰納法による性質の証明に適していますが、 効率を考慮して末尾再帰的な定義で書かれた関数の性質に対しては、 帰納法による証明において、 自明でない補題の発見を必要とする場合が多くなります。 この研究では、 文脈を操作するプログラム変換を用いて、 末尾再帰関数をそれと等価な非末尾再帰関数に変換し、 変換後の関数定義に基づいて帰納法による証明を行うというアプローチをとります。 説明者らが行った実験によれば、 このアプローチのほうが、 末尾再帰関数の定義を直接用いた証明を試みる中で補題を生成するという方法よりも良い結果が得られました[6]。 なお、 手続き型言語のプログラムの性質の検証を、 末尾再帰による関数型プログラムへの変換を通して行える可能性があるということも、 この手法の動機の一つです。

(ii) 従来の一階述語論理の項に対する書き換えシステムに基づく手法を、 束縛変数を伴う項に対する書き換えシステムに基づく手法に拡張します。 そのような手法は、 プログラミング言語自体を規定する体系(例えば、型システムなど)の性質を証明する際に特に有効であると考えられます。 説明者らは、 束縛変数の名前換えについても対象レベルで形式的に扱う名目書き換えシステムに対して、 検証のための手法で必要となる合流性や危険対の性質に関する成果を得ました。

書き換えシステム分野の概要と目的については、 浜名先生(群馬大学)のチュートリアルが大変分かりやすく、 参考になります。

参考となる指標

国際会議の格付けに関するMicrosoft Academic Searchのページ(コンピュータサイエンス部門)によると、 論文[1][2][4][5][8][9][11][12][13][14][16][17]の会議が全3524会議中上位3分の1以内にランクインされています。 (論文[2]の会議IJCARはCADE、FroCoS、TABLEAUXの合同会議として算出。)

また、 現時点で唯一の日本語の学術雑誌論文である論文[6]は、 日本ソフトウェア科学会第21回研究論文賞を受賞することになりました。

インパクトファクターとジャーナルの名声を評価するその他の指標

計算機科学分野における論文出版 by 青戸先生(新潟大学)