2013 年度実施状況報告書

非単調な再帰的定義の新しい基礎理論

研究課題

研究課題/領域番号	25540001
研究種目	挑戦的萌芽研究
研究機関	東北大学
研究代表者	住井英二郎東北大学, 情報科学研究科, 准教授 (00333550)
研究期間 (年度)	2013-04-01 – 2016-03-31
キーワード	プログラム理論 / 再帰 / パラメタ的高階抽象構文 / 環境双模倣
研究概要	平成25年度は、次年度以降の理論の構築に先立ち、主な関連研究を調査・検討した。特に、現時点で最も密接な関連研究と思われる、Hurらの研究[POPL'12,'13]について検討した。[POPL'12]は、Ahmed, Dreyerらのstep-indexつき論理関係と、住井らの環境双模倣を融合し、再帰型と破壊的代入を持つ多相λ計算におけるプログラム等価性に適用した研究である。[POPL'13]は、双模倣（環境双模倣を含む）の核心である余帰納的定義について、環境に類似したパラメタを考えることにより、余帰納法による証明を拡張した研究である。いずれも環境双模倣の直接的追従研究であるだけでなく、一般化を志向していると思われ、本研究と関連が深い。（ただし、推移律(transitivity)が成り立たない等の問題があり、本研究の目的を直に達するものではない。）他に、パラメタ化高階抽象構文(parametrized higher-order abstract syntax, PHOAS)、オブジェクト指向プログラミング言語におけるopen recursion、Hasegawaのトレースつきモノイダル圏に基づく再帰的定義の意味論等についても検討した。当初の研究実施計画には含まれていなかったが、（再帰的データ構造の典型である）リストや木と並んで重要なデータ構造であるグラフの、PHOASを用いた再帰的定義と双模倣についても、既存研究を参考に新たな知見が得られた。
現在までの達成度 (区分)	現在までの達成度 (区分) 2: おおむね順調に進展している理由本研究の目的は、一般的・初等的かつ単純な再帰(recursion)の理論を構築することにある。「再帰」は再帰的データ構造や再帰関数など、プログラム理論をはじめ計算機科学の中核をなす主要な概念の一つである。住井ら[JACM, TCS, POPL'04, POPL'05, LICS'07他]は環境(environment)の概念を用い、プログラム等価性（環境双模倣）の健全・完全かつ初等的で単純な再帰的定義を初めて与えた。本研究は「環境」の着想を一般化し、任意の再帰的定義に適用できるようにすることを目指している。平成25年度は、交付申請書の研究実施計画および上述の「研究実績の概要」に記載したとおり、主な関連研究を調査・検討し、ほぼ予定どおりの知見を得た。（トレースつきモノイダル圏に基づく再帰的定義の意味論については、さらなる調査・検討が必要である。）当初の研究実施計画には含まれていなかったが、（再帰的データ構造の典型である）リストや木と並んで重要なデータ構造であるグラフの、PHOASを用いた再帰的定義と双模倣についても、既存研究を参考に新たな知見が得られた。
今後の研究の推進方策	交付申請書の研究実施計画に記載したとおり、初年度に検討した関連研究に関する知見を活かしつつ、本研究の目的である、環境の着想に基づく一般的・初等的かつ単純な再帰的定義の理論を構築する。環境双模倣は、観察者の知識（既知の値の組の集合）を表す「環境」Eと、観察される実行中のプログラムM,Nとの3つ組(E,M,N)の集合Xであって、観察と実行に関して閉じていることを表す一定の再帰的条件を見たすものと定義される。それらの条件は集合Xの包含関係について単調(monotone)であるため、最大の環境双模倣「～」の定義が成立する(well-defined)。このように、環境の概念を導入することにより、環境を用いなければ論理的に成立しなかった(ill-defined)再帰的定義が可能となる。これを双模倣（プログラム等価性）に限らず、任意の再帰的定義に一般化することを目指す。（再帰的データ構造の典型である）リストや木と並んで重要なデータ構造であるグラフの、PHOASを用いた再帰的定義と双模倣についても、前述の通り既存研究を参考に新たな知見が得られたため、並行して研究を進める。
次年度の研究費の使用計画	物品費・旅費・人件費等の一部は、（使用目的上の問題がない）他予算で購入・雇用した機器・研究補助者や、学術雑誌・インターネット等で新たに公開・交換された文献・メール等により代替することが可能となったため。科学研究費補助金の対象である基礎的研究は土木事業等とは性質が大きく異なり、完全に進展を予測して支出を計画できるものではないが（結果がわかっていたらそれは研究ではない）、今後とも研究の進展にともなう必要に応じて計算機等の購入や、研究打ち合わせ・発表のための旅費等に用いる。