Fundamental properties of rewriting systems and evaluation strategy of functional programs
| Project/Area Number |
05680272
|
|---|
| Research Category |
Grant-in-Aid for General Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | MIE UNIVERSITY |
|---|
Principal Investigator |
OYAMAGUCHI Michio Mie University, Faculty of Engineering, Professor, 工学部, 教授 (50111828)
|
|---|
| Project Period (FY) |
1993 – 1994
|
| Project Status |
Completed (Fiscal Year 1994)
|
| Budget Amount *help |
¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 1994: ¥300,000 (Direct Cost: ¥300,000)
Fiscal Year 1993: ¥400,000 (Direct Cost: ¥400,000)
|
|---|
| Keywords | Term Rewriting Systems / Church-Rosser / E-overlapping / Non-omega-overlapping / simple-right-linear / Depth-preserving / Sequence-normalizing / 非E重なり / 非W重なり / 右定項TRS |
|---|
| Research Abstract |
Church-Rosser (CR) is an important property of term rewriting systems (TRS). Many sufficient conditions for this property have been obtained under the assumption that TRS's are linear or finite-terminating. On the other hand, for nonlinear and nonterminating TRS's, few results on the CR property have been obtained. Recently, we proposed two new approaches called the E-graph and conditional linearization ones, and obtained some new sufficient conditions for CR of nonlinear and nonterminating TRS's.
The purpose of this research is to develop our previous researches further. We have first shown that both non-E-overlapping and non-omega-overlapping are decidable and sufficient conditions for CR of right-ground TRS's. Next, we have shown that non-E-overlapping is also a sufficient condition for CR of simple-right-linear TRS's which properly include the class of right-ground TRS's. Moreover, we have considered the CR property of E-over-lapping TRS's and succeeded in obtaining some sufficient conditions for CR based on the analysis of the E-critical pairs.
In this research we have also succeeded in unifying the two different approached, i.e., the E-graph and conditional linearization ones by introducing the notion of sequence-normalizability. Using this unified approach we have obtained some sufficient conditions for CR which are a generalization of the previous ones. Furthermore, we have considered the CR property of non-simple-right-linear TRS's and showed that non-E-overlapping is a sufficient condition for CR of the class of strongly depth-preserving TRS's.
By the above results obtained by this research, our proposed plan for the CR property of TRS's has completely been achieved. This research project has also made a basic research in the reduction strategy of TRS's and an efficient implementation of functional programs, and obtained some new results.
|
Report
(3 results)
Research Products
(19 results)
