A rationale for conditional equational programming

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.

Authors

• Nachum Dershowitz
• Mitsuhiro Okada

Keywords

No keywords are indexed for this paper.