| Project/Area Number |
04680031
|
|---|
| Research Category |
Grant-in-Aid for General Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Informatics
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
坂部 俊樹 名古屋大学, 工学部, 助教授 (60111829)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
山本 晋一郎 名古屋大学, 工学部, 助手 (40240098)
結縁 祥治 名古屋大学, 工学部, 助手 (70230612)
酒井 正彦 名古屋大学, 工学部, 助手 (50215597)
平田 富夫 名古屋大学, 工学部, 助教授 (10144205)
稲垣 康善 名古屋大学, 工学部, 教授 (10023079)
|
|---|
| Project Period (FY) |
1992
|
| Project Status |
Completed (Fiscal Year 1992)
|
| Budget Amount *help |
¥1,800,000 (Direct Cost: ¥1,800,000)
Fiscal Year 1992: ¥1,800,000 (Direct Cost: ¥1,800,000)
|
|---|
| Keywords | メタプログラミング / メタ等式論理 / 書換え型計算モデル / 構造帰納法 |
|---|
| Research Abstract |
本研究では、メタ等式プログラミングの基礎を確立することを目的として、すでに本研究代表者のグループで提案している等式を用いたメタプログラミングのための計算モデルである動的項書換え計算(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を提案し、その意味論について検討を加えた。
|
