Confluence of conditional rewrite systems

Nachum Dershowitz, Mitsuhiro Okada, G. Sivakumar

Research output: Chapter in Book/Report/Conference proceedingConference contribution

41 Citations (Scopus)

Abstract

Conditional rewriting has been studied both from the point of view of algebraic data type specifications and as a computational paradigm combining logic and functional programming. An important issue, in either case, is determining whether a rewrite system has the Church-Rosser, or confluence, property. In this paper, we settle negatively the question whether “joinability of critical pairs” is, in general, sufficient for confluence of terminating conditional systems. We review known sufficient conditions for confluence, and also prove two new positive results for systems having critical pairs and arbitrarily big terms in conditions.

Original languageEnglish
Title of host publicationConditional Term Rewriting Systems - 1st International Workshop, Proceedings
PublisherSpringer Verlag
Pages31-44
Number of pages14
Volume308 LNCS
ISBN (Print)9783540192428
DOIs
Publication statusPublished - 1988 Jan 1
Externally publishedYes
Event1st International Workshop on Conditional Term Rewriting Systems, 1987 - Orsay, France
Duration: 1987 Jul 81987 Jul 10

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume308 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other1st International Workshop on Conditional Term Rewriting Systems, 1987
CountryFrance
CityOrsay
Period87/7/887/7/10

Fingerprint

Functional programming
Religious buildings
Confluence
Logic programming
Specifications
Functional Programming
Rewriting
Logic Programming
Paradigm
Specification
Sufficient
Sufficient Conditions
Term

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Dershowitz, N., Okada, M., & Sivakumar, G. (1988). Confluence of conditional rewrite systems. In Conditional Term Rewriting Systems - 1st International Workshop, Proceedings (Vol. 308 LNCS, pp. 31-44). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 308 LNCS). Springer Verlag. https://doi.org/10.1007/3-540-19242-5_3

Confluence of conditional rewrite systems. / Dershowitz, Nachum; Okada, Mitsuhiro; Sivakumar, G.

Conditional Term Rewriting Systems - 1st International Workshop, Proceedings. Vol. 308 LNCS Springer Verlag, 1988. p. 31-44 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 308 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Dershowitz, N, Okada, M & Sivakumar, G 1988, Confluence of conditional rewrite systems. in Conditional Term Rewriting Systems - 1st International Workshop, Proceedings. vol. 308 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 308 LNCS, Springer Verlag, pp. 31-44, 1st International Workshop on Conditional Term Rewriting Systems, 1987, Orsay, France, 87/7/8. https://doi.org/10.1007/3-540-19242-5_3
Dershowitz N, Okada M, Sivakumar G. Confluence of conditional rewrite systems. In Conditional Term Rewriting Systems - 1st International Workshop, Proceedings. Vol. 308 LNCS. Springer Verlag. 1988. p. 31-44. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/3-540-19242-5_3
Dershowitz, Nachum ; Okada, Mitsuhiro ; Sivakumar, G. / Confluence of conditional rewrite systems. Conditional Term Rewriting Systems - 1st International Workshop, Proceedings. Vol. 308 LNCS Springer Verlag, 1988. pp. 31-44 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{9fba7eba85f24fbab208065e17f8bce5,
title = "Confluence of conditional rewrite systems",
abstract = "Conditional rewriting has been studied both from the point of view of algebraic data type specifications and as a computational paradigm combining logic and functional programming. An important issue, in either case, is determining whether a rewrite system has the Church-Rosser, or confluence, property. In this paper, we settle negatively the question whether “joinability of critical pairs” is, in general, sufficient for confluence of terminating conditional systems. We review known sufficient conditions for confluence, and also prove two new positive results for systems having critical pairs and arbitrarily big terms in conditions.",
author = "Nachum Dershowitz and Mitsuhiro Okada and G. Sivakumar",
year = "1988",
month = "1",
day = "1",
doi = "10.1007/3-540-19242-5_3",
language = "English",
isbn = "9783540192428",
volume = "308 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "31--44",
booktitle = "Conditional Term Rewriting Systems - 1st International Workshop, Proceedings",
address = "Germany",

}

TY - GEN

T1 - Confluence of conditional rewrite systems

AU - Dershowitz, Nachum

AU - Okada, Mitsuhiro

AU - Sivakumar, G.

PY - 1988/1/1

Y1 - 1988/1/1

N2 - Conditional rewriting has been studied both from the point of view of algebraic data type specifications and as a computational paradigm combining logic and functional programming. An important issue, in either case, is determining whether a rewrite system has the Church-Rosser, or confluence, property. In this paper, we settle negatively the question whether “joinability of critical pairs” is, in general, sufficient for confluence of terminating conditional systems. We review known sufficient conditions for confluence, and also prove two new positive results for systems having critical pairs and arbitrarily big terms in conditions.

AB - Conditional rewriting has been studied both from the point of view of algebraic data type specifications and as a computational paradigm combining logic and functional programming. An important issue, in either case, is determining whether a rewrite system has the Church-Rosser, or confluence, property. In this paper, we settle negatively the question whether “joinability of critical pairs” is, in general, sufficient for confluence of terminating conditional systems. We review known sufficient conditions for confluence, and also prove two new positive results for systems having critical pairs and arbitrarily big terms in conditions.

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

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

U2 - 10.1007/3-540-19242-5_3

DO - 10.1007/3-540-19242-5_3

M3 - Conference contribution

AN - SCOPUS:85034823126

SN - 9783540192428

VL - 308 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 31

EP - 44

BT - Conditional Term Rewriting Systems - 1st International Workshop, Proceedings

PB - Springer Verlag

ER -