Program verification based on higher order rewriting systems
| Project/Area Number | 07680347 |
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology, Hokuriku |
|---|
Principal Investigator |
TOYAMA Yoshihito Japan Advanced Institute of Science and Technology, Hokuriku, Computer Science Department, Professor, 情報科学研究科, 教授 (00251968)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
SAKAI Masahiko Nagoya University, Graduate School of Engineering, Associate Professor, 大学院・工学研究科, 助教授 (50215597)
|
|---|
| Project Period (FY) |
1995 – 1997
|
| Project Status |
Completed(Fiscal Year 1997)
|
| Budget Amount *help |
¥700,000 (Direct Cost : ¥700,000)
Fiscal Year 1997 : ¥400,000 (Direct Cost : ¥400,000)
Fiscal Year 1996 : ¥300,000 (Direct Cost : ¥300,000)
|
|---|
| Keywords | term rewriting system / higher order rewriting / confluence property / termination / reduction |
|---|
| Research Abstract |
We have studied the termination property, the confluence property, and the reduction strategy of rewriting systems, which are the basis of higher order rewriting techniques. Through theoretical analysis and experiment, we have obtained the following results :
(1) An extended recursive decomposition ordering for higher order rewriting systems is proposed. This recursive decomposition ordering is useful for proving termination of higher order rewriting systems.
(2) Composable properties of term rewriting systems is presented. The key idea of our composability result is a top-down labeling. Using this labeling, it is proven that modular properties are composable for a naive sort attachment.
(3) It is shown that index reduction is normalizing for the class of stable balanced joinable strong sequential systems. This result offers the basis of effective computation methods of functional language.
(4) The modular property of left-linear complete term rewriting systems is proven, which is important in building algebraic specifications.
(5) We give an operational semantics of priority term rewriting systems by using conditional systems. By defining the class of strong sequential systems, we show that the index rewriting gives a normalizing strategy for priority term rewriting systems.
|
Report
(4results)
Research Products
(28results)
