Program verification based on higher order rewriting systems

基于高阶重写系统的程序验证

• 批准号: 07680347
• 负责人: TOYAMA Yoshihito
• 金额: $ 0.45万
• 依托单位: Japan Advanced Institute of Science and Technology, Hokuriku
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 1995
• 资助国家: 日本
• 起止时间: 1995 至 1997
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-07680347/
• 关键词: term rewriting system; higher order rewriting; confluence property; termination; reduction

We have studied the termination property, the confluence property, and the reduction strategy of rewriting systems, which are the basis of higher order rewriting techniques. Through theoretical analysis and experiment, we have obtained the following results :(1) An extended recursive decomposition ordering for higher order rewriting systems is proposed. This recursive decomposition ordering is useful for proving termination of higher order rewriting systems.(2) Composable properties of term rewriting systems is presented. The key idea of our composability result is a top-down labeling. Using this labeling, it is proven that modular properties are composable for a naive sort attachment.(3) It is shown that index reduction is normalizing for the class of stable balanced joinable strong sequential systems. This result offers the basis of effective computation methods of functional language.(4) The modular property of left-linear complete term rewriting systems is proven, which is important in building algebraic specifications.(5) We give an operational semantics of priority term rewriting systems by using conditional systems. By defining the class of strong sequential systems, we show that the index rewriting gives a normalizing strategy for priority term rewriting systems.

我们已经研究了终止属性，汇合属性以及重写系统的减少策略，这是高阶重写技术的基础。通过理论分析和实验，我们获得了以下结果：（1）提出了高阶重写系统的扩展递归分解顺序。此递归分解顺序可用于证明终止高阶重写系统的终止。（2）介绍了术语重写系统的合并属性。我们合成性结果的关键思想是自上而下的标签。使用此标签，证明模块化属性是可用于幼稚排序附件的组合性能。（3）证明，索引还原是稳定平衡的可加入强序系统的均等范围。该结果提供了有效的功能语言计算方法的基础。（4）证明了左线完整术语重写系统的模块化属性，这对于构建代数规格很重要。（5）我们通过使用条件系统给出了优先术语重写系统的操作语义。通过定义强序系统类别，我们表明索引重写为优先级重写系统提供了正常化的策略。

项目成果

長谷崇: "重なりのある強遂次系のインデックス簡約について" 信学技報. COMP96-32. 39-48 (1996)

Takashi Hase：“关于具有重叠的强顺序系统的索引缩减”IEICE COMP96-32 (1996)。

M.Sakai: "Left-incompatible term rewritisg systems and functional strategy" IEICE Trons.on Information andSystem. E88-D. 1176-1182 (1997)

M.Sakai：“左不兼容术语重写系统和功能策略”IEICE Trons.on 信息和系统。

T.Aoto: "Persistency of confluence" J.of Universal Comput.Sci.3. 1134-1147 (1997)

T.Aoto：“融合的持久性”J.of Universal Comput.Sci.3。

佐賀正芳: "リスト生成法に基づくプログラム変換" 電気関係学会北陸支部連合大会予稿集(1997). 287-287 (1997)

Masayoshi Saga：“基于列表生成方法的程序转换”北陆电气工程学会分会联合会论文集（1997）287-287（1997）。

高橋宜孝: "条件付き項書き換え系の合流性について" 信学会論文誌. J79-D-1 No.11. 897-902 (1996)

Yoshitaka Takahashi：“论条件术语重写系统的汇合”，IEICE 研究所汇刊 J79-D-1 No. 897-902 (1996)。