Program verification based on higher order rewriting systems

点击翻译按钮获取中文摘要

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.