| 研究課題/領域番号 |
08458067
|
|---|
| 研究種目 |
基盤研究(B)
|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
濱口 毅 名古屋大学, 工学部, 助手 (90273284)
|
|---|
| 研究分担者 |
馮 速 名古屋大学, 工学部, 助手 (90262881)
結縁 祥治 名古屋大学, 工学部, 助手 (70230612)
阿草 清滋 名古屋大学, 工学部, 教授 (90026360)
稲垣 康善 名古屋大学, 工学部, 教授 (10023079)
坂部 俊樹 名古屋大学, 工学部, 教授 (60111829)
|
|---|
| キーワード | メタ計算 / 書換え計算 / 項書換え系 / 並行計算 / 検証 / 代数的仕様 / 帰納的定理 / 被覆集合帰納法 |
|---|
| 研究概要 |
本年度の研究実績は以下の通りである。
メタ項書換え計算の前身である動的項書換え計算に関して、その部分クラスに対する合流性の十分条件を与えた。この結果は、メタ項書換え計算へも自然に拡張可能であり、メタ項目書換え計算の解析を行なう時の有力な理論的ツールとなる。
項書換え系の等価性判定に関する研究では、被覆集合帰納法による等価性判定を自動化する次のような手順を明らかにした。
1.与えられた2つの項書換え系から、特性項とよぶ項の集合を抽出する。
2.各々の特性項に対して、次のような条件式を生成する。すべての特性項の条件式が同時に成立することが与えられた項書換え系が等価であることの必要十分条件である。
3.step2の各条件に対して、それが成立することを証明するための被覆集合を生成する。
4.step2の各条件に対する被覆集合帰納法を実行するメタ項書換え計算の項を構成する。
5.step4で得られたメタ項書換え計算の項を評価する。その結果がTRUEであれば、与えられた2つの項書換え系は等価である。
メタ項書換え計算の意味論について、次のような成果を得た。メタ項書換え計算の意味論を定式化するときの基本的なアイデアは次の通りである。項の意味は、その項から抽出できるデータによって定められ、抽出されるデータは、その項をあらゆる「文脈」下において計算した結果得られる項である。このアイデアに基づいてメタ項書換え計算の動的意味論を与えた。この意味論の特徴は、与えられた項に対して、その項の意味を抽出するようなメタ項書換え計算の項を構成でき、さらに、項と項の等価性を帰納法によって証明するためのメタ項書換え計算の項を構成できることである。
|
