Application of Conditional Rewrite Systems to Declarative Programming Languages

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

The objective of our research is the investigation of conditional rewrite systems as a computational model of declarative programming languages. We study narrowing since it is fundamental to give a computational mechanism of functional-logic languages, a class of declarative programming languages. The results we obtained are as follows.1. We designed two narrowing calculi called OINC (Outside-In Narrowing Calculus) and LNC ( Lazy Narrowing Calculus) in order to give computational mechanisms of declarative programming languages. The two calculi enable us to incorporate the notion of lazy-evaluation, developed in functional programming languages, into functional-logic programming languages. We also obtained completeness results of these calculi for a class of term rewriting systems.2. We Proposed a syntactic sufficient condition for level-confluence of conditional rewrite systems with extra variables in the right-hand side of their rewrite rules. Level-confluence is an important property to guarantee completeness of narrowing for condtional rewrite systems. Using this result, we showed a new sufficient condition for completeness of narrowing for conditional rewrite systems with extra variables.3. We investigated a relationship between conditional narrowing and models of declarative programming languages. We showed conditional narrowing is sound and complete with respect to two typical models of functional-logic languages based on strict equations.4. In order to apply properties of conditional rewrite systems to meta programming in declarative programming languages, we investigated modular properties of conditional rewrite systems. We showed level-confluence in modular for conditional rewrite systems with extra variables.