1994 Fiscal Year Final Research Report Summary
EXPLANATION-BASED LEARNING AND REFORMATION FOR PROGRAM GENERATION,TRANSFORMATION,AND VERIFICATION
| Project/Area Number |
04650298
|
|---|
| Research Category |
Grant-in-Aid for General Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
情報工学
|
|---|
| Research Institution | Hokkaido University |
|---|
Principal Investigator |
KURIHARA Masahito Hokkaido Univ., Fac.of Eng., Associate Professor, 工学部, 助教授 (50133707)
|
|---|
| Project Period (FY) |
1992 – 1994
|
| Keywords | Term rewriting system / Program generation / Termination / Verification / EBL / Completion / Reflection / Module |
|---|
| Research Abstract |
This research aims at developing foundations and applications of explanation-based learning (EBL) techniques for the domain of program generation, transformation, and verification, which is one of the most active area of research field in software science. The results of the research are divided into five parts, each corresponding to a single chapter of the final report. The first two results provide the theoretical foundation of the research, while the other three present the results concerning verification, generation, and transformation, respectively. The are summarizad as follows :
1.Meta-facility for a class of equational languages has been developed. This ensures that EBL mechanisms can be incorporated in the reflective framework of the languages.
2.Modularity in the framework of equational languages has been studied. In paticular, the modularity of simple termination, which plays an important role in verification and generation, has been formally proved.
3.The EBL has been applied to the verification of termination of term rewriting systems. The technique has successfully improved the efficiency of the overall system.
4.The EBL has been applied to the program generation based on Kunth-Bendix completion of term rewriting systems. The technique has allowed us to develop an efficient procedure for completion with multiple reduction orderings.
5.A program tarnsformation technique which preserves termination has been studied and applied to the analysis of composable combination of term rewriting systems. The EBL is related to the process of generalizing known techniques of tranformation.
|
