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
Externally publishedYes

Fingerprint

Functional programming
Logic programming
Rewriting
LISP (programming language)
Programming
Functional Programming
Confluence
Semantics
Logic Programming
Prolog
Expressive Power
Term
Predicate
Termination
Property A
Completeness
Correctness
Paradigm
Higher Order

ASJC Scopus subject areas

  • Computational Theory and Mathematics

Cite this

A rationale for conditional equational programming. / Dershowitz, Nachum; Okada, Mitsuhiro.

In: Theoretical Computer Science, Vol. 75, No. 1-2, 1990, p. 111-138.

Research output: Contribution to journalArticle

Dershowitz, Nachum ; Okada, Mitsuhiro. / A rationale for conditional equational programming. In: Theoretical Computer Science. 1990 ; Vol. 75, No. 1-2. pp. 111-138.
@article{aa6b10063c7041a6941d18bccdf31036,
title = "A rationale for conditional equational programming",
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.",
author = "Nachum Dershowitz and Mitsuhiro Okada",
year = "1990",
doi = "10.1016/0304-3975(90)90064-O",
language = "English",
volume = "75",
pages = "111--138",
journal = "Theoretical Computer Science",
issn = "0304-3975",
publisher = "Elsevier",
number = "1-2",

}

TY - JOUR

T1 - A rationale for conditional equational programming

AU - Dershowitz, Nachum

AU - Okada, Mitsuhiro

PY - 1990

Y1 - 1990

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=0025489167&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0025489167&partnerID=8YFLogxK

U2 - 10.1016/0304-3975(90)90064-O

DO - 10.1016/0304-3975(90)90064-O

M3 - Article

AN - SCOPUS:0025489167

VL - 75

SP - 111

EP - 138

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

IS - 1-2

ER -