1995 Fiscal Year Annual Research Report
| Project/Area Number |
07680350
|
|---|
| Research Category |
Grant-in-Aid for General Scientific Research (C)
|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
酒井 正彦 北陸先端科学技術大学院大学, 情報科学研究科, 助教授 (50215597)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
山本 晋一郎 名古屋大学, 工学部, 助手 (40240098)
外山 芳人 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (00251968)
|
|---|
| Keywords | 項書換え系 / 合流条件 / 停止条件 / E単一化 |
|---|
| Research Abstract |
本研究は等式論理における検証法の確立し,さらに,一般のソフトウェアを代数的手法を用いて等式論理に自動的に変換することにより,これらの検証への応用を図るものである.
今年度は,停止順序を満たす等式を通常の項書換え規則とみなし,これを満たさない等式は集合としての書換え規則とみなす項集合書換え系の形式的定義を与えた.さらに,(1)停止条件,(2)線形規則における合流条件が明らかになた.
(1)項集合書換え系においては,通常の項書換え系におけるE合同上の書換えよりも緩い条件で停止性を持つことが分かった.
(2)この条件は,停止性を満たし非線形規則を持たない項集合書換え系に対して,その危険対が合流するならば合流性を持つというものである.これは,等式付の項書換え規則に対応させて考えると,Huet(1980)の条件とほぼ同じ結果であるが,本結果の方が(1)の停止条件が緩い分だけ拡張になっている.
また,優先順位つき項書換え系の定義を行ない,その等式論理に基づく意味論を与えた.これにより,関数型プログラムを等式論理に変換して検証するための基礎が与えられた.
|
Research Products
(5 results)
-
[Publications] 酒井正彦: "The Functional Strategy-The Extended Left‐incompatible System" 電子情報通信学会 技術報告. SS95‐17. 55-62 (1995)
-
[Publications] 酒井正彦: "The Semantics of Priority Term Rewriting Systems and their Strong sequentiality" 電子情報通信学会 技術報告. SS95‐40. 31-38 (1996)
-
[Publications] 岩見宗弘: "高階項書換え系の停止性について" 電子情報通信学会 技術報告. COMP95‐85. 113-121 (1996)
-
[Publications] 草刈圭一朗: "非線形項書換え系の合流性について" 電子情報通信学会 技術報告. COMP95‐86. 123-129 (1996)
-
[Publications] 中野賢司: "項書換え系のAC停止性について" 電子情報通信学会 技術報告. COMP(発表予定). (1996)
