Confluence of conditional rewrite systems

Nachum Dershowitz; Mitsuhiro Okada; G. Sivakumar

doi:10.1007/3-540-19242-5_3

Confluence of conditional rewrite systems

Nachum Dershowitz, Mitsuhiro Okada, G. Sivakumar

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

47 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 language	English
Title of host publication	Conditional Term Rewriting Systems - 1st International Workshop, Proceedings
Editors	Stephane Kaplan, Jean-Pierre Jouannaud
Publisher	Springer Verlag
Pages	31-44
Number of pages	14
ISBN (Print)	9783540192428
DOIs	https://doi.org/10.1007/3-540-19242-5_3
Publication status	Published - 1988
Externally published	Yes
Event	1st International Workshop on Conditional Term Rewriting Systems, 1987 - Orsay, France Duration: 1987 Jul 8 → 1987 Jul 10

Publication series

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

Other

Other	1st International Workshop on Conditional Term Rewriting Systems, 1987
Country/Territory	France
City	Orsay
Period	87/7/8 → 87/7/10

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/3-540-19242-5_3

Cite this

Dershowitz, N., Okada, M., & Sivakumar, G. (1988). Confluence of conditional rewrite systems. In S. Kaplan, & J-P. Jouannaud (Eds.), Conditional Term Rewriting Systems - 1st International Workshop, Proceedings (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. ed. / Stephane Kaplan; Jean-Pierre Jouannaud. 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 proceeding › Conference contribution

Dershowitz, N, Okada, M & Sivakumar, G 1988, Confluence of conditional rewrite systems. in S Kaplan & J-P Jouannaud (eds), Conditional Term Rewriting Systems - 1st International Workshop, Proceedings. 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 Kaplan S, Jouannaud J-P, editors, Conditional Term Rewriting Systems - 1st International Workshop, Proceedings. Springer Verlag. 1988. p. 31-44. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 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. editor / Stephane Kaplan ; Jean-Pierre Jouannaud. 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",

note = "Funding Information: * This research was supportedi n part by the National ScienceF oundationu nder Grant DCR 85-13417. Publisher Copyright: {\textcopyright} 1988, Springer-Verlag.; 1st International Workshop on Conditional Term Rewriting Systems, 1987 ; Conference date: 08-07-1987 Through 10-07-1987",

year = "1988",

doi = "10.1007/3-540-19242-5_3",

language = "English",

isbn = "9783540192428",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "31--44",

editor = "Stephane Kaplan and Jean-Pierre Jouannaud",

booktitle = "Conditional Term Rewriting Systems - 1st International Workshop, Proceedings",

}

TY - GEN

T1 - Confluence of conditional rewrite systems

AU - Dershowitz, Nachum

AU - Okada, Mitsuhiro

AU - Sivakumar, G.

PY - 1988

Y1 - 1988

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

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

A2 - Kaplan, Stephane

A2 - Jouannaud, Jean-Pierre

PB - Springer Verlag

T2 - 1st International Workshop on Conditional Term Rewriting Systems, 1987

Y2 - 8 July 1987 through 10 July 1987

ER -

Confluence of conditional rewrite systems

Abstract

Publication series

Other

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this