Non-determinsitic algebraic rewriting as adjunction
This provides a foundational theoretical framework for non-deterministic rewriting in algebraic systems, which is incremental but extends existing work to more general cases.
The paper tackles the problem of providing a formal semantics for rewriting systems that don't assume confluence or termination, by developing a model-theoretic framework based on preordered algebra. The result is a characterization of algebraic rewriting as a persistent adjunction, which is used to prove soundness and completeness for computational models in Maude and CafeOBJ, and to develop compositionality results for modular rewriting.
We develop a general model theoretic semantics to rewriting beyond the usual confluence and termination assumptions. This is based on preordered algebra which is a model theory that extends many sorted algebra. In this framework we characterise rewriting in arbitrary algebras rather than term algebras (called algebraic rewriting) as a persistent adjunction and use this result, on the one hand for proving the soundness and the completeness of an abstract computational model of rewriting that underlies the non-deterministic programming with Maude and CafeOBJ, and on the other hand for developing a compositionality result for algebraic rewriting in the context of the pushout-based modularisation technique.