A rationale for conditional equational programming

Nachum Dershowitz, Mitsuhiro Okada

研究成果: Article査読

62 被引用数 (Scopus)


Conditional equations provide a paradigm of computation that combines the clean syntax and semantics of LISP-like functional programming with Prolog-like logic programming in a uniform manner. For functional programming, equations are used as rules for left-to-right rewriting; for logic programming, the same rules are used for conditional narrowing. Together, rewriting and narrowing provide increased expressive power. We discuss some aspects of the theory of conditional rewriting, and the reasons underlying certain choices in designing a language based on them. The most important correctness property a conditional rewriting program may posses is ground confluence; this ensures that at most one value can be computed from any given (variable-free) input term. We give criteria for confluence. Reasonable conditions for ensuring the completeness of narrowing as an operational mechanism for solving goals are provided; these results are then extended to handle rewriting with existentially quantified conditions and built-in predicates. Some termination issues are also considered, including the case of rewriting with higher-order terms.

ジャーナルTheoretical Computer Science
出版ステータスPublished - 1990

ASJC Scopus subject areas

  • 理論的コンピュータサイエンス
  • コンピュータ サイエンス(全般)


「A rationale for conditional equational programming」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。