CONDITIONAL REWRITING LOGIC - DEDUCTION, MODELS AND CONCURRENCY

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.