EXPLANATION-BASED LEARNING AND REFORMATION FOR PROGRAM GENERATION,TRANSFORMATION,AND VERIFICATION

基于解释的学习和程序生成、转换和验证的改革

• 批准号: 04650298
• 负责人: KURIHARA Masahito
• 金额: $ 1.34万
• 依托单位: Hokkaido University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for General Scientific Research (C)
• 财政年份: 1992
• 资助国家: 日本
• 起止时间: 1992 至 1994
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-04650298/
• 关键词: Term rewriting system; Program generation; Termination; Verification; EBL; Completion; Reflection; Module; 項書き換え系; 変換; リフォーメーション; 真偽維持システム; 学習; 項書換えシステム; プログラム検証; ATMS

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.

本研究旨在为软件科学中最活跃的研究领域之一--程序生成、转换和验证领域的基于推理的学习（EBL）技术奠定基础和应用。研究结果分为五个部分，每个部分对应最后报告的一个章节。前两个结果提供了研究的理论基础，而其他三个分别呈现了关于验证，生成和转换的结果。1.建立了一类方程语言的元工具。这保证了EBL机制可以被纳入语言的反射框架。2.研究了等式语言框架中的模块性。特别地，形式化地证明了在验证和生成中起重要作用的简单终止性的模块性。3.将EBL应用于项重写系统的终止性验证。该技术成功地提高了整个系统的效率。4.将EBL应用于基于Kunth-Benzetron完成的项重写系统的程序生成。该技术使我们能够开发出一个有效的程序完成多个减少订单。5.保持终止的程序转换技术已被研究，并应用于分析的组合项重写系统。EBL与推广已知的转换技术的过程有关。

项目成果

栗原 正仁: "Another representation of integers in logic" Trans.of Information Processing Society of Japan. 34. 536-538 (1993)

Masahito Kurihara：“逻辑中整数的另一种表示” Trans.of 日本信息处理学会 34. 536-538 (1993)。

Masahito Kurihara: "An algebraic specification and an object-oriented implementation of a reflective language" Proc.IMSA'92 International Workshop on Reflection and Meta-level Architecture. 1. 137-142 (1992)

Masahito Kurihara：“反射语言的代数规范和面向对象的实现”Proc.IMSA92 国际反射和元级架构研讨会。

栗原 正仁: "Using ATMS to efficiently verify the termination of rewrite rule programs" International Journal of Software Engineering and Knowledge Engineering. 2. 547-565 (1992)

Masahito Kurihara：“使用 ATMS 有效验证重写规则程序的终止”国际软件工程和知识工程杂志 2. 547-565 (1992)。

M.Kurihara and A.Ohuchi: "Modularity of simple termination of term rewriting systems with shared constructors" Theoretical Comput.Sci.103. 273-282 (1992)

M.Kurihara 和 A.Ohuchi：“具有共享构造函数的术语重写系统的简单终止的模块化”Theoretical Comput.Sci.103。

栗原正仁: "Another representation of integers in logic" 情報処理学会論文誌. 34. 536-538 (1993)

Masahito Kurihara：“逻辑中整数的另一种表示”，日本信息处理学会汇刊 34. 536-538 (1993)。