Application of Conditional Rewrite Systems to Declarative Programming Languages

我们的研究目标是调查的条件重写系统作为一个计算模型的声明式编程语言。我们研究缩小，因为它是基本的函数逻辑语言，一类声明式编程语言的计算机制。主要研究结果如下：1.我们设计了两个缩窄演算OINC（Outside-In Narrowing Calculus）和LNC（Lazy Narrowing Calculus），以给出声明式编程语言的计算机制。这两个演算使我们能够将在函数式编程语言中开发的延迟求值的概念纳入函数式逻辑编程语言。对于一类项重写系统，我们也得到了这些演算的完备性结果.本文提出了重写规则右侧带有额外变量的条件重写系统的水平汇合的一个句法充分条件。层次汇合是保证条件重写系统收缩完备性的一个重要性质。利用这一结果，我们给出了一个新的具有额外变量的条件重写系统收缩完备性的充分条件.我们研究了声明式编程语言的条件缩小和模型之间的关系。针对基于严格方程的两种典型的函数逻辑语言模型，我们证明了条件缩窄是合理和完备的.为了将条件重写系统的性质应用到声明式编程语言的Meta编程中，我们研究了条件重写系统的模块性质。我们在模块化的条件重写系统中显示了额外变量的水平汇合。

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.