Conditional Rewriting Logic: Deduction, Models and Concurrency

摘要

Term rewriting has so fat been understood almost exclusively - a technique forequational reasoning. This paper proposes a much broader interpretation in which term rewriting as such can be used both as a semantic foundation and as a programming paradigm in are 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 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.