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)利用条件系统给出了优先项重写系统的操作语义。通过定义强序列系统类，我们证明了索引重写给出了优先项重写系统的一个规范化策略。

项目成果

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 信息和系统。

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

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

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）。

Y.Toyama: "Termination for the direct sumof left-linear complete term rewriting systems" J.ACM. 42. 1275-1304 (1995)

Y.Toyama：“左线性完整项重写系统的直和的终止”J.ACM。