TY - GEN
T1 - Conditional rewriting logic
T2 - 2nd International Workshop on Conditional and Typed Rewriting Systems, CTRS 1990
AU - Meseguer, José
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1991.
PY - 1991
Y1 - 1991
N2 - Term rewriting has so far been understood almost exclusively as a technique for equational reasoning. This paper proposes a much broader interpretation in which term rewriting can be used both as a semantic foundation and as a programming paradigm in areas such as reactive systems, concurrency theory and object-oriented programming that do not fit naturally within the functional world of equational logic. The interpretation proposed views conditional rewriting as a logic in its own right, with its own proof theory and with a very general model theory of wide applicability. The logic is sound and complete and admits initial models. Equational logic appears as a special refinement of the general framework; this supports a natural unification of the functional and concurrent programming paradigms with a purely declarative style. Throughout the paper, the concurrent nature of term rewriting is emphasized; the role of rewriting as a unified model of concurrency is also discussed.
AB - Term rewriting has so far been understood almost exclusively as a technique for equational reasoning. This paper proposes a much broader interpretation in which term rewriting can be used both as a semantic foundation and as a programming paradigm in areas such as reactive systems, concurrency theory and object-oriented programming that do not fit naturally within the functional world of equational logic. The interpretation proposed views conditional rewriting as a logic in its own right, with its own proof theory and with a very general model theory of wide applicability. The logic is sound and complete and admits initial models. Equational logic appears as a special refinement of the general framework; this supports a natural unification of the functional and concurrent programming paradigms with a purely declarative style. Throughout the paper, the concurrent nature of term rewriting is emphasized; the role of rewriting as a unified model of concurrency is also discussed.
UR - http://www.scopus.com/inward/record.url?scp=84960444717&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84960444717&partnerID=8YFLogxK
U2 - 10.1007/3-540-54317-1_81
DO - 10.1007/3-540-54317-1_81
M3 - Conference contribution
AN - SCOPUS:84960444717
SN - 9783540543176
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 64
EP - 91
BT - Conditional and Typed Rewriting Systems - 2nd International CTRS Workshop, Proceedings
A2 - Kaplan, Stephane
A2 - Okada, Mitsuhiro
PB - Springer
Y2 - 11 June 1990 through 14 June 1990
ER -