| 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
|
| Project Status |
Completed (Fiscal Year 2005)
|
| Budget Amount *help |
¥2,500,000 (Direct Cost: ¥2,500,000)
Fiscal Year 2005: ¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 2004: ¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 2003: ¥900,000 (Direct Cost: ¥900,000)
|
|---|
| 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.
|
