メタ等式プログラミングに関する基礎的研究

本研究では、メタ等式プログラミングの基礎を確立することを目的として、すでに本研究代表者のグループで提案している等式を用いたメタプログラミングのための計算モデルである動的項書換え計算(DTRC)についての研究を進めるとともに、それを単純化ならびに拡張して、新たにメタ項書換え計算(MTRC,Meta-Term Rewriting Calculus)を提案し、MTRCの表現能力を検証した。さらに、任意有限のメタレベルの計算を表現するための計算モデルの研究にも着手した。具体的な研究内容は次の通りである。(1)DTRC上で条件つき項書換え系の実行系を実現し、条件つき項書換え系の解析にDTRCの解析手法が適用できる可能性があることを示した。(2)等式理論の帰納的定理の証明法である構造帰納法、被覆集合帰納法の証明過程の記述ができることを示した。すなわち、与えられた等式理論と証明すべき等式をMTRC項に変換するアルゴリズムを与え、変換先のMTRC項の書換え結果がtrueになれば証明成功と判断できることを示した。さらに、MTRCのインタプリタを関数型プログラム言語MLで実現し、実際に自然数上の可算の結合性、可換性の証明がほとんど自動的に行なえることを明らかにした。(3)whileプログラムのMTRCへの翻訳アルゴリズムを示すとともに、Hoare公理系でのプログラム検証過程をMTRCで記述できることを示した。(3)さらに、MTRCがメタレベル1のメタ計算を表現するのに対して、任意有限のメタレベルのメタ計算を表現できる計算モデルωMRCを提案し、その意味論について検討を加えた。

本研究では、メタ等式プログラミングの基礎を確立することを目的として、すでに本研究代表者のグループで提案している等式を用いたメタプログラミングのための計算モデルである動的項書換え計算(DTRC)についての研究を進めるとともに、それを単純化ならびに拡張して、新たにメタ項書換え計算(MTRC,Meta-Term Rewriting Calculus)を提案し、MTRCの表現能力を検証した。さらに、任意有限のメタレベルの計算を表現するための計算モデルの研究にも着手した。具体的な研究内容は次の通りである。(1)DTRC上で条件つき項書換え系の実行系を実現し、条件つき項書換え系の解析にDTRCの解析手法が適用できる可能性があることを示した。(2)等式理論の帰納的定理の証明法である構造帰納法、被覆集合帰納法の証明過程の記述ができることを示した。すなわち、与えられた等式理論と証明すべき等式をMTRC項に変換するアルゴリズムを与え、変換先のMTRC項の書換え結果がtrueになれば証明成功と判断できることを示した。さらに、MTRCのインタプリタを関数型プログラム言語MLで実現し、実際に自然数上の可算の結合性、可換性の証明がほとんど自動的に行なえることを明らかにした。(3)whileプログラムのMTRCへの翻訳アルゴリズムを示すとともに、Hoare公理系でのプログラム検証過程をMTRCで記述できることを示した。(3)さらに、MTRCがメタレベル1のメタ計算を表現するのに対して、任意有限のメタレベルのメタ計算を表現できる計算モデルωMRCを提案し、その意味論について検討を加えた。