2005 Fiscal Year Final Research Report Summary
Program verification method based on reduction approximations
| Project/Area Number |
14580357
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
TOYAMA Yoshihito Tohoku University, Research Institute of Electrical Communication, Professor, 電気通信研究所, 教授 (00251968)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
AOTO Takahito Tohoku University, Research Institute of Electrical Communication, Associate Professor, 電気通信研究所, 助教授 (00293390)
KIKUCHI Kentarou Tohoku University, Research Institute of Electrical Communication, Research Associate, 電気通信研究所, 助手 (40396528)
|
|---|
| Project Period (FY) |
2002 – 2005
|
| Keywords | reduction system / needed reduction / negular preserving approximation / normalizing strategy / external reduction / balanced weak confluence |
|---|
| Research Abstract |
To propose program verification techniques based on reduction approximations, we have studied. rewriting theories among normalization reduction strategies, program transformation by template, termination of higher-order rewriting systems, automated proving for higher-order inductive theorems, decidability of reachability problem. Thorough theoretical analysis and experiments, we have obtained the following results.
(1)We proposed the notion of normalizing strategy based on balanced weak confluence. It was shown that external reduction is a normalizing strategy for left-linear term rewriting systems if every critical pair is root balanced joinable. This results expands normalizing strategy of needed reduction. We also presented that external reduction is a computable reduction strategy if regular preserving approximation if it exits.
(2)We developed a framework of program transformation by template based on rewriting systems. The correctness of our program transformation method is proven without explicit use of induction on data structures. Thus our program transformation system can easily incorporate with automated theorem provers.
(3)We introduce the notion of growing approximation, which is a generalization of strong sequential approximation, NV-sequential approximation and right-linear growing approximation. We have shown that the growing approximation extends the class of term rewriting systems having a decidable normalizing strategy. Moreover, the decidability of confluence and termination for growing systems is presented.
|
