2005 Fiscal Year Final Research Report Summary
Study on Rewriting Theory for Analysis, Verification and Efficient Execution of Functional Programs
| Project/Area Number |
15500007
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
SAKAI Masahiko Nagoya University, Grad.School of Information Science, Prof., 大学院・情報科学研究科, 教授 (50215597)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
SAKABE Toshiki Nagoya Univ., Grad.School of Information Science, Prof., 大学院・情報科学研究科, 教授 (60111829)
KUSAKARI Keiichirou Nagoya Univ., Grad.School of Information Science, Lecturer, 大学院・情報科学研究科, 講師 (90323112)
NISHIDA Naoki Nagoya Univ., Grad.School of Information Science, Aesearch Associate, 大学院・情報科学研究科, 助手 (00397449)
KASUYA Hideto Auchi Prefectural Univ., School of Information Science, Research Associate, 情報科学部, 助手 (10295579)
|
|---|
| Project Period (FY) |
2003 – 2005
|
| Keywords | term rewriting system / functional language / normalizing strategy / termination proof / implicit induction / outer-most strategy |
|---|
| Research Abstract |
This research is toward removing gaps that prevent from applying results of term rewriting systems (TRS for short) to fuctional languages. The following results were obtained ;
(1) The previously proposed dependency pair method for proving termination of higher-order rewrite systems cannot be applied for ones containing nested variable in a right-hand side and containing copy rules. We succeeded to remove the strong restriction from it for proving termination of simple-typed rewriting systems.
(2) We showed that the needed redexes with respect to strong sequential or NV approximation are decidable by using tree-automata technique and the de Bruijn notations.
(3) It appeared that theorems provable by implicit induction in higher-order rewrite systems are the subclass of the inductive theorems. The case happens that some inductive theorems are judged to be not inductive. We gave a condition to prevent this situation.
(4) We gave a condition that guarantees the outer-most reduction strategy to be complete for overlapping TRSs, and showed a transformation of TRSs that produce TRSs that satisfy the condition.
(5) We developed a transformation of TRSs whose outputs define the inverse computation of the input constructor TRSs. In the computation, innermost narrowing is effective for obtaining all results in case of linear TRSs with extra variables.
|
