A rationale for conditional equational programming

Nachum Dershowitz, Mitsuhiro Okada

Research output: Contribution to journalArticle

62 Citations (Scopus)

Abstract

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.

Original languageEnglish
Pages (from-to)111-138
Number of pages28
JournalTheoretical Computer Science
Volume75
Issue number1-2
DOIs
Publication statusPublished - 1990

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'A rationale for conditional equational programming'. Together they form a unique fingerprint.

  • Cite this