1992 Fiscal Year Annual Research Report
| Project/Area Number |
04680031
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
坂部 俊樹 名古屋大学, 工学部, 助教授 (60111829)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
山本 晋一郎 名古屋大学, 工学部, 助手 (40240098)
結縁 祥治 名古屋大学, 工学部, 助手 (70230612)
酒井 正彦 名古屋大学, 工学部, 助手 (50215597)
平田 富夫 名古屋大学, 工学部, 助教授 (10144205)
稲垣 康善 名古屋大学, 工学部, 教授 (10023079)
|
|---|
| 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を提案し、その意味論について検討を加えた。
|
Research Products
(6 results)
-
[Publications] 坂部 俊樹: "メタプログラミング" 電気関係学会東海支部連合大会予稿集. S6-1-S6-2 (1992)
-
[Publications] Su Feng: "Interpretation of Conditinal Term rewriting Systems by DTRC" 日本ソフトウェア科学会第9回全国大会論文集. 313-316 (1992)
-
[Publications] Shoje Yuen: "An Extension of the Testing Method for Processes Passing Infinite values" Proceedings of the First North American Process Algebra Workshop. 10-1-10-20 (1992)
-
[Publications] 結縁 祥治: "無限構造の値を受け渡す通信プロセスのテスト等価性について" 電子情報通信学会技術研究報告. COMP92-20. 31-40 (1992)
-
[Publications] 大須賀 健: "通信プロセスにおける有限受理グラフを用いた試験等価性の証明法について" 電子情報通信学会技術研究報告. COMP92-72. 39-48 (1992)
-
[Publications] 太郎良 浩次: "木パターンマッチングのための並列アルゴリズム" 電子情報通信学会論文誌. J75-DI. 400-409 (1992)
